CBMC

cbmc:sv-comp19

  1. Git
  2. lp:cbmc
  3. sv-comp19
Last commit made on 2018-11-28
Get this branch:
git clone -b sv-comp19 https://git.launchpad.net/cbmc

Branch merges

Branch information

Name:
sv-comp19
Repository:
lp:cbmc

Recent commits

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

Skip phi assignment if one of the merged states has an uninitialised object

With level-2 counters incremented on declaration and non-deterministic
initialisation upon allocation, the only remaining sources are pointer
dereferencing, where uninitialised objects necessarily refer to invalid objects.

This is a cleaner implementation of 369f077d2e. Removing only the code
introduced in 369f077d2e would yield a wrong result for
regression/cbmc/Local_out_of_scope3.

95f1859... by Michael Tautschnig <email address hidden>

clang-format cleanup

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

Non-deterministic initialisation of argc/argv/envp

443dfdb... by Michael Tautschnig <email address hidden>

Don't implement pthread_keyt destructors

They are too expensive due to extensive shared-variable use.

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

pthread_cond_wait may return spuriously

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

Detect use of free() with alloca-allocated objects

As we internally use dynamic allocation, we previously did not distinguish
alloca-allocated from malloc/calloc-allocated ones.

4d6d81f... by Michael Tautschnig <email address hidden>

Needs more profiling: Do not sort operands as part of simplification

7e3b18a... by Peter Schrammel <email address hidden>

Fix memory leak check for __VERIFIER_error

1672dbc... by Peter Schrammel <email address hidden>

Add memory leak instrumentation to abort and exit

53e4f60... by Peter Schrammel <email address hidden>

Factor out memory leak instrumentation into separate function