Collection of patches for SV-COMP'17#363

Closed

tautschnig wants to merge 24 commits intodiffblue:developfrom

tautschnig:sv-comp-2017

Commits on Jun 8, 2017

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

martin
authored and
tautschnig
committed
An alternative implementation to avoid the difference between RNE and RNA.

martin
authored and
tautschnig
committed
Fix special cases for the remainder functions, now down to 4 failures!

martin
authored and
tautschnig
committed
Support "polymorphic" floating-point functions, fix typos
tautschnig
committed
Do not perform SSA sanity checks
tautschnig
committed
Avoid repeated hash computation, reduce irept::dt size
tautschnig
committed
Constrain the malloc/alloca size to fit our object:offset encoding
tautschnig
committed
Abort concurrency encoding in possibly unsound cases
tautschnig
committed
Update all constant offsets, not just 0
tautschnig
committed
Abort on byte_update(pointer)
tautschnig
committed
Ensure that local declarations do not introduce spurious dead warnings
tautschnig
committed
Needs more profiling: Do not sort operands as part of simplification
tautschnig
committed
Split ID_and/ID_or vs ID_xor simplification
tautschnig
committed
Do not unnecessarily sort guard conjuncts
tautschnig
committed
Switch SAT solver to glucose
tautschnig
committed
Generalize ID_malloc to ID_allocate with optional zero-init
tautschnig
committed
Check for memory leaks in C++ new/delete
tautschnig
committed
invalid_object(pointer) is true for all non-existent objects
tautschnig
committed
Use a known constant offset when dereferencing
tautschnig
committed
Extensions to simplify_byte_extract
tautschnig
committed
expr2ct hack for SV-COMP: no struct type body output
tautschnig
committed

Commits on Oct 13, 2017

fixup! Generalize ID_malloc to ID_allocate with optional zero-init
tautschnig
committed
fixup! invalid_object(pointer) is true for all non-existent objects
tautschnig
committed
Update Glucose interface
tautschnig
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Collection of patches for SV-COMP'17#363

Collection of patches for SV-COMP'17#363
tautschnig wants to merge 24 commits intodiffblue:developfrom
tautschnig:sv-comp-2017

Commits on Jun 8, 2017

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

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

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

Support "polymorphic" floating-point functions, fix typos

Do not perform SSA sanity checks

Avoid repeated hash computation, reduce irept::dt size

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

Abort concurrency encoding in possibly unsound cases

Update all constant offsets, not just 0

Abort on byte_update(pointer)

Ensure that local declarations do not introduce spurious dead warnings

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

Split ID_and/ID_or vs ID_xor simplification

Do not unnecessarily sort guard conjuncts

Switch SAT solver to glucose

Generalize ID_malloc to ID_allocate with optional zero-init

Check for memory leaks in C++ new/delete

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

Use a known constant offset when dereferencing

Extensions to simplify_byte_extract

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

Commits on Oct 13, 2017

fixup! Generalize ID_malloc to ID_allocate with optional zero-init

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

Update Glucose interface

Collection of patches for SV-COMP'17#363tautschnig 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

Commits on Oct 13, 2017

Collection of patches for SV-COMP'17#363
tautschnig wants to merge 24 commits intodiffblue:developfrom
tautschnig:sv-comp-2017