lp:cbmc

Author: Michael Tautschnig
Author Date: 2024-04-26 09:57:54 UTC

Deploying to gh-pages from @ diffblue/cbmc@2d63a718b10371b5a08175f67e1b171a98a33364 🚀

Author: Michael Tautschnig
Author Date: 2024-04-26 09:55:11 UTC

Merge pull request #8238 from tautschnig/features/dprintf

C library: implement {v,}dprintf

Author: Daniel Kroening
Author Date: 2024-04-02 16:57:30 UTC

introduce 'fatal assertions'

This introduces a variant of ASSERT instructions that are fatal when they
are refuted. Execution paths through fatal assertions that are refuted are
undefined. Assertions that (otherwise) pass and that are reachable from a
refuted fatal assertion are now reported as UNKNOWN.

The motivating use-case for fatal assertions is undefined behavior in
languages such as C/C++ or Rust.

Noi attempt is made to modify the outcome of ASSERT instructions that are
refuted owing to a trace through a refuted fatal assertion. The computation
of the trace is not robust enough.

Author: Daniel Kroening
Author Date: 2024-04-01 21:02:32 UTC

clang-format the moved files

Author: Daniel Kroening
Author Date: 2024-04-01 21:02:32 UTC

clang-format the moved files

Author: Daniel Kroening
Author Date: 2024-03-19 20:29:08 UTC

simplify extractbits_exprt representation

The current representation of extractbits_exprt stores both the upper and
lower indices of the range that is to be extracted, and their difference
plus one in form of the width of the type of the expression.

This removes the upper index, as it can be deduced from the lower index and
the width of the result. The key benefit is reducing burden on the user of
the class, who a) doesn't have to remember which index comes first, and b)
doesn't have to do the calculation of the upper index.

Author: Daniel Kroening
Author Date: 2024-03-10 12:46:19 UTC

CI: fix chocolatey error

Chocolatey reports "Cannot read keys when either application does not have a console".

Author: Daniel Kroening
Author Date: 2024-02-24 15:33:21 UTC

fixup update_bits_exprt

Author: Daniel Kroening
Author Date: 2024-02-03 23:57:47 UTC

SMT2: implement with on bit-vectors

Author: Daniel Kroening
Author Date: 2023-12-24 17:20:34 UTC

cbmc preprocessing: call set_language_options after checking for null

This avoids a segfault when there is no appropriate language module.

Author: Daniel Kroening
Author Date: 2023-12-18 16:08:36 UTC

fix nondeterministic hex_trace test

The cbmc/hex_trace test pattern relies on a particular value (0) for an
uninitialized local variable. This removes the pattern.

See
https://github.com/diffblue/cbmc/actions/runs/6672135313/job/18269948126?pr=7979
as an exemplar where this was triggered.

Author: Daniel Kroening
Author Date: 2023-11-27 21:48:35 UTC

tweak whitespace to satisfy cpplint

Author: Thomas Given-Wilson
Author Date: 2023-10-29 11:17:21 UTC

Add CODEOWNERS for CHANGELOG

Add specific CODEOWNERS for CHANGELOG

Author: Thomas Given-Wilson
Author Date: 2023-09-14 09:24:24 UTC

Increment version to cbmc 5.92.0

Author: Thomas Given-Wilson
Author Date: 2023-08-03 12:38:29 UTC

Turns off using lambdas for array comprehension

Using lambdas for array comprehension can cause errors in
get-value operations later.

Fixes #7767

Author: Thomas Given-Wilson
Author Date: 2023-08-03 09:41:45 UTC

20230803-cbmc-5.89.0

Author: Martin Brain
Author Date: 2023-08-02 15:13:24 UTC

Add Duff's device

Author: Daniel Kroening
Author Date: 2023-05-01 15:11:12 UTC

add a 'language feature' facility for goto programs

This adds a facility to track the language features used by a goto program.
The features are stored in the value of a symbol in the symbol table part of
a goto model. The default, when not specificd, is 'true', i.e., we
conservatively assume that the feature might be in use unless we know
otherwise.

Checks for three language features not supported by goto symex are added
(assembler, function pointers, vectors).

Author: Thomas Given-Wilson
Author Date: 2023-04-27 10:32:24 UTC

CBMC version 5.82.0

Author: Thomas Given-Wilson
Author Date: 2023-04-26 21:04:27 UTC

Dirty hackery

Author: TGWDB
Author Date: 2023-04-03 20:52:37 UTC

Merge pull request #7645 from NlightNFotis/rust_verification_result

Translate verification results from C++ to Rust

Author: Daniel Kroening
Author Date: 2023-01-09 13:18:47 UTC

avoid deprecated std::iterator

