Patch set for SV-COMP'19 [depends-on: #2000, #3462]#3486

Closed

tautschnig wants to merge 33 commits intodevelopfrom

sv-comp19

Commits on Nov 28, 2018

expr2ct hack for SV-COMP: no struct type body output
tautschnig
committed
Use clean-C configuration for graphml counterexample
tautschnig
committed
Do not output "NULL"
tautschnig
committed
No outgoing edges from violation nodes

peterschrammel
authored and
tautschnig
committed
Using cache to speed up generation of grapml file.

marek-trtik
authored and
tautschnig
committed
Hack to make CPAchecker parse graphml concurrency witnesses

peterschrammel
authored and
tautschnig
committed
Make sure SSA suffixes are stripped off graphml output

peterschrammel
authored and
tautschnig
committed
Remove obsolete graphml frontierNode, nodeType and add new cyclehead

peterschrammel
authored and
tautschnig
committed
Remove obsolete sourcecode element in graphml

peterschrammel
authored and
tautschnig
committed
Split array-list into assignments and hide dynamic objects

peterschrammel
authored and
tautschnig
committed
Remove obsolete sourcecode element from graphml

peterschrammel
authored and
tautschnig
committed
graphml: More precise detection of when to use '\result' variable.

marek-trtik
authored and
tautschnig
committed
graphml: Special (hacky) structure of concurrency witness.

marek-trtik
authored and
tautschnig
committed
Update expected graphml output, to be merged
tautschnig
committed
Add violation node for the memory safety benchmarks

lucasccordeiro
authored and
tautschnig
committed
Ensure that local declarations do not introduce spurious dead warnings
tautschnig
committed
invalid_object(pointer) is true for all non-existent objects
tautschnig
committed
fixup! Do not output "NULL"
tautschnig
committed
Add a definition of alloca
tautschnig
committed
Do not perform SSA sanity checks
tautschnig
committed
irept: Use singly-linked lists with SUB_IS_LIST
tautschnig
committed
Avoid repeated hash computation, reduce irept::dt size
tautschnig
committed
C library: model pthread_key_create, pthread_{get,set}specific
tautschnig
committed
Factor out memory leak instrumentation into separate function

peterschrammel
authored and
tautschnig
committed
Add memory leak instrumentation to abort and exit

peterschrammel
authored and
tautschnig
committed
Fix memory leak check for __VERIFIER_error

peterschrammel
authored and
tautschnig
committed
Needs more profiling: Do not sort operands as part of simplification
tautschnig
committed
Detect use of free() with alloca-allocated objects
tautschnig
committed
pthread_cond_wait may return spuriously
tautschnig
committed
Don't implement pthread_keyt destructors
tautschnig
committed
Non-deterministic initialisation of argc/argv/envp
tautschnig
committed
clang-format cleanup
tautschnig
committed
Skip phi assignment if one of the merged states has an uninitialised object
tautschnig
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Patch set for SV-COMP'19 [depends-on: #2000, #3462]#3486

Commits on Nov 28, 2018

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

Use clean-C configuration for graphml counterexample

Do not output "NULL"

No outgoing edges from violation nodes

Using cache to speed up generation of grapml file.

Hack to make CPAchecker parse graphml concurrency witnesses

Make sure SSA suffixes are stripped off graphml output

Remove obsolete graphml frontierNode, nodeType and add new cyclehead

Remove obsolete sourcecode element in graphml

Split array-list into assignments and hide dynamic objects

Remove obsolete sourcecode element from graphml

graphml: More precise detection of when to use '\result' variable.

graphml: Special (hacky) structure of concurrency witness.

Update expected graphml output, to be merged

Add violation node for the memory safety benchmarks

Ensure that local declarations do not introduce spurious dead warnings

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

fixup! Do not output "NULL"

Add a definition of alloca

Do not perform SSA sanity checks

irept: Use singly-linked lists with SUB_IS_LIST

Avoid repeated hash computation, reduce irept::dt size

C library: model pthread_key_create, pthread_{get,set}specific

Factor out memory leak instrumentation into separate function

Add memory leak instrumentation to abort and exit

Fix memory leak check for __VERIFIER_error

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

Detect use of free() with alloca-allocated objects

pthread_cond_wait may return spuriously

Don't implement pthread_keyt destructors

Non-deterministic initialisation of argc/argv/envp

clang-format cleanup

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