CBMC

cbmc:experiment

  1. Git
  2. lp:cbmc
  3. experiment
Last commit made on 2023-04-26
Get this branch:
git clone -b experiment https://git.launchpad.net/cbmc

Branch merges

Branch information

Name:
experiment
Repository:
lp:cbmc

Recent commits

ddb1675... by Thomas Given-Wilson <email address hidden>

Dirty hackery

793801c... by Michael Tautschnig <email address hidden>

Merge pull request #7676 from tautschnig/bugfixes/cvc5-no-lambda

SMT2 back-end: CVC5 does not support lambda expressions

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

SMT2 back-end: CVC5 does not support lambda expressions

I wrongly asserted (in 8fdb8bb8bd8) that CVC5 supports lambda. It
seemingly does not, as can also be confirmed using Z3's test
https://github.com/Z3Prover/z3test/blob/master/regressions/smt2/memset.smt2.

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

Merge pull request #7618 from tautschnig/features/less-than-prop

Enable constant propagation in less-than encoding

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

Enable constant propagation in less-than encoding

When comparing two bitvectors that are (in parts) constant then the
result should be a constant.

6f82023... by Michael Tautschnig <email address hidden>

Merge pull request #7669 from tautschnig/bugfixes/7654-byte-extract

Byte-extract lowering: do not blindly use offsets

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

Byte-extract lowering: do not blindly use offsets

When unpacking an array we must not create 0 bytes up until an offset
when the source array can never be as large. Doing so when within a
struct would spuriously produce a larger member.

The test case highlighted a problem in the SMT2 back-end: the first
operand of a struct was not correctly flattened and instead used default
expression conversion (which is only ok when the array theory is never
being used). To avoid this problem creeping in again, factor out the
operand conversion into a lambda and invoke that lambda each time.

Fixes: #7654

5cd2d1b... by Michael Tautschnig <email address hidden>

Merge pull request #7648 from tautschnig/features/preserve-sizeof

Simplify overflow-result: preserve sizeof annotation

d2d7f76... by Fotis Koutoulakis <email address hidden>

Merge pull request #7665 from esteffin/esteffin/gcc-12-unreachable-fix

Fixup GCC 12 errors

40401ce... by Michael Tautschnig <email address hidden>

Merge pull request #7622 from tautschnig/features/simplify-array-size

Simplify array size expressions