Code

Collection of patches for SV-COMP'17#363

Code

Closed

tautschnig wants to merge 24 commits intodiffblue:developdiffblue/cbmc:developfrom

tautschnig:sv-comp-2017tautschnig/cbmc:sv-comp-2017Copy head branch name to clipboard

Commits

Commits on Jun 8, 2017

• A first cut at the additions we need to the math library.

  

  martin

  authored and

  tautschnig

  committed
  2345494

  Copy full SHA for 2345494

• An alternative implementation to avoid the difference between RNE and RNA.

  

  martin

  authored and

  tautschnig

  committed
  e4b3dcc

  Copy full SHA for e4b3dcc

• Fix special cases for the remainder functions, now down to 4 failures!

  

  martin

  authored and

  tautschnig

  committed
  c83bfde

  Copy full SHA for c83bfde

• Support "polymorphic" floating-point functions, fix typos

  Show description for 53513f0
  tautschnig

  committed
  53513f0

  Copy full SHA for 53513f0

• Do not perform SSA sanity checks

  Show description for 88d613f
  tautschnig

  committed
  88d613f

  Copy full SHA for 88d613f

• Avoid repeated hash computation, reduce irept::dt size

  Show description for 3abe347
  tautschnig

  committed
  3abe347

  Copy full SHA for 3abe347

• Constrain the malloc/alloca size to fit our object:offset encoding

  Show description for 55303ec
  tautschnig

  committed
  55303ec

  Copy full SHA for 55303ec

• Abort concurrency encoding in possibly unsound cases

  tautschnig

  committed
  05caee0

  Copy full SHA for 05caee0

• Update all constant offsets, not just 0

  tautschnig

  committed
  6d257b4

  Copy full SHA for 6d257b4

• Abort on byte_update(pointer)

  Show description for 50b2473
  tautschnig

  committed
  50b2473

  Copy full SHA for 50b2473

• Ensure that local declarations do not introduce spurious dead warnings

  Show description for 99fc38e
  tautschnig

  committed
  99fc38e

  Copy full SHA for 99fc38e

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

  tautschnig

  committed
  8b40b47

  Copy full SHA for 8b40b47

• Split ID_and/ID_or vs ID_xor simplification

  Show description for 45f5f6a
  tautschnig

  committed
  45f5f6a

  Copy full SHA for 45f5f6a

• Do not unnecessarily sort guard conjuncts

  Show description for 8c2d426
  tautschnig

  committed
  8c2d426

  Copy full SHA for 8c2d426

• Switch SAT solver to glucose

  tautschnig

  committed
  8bea311

  Copy full SHA for 8bea311

• Generalize ID_malloc to ID_allocate with optional zero-init

  Show description for dc5b865
  tautschnig

  committed
  dc5b865

  Copy full SHA for dc5b865

• Check for memory leaks in C++ new/delete

  tautschnig

  committed
  97091d4

  Copy full SHA for 97091d4

• invalid_object(pointer) is true for all non-existent objects

  Show description for d556ef1
  tautschnig

  committed
  d556ef1

  Copy full SHA for d556ef1

• Use a known constant offset when dereferencing

  tautschnig

  committed
  e6b7de7

  Copy full SHA for e6b7de7

• Extensions to simplify_byte_extract

  Show description for 1c51cbf
  tautschnig

  committed
  1c51cbf

  Copy full SHA for 1c51cbf

• expr2ct hack for SV-COMP: no struct type body output

  Show description for cdd7f3a
  tautschnig

  committed
  cdd7f3a

  Copy full SHA for cdd7f3a

Commits on Oct 13, 2017

• fixup! Generalize ID_malloc to ID_allocate with optional zero-init

  tautschnig

  committed
  b61360a

  Copy full SHA for b61360a

• fixup! invalid_object(pointer) is true for all non-existent objects

  tautschnig

  committed
  96af9f3

  Copy full SHA for 96af9f3

• Update Glucose interface

  tautschnig

  committed
  7994464

  Copy full SHA for 7994464