CBMC

cbmc:feature/unwind-bound-analysis

  1. Git
  2. lp:cbmc
  3. feature/unwind-bound-analysis
Last commit made on 2022-11-18
Get this branch:
git clone -b feature/unwind-bound-analysis https://git.launchpad.net/cbmc

Branch merges

Branch information

Name:
feature/unwind-bound-analysis
Repository:
lp:cbmc

Recent commits

909e02f... by martin <martin@michael>

WIP

b4a19b2... by "Felipe R. Monteiro" <email address hidden>

Merge pull request #7356 from remi-delmas-3000/dfcc-disable-library-checks

CONTRACTS: Disable checks on `cprover_contracts.c`

764519a... by Michael Tautschnig <email address hidden>

Merge pull request #7360 from tautschnig/bugfixes/b-e-zero

Byte-extract lowering: extracting zero-width struct members is fine

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

Byte-extract lowering: extracting zero-width struct members is fine

We can safely handle the case of extracting zero bits, and shouldn't
fall back to a code path that would result in invalid typecast
operations.

Also fix a typo in a comment on the affected code path.

3a26e73... by Michael Tautschnig <email address hidden>

Merge pull request #7333 from diffblue/smt2_to_fp_unsigned

SMT2 parser: implement to_fp_unsigned

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

Merge pull request #7354 from FrNecas/frnecas-witness-assume-develop

Only add assumption scope if not empty

8fd4d0a... by Michael Tautschnig <email address hidden>

Merge pull request #7345 from diffblue/smt2_saturating

SMT2 backend: implement saturating arithmetic

7bea872... by Michael Tautschnig <email address hidden>

Merge pull request #7341 from tautschnig/feature/simp-pointer-subtract

Simplify non-trivial pointer subtraction

25abf15... by Michael Tautschnig <email address hidden>

Merge pull request #7352 from tautschnig/bugfixes/struct-union-empty

Byte-operator lowering: struct and union constants are not ID_constant

26fb550... by Remi Delmas <email address hidden>

CONTRACTS: disable checks on `cprover_contracts.c`

Prevents a 5-10x blowup in the number of generated checks for
DFCC instrumented programs.

Functions in `cprover_contracts.c` contain assertions that
check for possible overflows of null pointers where needed,
so we guard against automatic checks instantiation by adding
"checked" pragmas to all instructions of the library.