C++17 deprecates std::iterator. The recommended alternative is to use an
iterator_category member.

Author: martin
Author Date: 2021-10-10 20:24:58 UTC

WIP

Author: Daniel Kroening
Author Date: 2022-11-12 17:52:12 UTC

CHC solver: byte-wise reading

This adds support for reading objects byte-wise via a cast to char * using a
byte_extract expression.

Author: Daniel Kroening
Author Date: 2022-11-11 14:59:31 UTC

introduce state labels

Author: Daniel Kroening
Author Date: 2022-11-03 10:14:20 UTC

disallow flexible array members in unions

This change yields an error if a flexible array member is used in a union.
C11 allows them in structs, but not unions.

Author: Daniel Kroening
Author Date: 2022-11-03 09:47:18 UTC

fx

Author: Daniel Kroening
Author Date: 2022-10-18 20:27:03 UTC

extract inductiveness check

Author: Daniel Kroening
Author Date: 2022-09-20 13:21:59 UTC

index_exprt now checks type of index operand

The constructors of index_exprt now check the type of the index operand.

1) In the case of vectors, a precondition enforces that the index operand
has the index type.

2) In the case of arrays, a typecast is added in case the type differs.
The correct type will be enforced eventually.

Author: Daniel Kroening
Author Date: 2022-10-13 13:45:37 UTC

replace usage of source_locationt::get_function()

Author: Daniel Kroening
Author Date: 2022-09-21 12:56:51 UTC

remove enum_constant_type()

The function has been deprecated in January 2022, and has no users in the
code base.

Author: TGWDB
Author Date: 2022-09-15 13:54:30 UTC

Revert "introduce cstrlen_exprt"

Author: Daniel Kroening
Author Date: 2022-06-11 11:00:17 UTC

introduce __CPROVER_map type

This introduces C syntax for a type

  __CPROVER_map domain -> codomain

where domain is a list of types and codomain is a type. The type is
internal, for modeling purposes. It replaces arrays with size
__CPROVER_infinity, which are now deprecated.

Author: Daniel Kroening
Author Date: 2021-10-21 11:47:58 UTC

goto symex now handles function pointers

Author: Daniel Kroening
Author Date: 2022-05-31 10:09:44 UTC

introduce __CPROVER_pointer_offset_t

Author: Daniel Kroening
Author Date: 2022-05-26 10:05:20 UTC

simplifier: use resultt<> instead of bool

The consistent use of resultt<> makes the code easier to read.

Author: Daniel Kroening
Author Date: 2022-05-13 02:23:30 UTC

codet is not an expression

Author: Daniel Kroening
Author Date: 2022-04-29 14:18:38 UTC

fx

Author: Daniel Kroening
Author Date: 2022-04-28 21:59:32 UTC

re-encode integers converted to pointers

Author: Daniel Kroening
Author Date: 2017-07-26 07:26:06 UTC

Array theory: implement weakly equivalent arrays

