CBMC

cbmc:feature/spicy-loops

  1. Git
  2. lp:cbmc
  3. feature/spicy-loops
Last commit made on 2023-08-02
Get this branch:
git clone -b feature/spicy-loops https://git.launchpad.net/cbmc

Branch merges

Branch information

Name:
feature/spicy-loops
Repository:
lp:cbmc

Recent commits

560f984... by Martin Brain <email address hidden>

Add Duff's device

52cfd42... by Martin Brain <email address hidden>

WIP

ea500da... by Michael Tautschnig <email address hidden>

Merge pull request #7494 from tautschnig/bugfixes/7473-recursion

Fix symex coverage reporting of recursive calls

85b7bb9... by Fotis Koutoulakis <email address hidden>

Merge pull request #7434 from esteffin/esteffin/incr-smt2-new-regressions

Add regression tests from CBMC folder to incremental SMT2 backend

1412b19... by Michael Tautschnig <email address hidden>

Fix symex coverage reporting of recursive calls

Recursive calls have two successors as far as coverage recording in
symex is concerned: the edge back to the beginning of the function as
well as the (pseudo-)edge to instruction after the call. Fix the
invariant to account for this case.

Also, remove debugging-to-stderr.

Fixes: #7473

Co-authored-by: Qiuye-Hua

e913535... by Michael Tautschnig <email address hidden>

Merge pull request #6893 from diffblue/unsigned_pointer_offset

make pointer_offset_exprt unsigned

7cb83c1... by Remi Delmas <email address hidden>

CONTRACTS: take unsigned offsets into account

f8cc13a... by Daniel Kroening <email address hidden>

make pointer_offset_exprt unsigned

This commit changes the type of __CPROVER_POINTER_OFFSET from ssize_t to
size_t. To match, relational operators on pointers are now unsigned, to
enable p+PTRDIFF_MAX+1 > p.

The rationale is subtle. The ISO C 11 standard 6.5.8 par 5 suggests that a
pair of pointers can be compared if either the pointers point into the
object, or one beyond the end of the sequence. The behavior in the case of
a pointer that points before the sequence is undefined. There is a similar
narrative for pointer arithmetic. A pointer with an offset that has a set
most significant bit should thus compare "less than" a pointer with an
offset that has a zero MSB. This suggests an unsigned encoding.

bdc3538... by Enrico Steffinlongo <email address hidden>

Add 645 regression tests from cbmc folder

9b6d003... by Michael Tautschnig <email address hidden>

replace_expr: check type consistency

Make sure that replace_expr cannot introduce type-inconsistent
expressions. This wouldn't be a fault of replace_expr, but rather
requires fixing the caller. Add preconditions to check this.