This implements Christ and Hoenicke's Weakly Equivalent Arrays
(https://arxiv.org/pdf/1405.6939.pdf) with in-place depth-first path
enumeration.

Co-authored-by: Michael Tautschnig <tautschn@amazon.com>

Author: Daniel Kroening
Author Date: 2022-01-02 21:05:06 UTC

add a test with invalid quantifications over Booleans

Author: Daniel Kroening
Author Date: 2021-06-28 14:01:28 UTC

remove encoding of arrays of bools into bitvector

The encoding of arrays of booleans as arrays of (_ bitvec 1) was necessary
when solvers did not support arrays of booleans.

This support is now broadly available, removing the need for this code path.

Author: Saswat Padhi
Author Date: 2022-02-17 01:12:11 UTC

fix minor sign comparison warnings

Author: Daniel Kroening
Author Date: 2022-01-31 15:19:21 UTC

remove direct use of typet::subtype()

Author: Grigory Fedyukovich
Author Date: 2021-12-30 07:04:32 UTC

added pointer dereferencing check;
fixed minor bugs; added more regression tests

Author: Daniel Kroening
Author Date: 2021-11-08 15:10:20 UTC

expand value_sett::apply_code_rec

The method value_sett::apply_code_rec is expanded at its call site; this
removes the invocation of get_code(), which is earmarked for removal.

Author: Daniel Kroening
Author Date: 2021-10-26 18:59:52 UTC

__CPROVER_r/w_ok does not require null or a valid pointer

The definition of __CPROVER_r/w_ok (in goto_check.cpp) does include the case
of an invalid pointer, and thus, there is no need to check that the pointer
given to these predicates is valid.

Author: Daniel Kroening
Author Date: 2021-09-25 16:23:04 UTC

is_invalid_pointer is now defined as a bi-implication

The previous encoding of is_invalid_pointer is an implication,
which means that constraints that a pointer is not an invalid
pointer have no meaning.

This commit changes the encoding to be a bi-implication, using
the numerical range of the valid pointers.

Author: Daniel Kroening
Author Date: 2021-10-10 20:58:05 UTC

move code_declt to goto_instruction_code.h

code_declt is now used exclusively by goto instructions, and thus belongs
into goto_instruction_code.h.

Author: Daniel Kroening
Author Date: 2019-01-27 11:47:09 UTC

add an implementation of std::variant<...>

This allows strengthening type safety in a number of data structures we
already have.

Author: Daniel Kroening
Author Date: 2021-08-27 18:52:22 UTC

remove two uses of goto_instructiont::incoming_edges

This removes two uses of goto_instructiont::incoming_edges, which is
deprecated.

Author: Elizabeth Polgreen
Author Date: 2021-05-20 17:57:58 UTC

fix unary minus smt literals

Author: martin
Author Date: 2021-06-17 12:49:50 UTC

Tag another test that fails if you don't have z3 on your path

Author: Daniel Kroening
Author Date: 2021-03-25 21:15:43 UTC

smt2 parser: lambda

Author: Daniel Kroening
Author Date: 2021-03-17 09:11:08 UTC

C grammar: introduce attribute_specifier

This is a preparatory step for introducing C2x-style attribute specifiers.

This also makes it easier to introduce other, custom attributes, say for
code contracts.

Author: Michael Tautschnig
Author Date: 2019-03-02 12:23:43 UTC

Remove base_type_eq

We consistently use tag types, and two expressions are now base_type_eq if, and
only if, they have types that compare equal.

Author: Daniel Kroening
Author Date: 2020-09-23 19:22:19 UTC

add encoding for SYNTH-COMP

Author: Fotis Koutoulakis
Author Date: 2020-08-10 15:15:57 UTC

Build CBMC in Visual Studio 2019, in Github Actions.

Author: Daniel Kroening
Author Date: 2020-08-17 19:50:18 UTC

array decision procedure now knows array_list_exprt

Author: Daniel Kroening
Author Date: 2020-07-28 08:36:31 UTC

goto-instrument: function pointer removal with value_set_fi

This adds a new option to goto-instrument for removing function pointers.
The points-to analysis is done using flow-insensitive value sets, which is
more precise than using the signature of the function to identify the
points-to set.

Author: hannes-steffenhagen-diffblue
Author Date: 2020-07-15 09:53:55 UTC

Merge pull request #5372 from hannes-steffenhagen-diffblue/vsd/new-value-set/basic-value-set-operations

Implement basic operations for VSD Value Sets

Author: Daniel Kroening
Author Date: 2020-06-22 14:01:55 UTC

add --remote-sat command line option

This option selects the 'remote SAT' solver.

Author: Daniel Kroening
Author Date: 2020-05-30 08:31:11 UTC

add missing virtual destructor

This adds a virtual destructor, enabling compilation with recent versions of
clang++.

Author: Daniel Kroening
Author Date: 2020-05-30 08:26:07 UTC

add missing std::move on return

This enables compilation with recent versions of clang++.

Author: Daniel Kroening
Author Date: 2020-05-13 17:38:05 UTC

use mp_integer instead of size_t

This prevents a dependency of the analysis on the architecture that CBMC has
been compiled for.

Author: Fotis Koutoulakis
Author Date: 2020-04-20 12:55:23 UTC

Merge pull request #5300 from NlightNFotis/feature/vsd_value_set

Add the value sets to the variable sensitivity domain

Author: Chris Smowton
Author Date: 2020-02-21 11:36:23 UTC

String solver: support bounded-length intermediate strings, smaller index sets

This introduces two related features: the ability for the string solver to use constant-sized
arrays to store variable-length strings (which may be cheaper since smaller formulas are
generally needed to represent them and their constraints to the solver), and the ability to
maintain its array index-sets as sets of constants rather than symbolic expressions, which
can save a great deal of time and memory in the situation where there are many symbolic
indices that in all models occurring in practice tend to refer to the same indices.

Both are off-by-default for now since they are not heavily studied: I expect constant-sized
arrays would be expensive in the case where strings are numerous and sparsely constrained,
while storing index-sets as constants will result in more solver iterations when the solver
changes its valuation of symbolic index expressions each iteration (meaning the index set
grows despite the symbolic index set remaining the same size).

Author: martin
Author Date: 2019-08-22 23:08:20 UTC

Thread a single history through all initialisation and fixedpoints

This is needed to support histories that carry information across
function calls. It requires some changes to the internal API in
ai_baset but should not give any changes to the results computed.

Author: Daniel Kroening
Author Date: 2019-11-14 08:22:45 UTC

accept multiple instances of the --unwinset command line option

This closes issue #5185

Author: Daniel Kroening
Author Date: 2019-11-05 14:09:59 UTC

remove unnecessary .c_str()

Author: Lukasz A.J. Wrona
Author Date: 2019-10-17 10:58:05 UTC

fixup! codebuild windows cmake

Author: Daniel Kroening
Author Date: 2019-10-13 16:37:11 UTC

turn nullary function symbols into function applications

Author: Nathan Phillips
Author Date: 2018-03-16 17:27:24 UTC

Unit test to demonstrate issue in make_object_get_class_code

Author: Owen
Author Date: 2019-08-22 09:26:57 UTC

Document profiling option

Add instructions on building cprover binaries so they can be profiled
by a tool like gprof.

Author: Antonia Lechner
Author Date: 2019-08-08 12:47:33 UTC

Remove accidental echo

Author: Antonia Lechner
Author Date: 2019-08-08 10:51:50 UTC

change that clang-format should not detect

Author: Daniel Kroening
Author Date: 2019-06-06 10:15:19 UTC

introduce code_havoc_objectt

This documents an existing codet variant.

Author: Daniel Kroening
Author Date: 2019-04-06 19:10:45 UTC

remove java_method_typet::final/native

This removes four methods from java_method_typet. They do not belong there,
as neither 'native' nor 'final' are part of the type of the method (they are
field modifiers). They are never read.

Author: Daniel Kroening
Author Date: 2019-02-03 19:17:41 UTC

java: do not use void reference

The concept of 'void *' is borrowed from C. This commit changes 'void *' to
a reference to java.lang.object.

The benefit is that we will be able to establish that all references in Java
are references to an object.

Author: Daniel Kroening
Author Date: 2018-05-25 10:23:43 UTC

enable conversion from irep_idt to enum class

Author: Kareem Khazem
Author Date: 2019-07-17 13:22:52 UTC

Whitespace fixes in preparation for func contracts

This commit applies clang-format and other whitespace changes introduced
by future commits, which introduce function contracts.

Author: Daniel Kroening
Author Date: 2019-07-11 13:49:54 UTC

pre/post traversal expression transformers

Transformers for expressions that offer an interface similar to that offered
by

void goto_programt::transform(std::function<optionalt<exprt>(exprt)>);

on goto programs. Both pre- and post-traversal options are available.

The key benefit over the non-const visit method is that sharing is only
broken up when required.

Author: xbauch
Author Date: 2019-07-02 09:25:11 UTC

Force-fail float-div test on smt2_solver

Author: Daniel Kroening
Author Date: 2019-06-28 10:52:03 UTC

more new interface

Author: Peter Schrammel
Author Date: 2019-06-08 15:17:22 UTC

Patch to make compile

Author: Peter Schrammel
Author Date: 2019-06-08 15:17:22 UTC

Patch to make compile

Author: Peter Schrammel
Author Date: 2019-06-08 15:17:32 UTC

Patch to make compile

Author: Peter Schrammel
Author Date: 2019-06-08 15:17:23 UTC

Patch to make compile

Author: Peter Schrammel
Author Date: 2019-06-08 15:17:26 UTC

Patch to make compile

Author: Peter Schrammel
Author Date: 2019-06-08 15:25:18 UTC

Patch to make compile

Author: Peter Schrammel
Author Date: 2019-06-08 15:17:42 UTC

Patch to make compile

Author: Peter Schrammel
Author Date: 2019-06-08 15:17:45 UTC

Patch to make compile

Author: Peter Schrammel
Author Date: 2019-06-08 15:17:44 UTC

Patch to make compile

Author: Peter Schrammel
Author Date: 2019-06-08 15:17:30 UTC

Patch to make compile

Author: Peter Schrammel
Author Date: 2019-06-08 15:17:29 UTC

Patch to make compile

Author: Peter Schrammel
Author Date: 2019-06-08 15:17:28 UTC

Patch to make compile

Author: Daniel Kroening
Author Date: 2019-05-30 12:58:20 UTC

remove_java_new can now follow one typecast

statements such as

var = (type) java_new(....)

can now be lowered. This removes the requirement to introduce a temporary
just to do the typecast.

Author: Daniel Kroening
Author Date: 2018-09-22 00:10:47 UTC

correct type of boolean operators

Author: Daniel Kroening
Author Date: 2019-05-28 13:22:46 UTC

change signature of simplify_inequality_*

Author: Daniel Kroening
Author Date: 2018-12-07 16:05:26 UTC

added java2goto