diff --git a/regression/cbmc-concurrency/thread_chain_cbmc1/main.c b/regression/cbmc-concurrency/thread_chain_cbmc1/main.c index f9e0ab46b64..ed0471a5b18 100644 --- a/regression/cbmc-concurrency/thread_chain_cbmc1/main.c +++ b/regression/cbmc-concurrency/thread_chain_cbmc1/main.c @@ -18,7 +18,7 @@ typedef unsigned long thread_id_t; // Internal unbounded array indexed by local thread identifiers -extern __CPROVER_bool __CPROVER_threads_exited[]; +__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint]; // A thread_chain is like a chain of threads `f, g, ...` where `f` // must terminate before `g` can start to run, and so forth. diff --git a/regression/cbmc-concurrency/thread_chain_cbmc2/main.c b/regression/cbmc-concurrency/thread_chain_cbmc2/main.c index f9e0ab46b64..ed0471a5b18 100644 --- a/regression/cbmc-concurrency/thread_chain_cbmc2/main.c +++ b/regression/cbmc-concurrency/thread_chain_cbmc2/main.c @@ -18,7 +18,7 @@ typedef unsigned long thread_id_t; // Internal unbounded array indexed by local thread identifiers -extern __CPROVER_bool __CPROVER_threads_exited[]; +__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint]; // A thread_chain is like a chain of threads `f, g, ...` where `f` // must terminate before `g` can start to run, and so forth. diff --git a/regression/cbmc-library/__atomic_always_lock_free-01/main.c b/regression/cbmc-library/__atomic_always_lock_free-01/main.c index cfb762868e4..5b88bd587df 100644 --- a/regression/cbmc-library/__atomic_always_lock_free-01/main.c +++ b/regression/cbmc-library/__atomic_always_lock_free-01/main.c @@ -1,5 +1,9 @@ #include +#ifndef __GNUC__ +_Bool __atomic_always_lock_free(__CPROVER_size_t, void *); +#endif + int main() { assert(__atomic_always_lock_free(sizeof(int), 0)); diff --git a/regression/cbmc-library/__atomic_clear-01/main.c b/regression/cbmc-library/__atomic_clear-01/main.c index 94a759177c5..57bf57abbc2 100644 --- a/regression/cbmc-library/__atomic_clear-01/main.c +++ b/regression/cbmc-library/__atomic_clear-01/main.c @@ -1,5 +1,9 @@ #include +#ifndef __GNUC__ +void __atomic_clear(_Bool *, int); +#endif + int main() { _Bool n; diff --git a/regression/cbmc-library/__atomic_is_lock_free-01/main.c b/regression/cbmc-library/__atomic_is_lock_free-01/main.c index 514abeaac5d..3ac747b7976 100644 --- a/regression/cbmc-library/__atomic_is_lock_free-01/main.c +++ b/regression/cbmc-library/__atomic_is_lock_free-01/main.c @@ -1,5 +1,9 @@ #include +#ifndef __GNUC__ +_Bool __atomic_is_lock_free(__CPROVER_size_t, void *); +#endif + int main() { assert(__atomic_is_lock_free(sizeof(int), 0)); diff --git a/regression/cbmc-library/__atomic_signal_fence-01/main.c b/regression/cbmc-library/__atomic_signal_fence-01/main.c index 3a809cf651f..539a54287e5 100644 --- a/regression/cbmc-library/__atomic_signal_fence-01/main.c +++ b/regression/cbmc-library/__atomic_signal_fence-01/main.c @@ -1,5 +1,9 @@ #include +#ifndef __GNUC__ +void __atomic_signal_fence(int); +#endif + int main() { __atomic_signal_fence(0); diff --git a/regression/cbmc-library/__atomic_test_and_set-01/main.c b/regression/cbmc-library/__atomic_test_and_set-01/main.c index 9a9150b3766..4fdcf0ffb68 100644 --- a/regression/cbmc-library/__atomic_test_and_set-01/main.c +++ b/regression/cbmc-library/__atomic_test_and_set-01/main.c @@ -1,5 +1,9 @@ #include +#ifndef __GNUC__ +_Bool __atomic_test_and_set(void *, int); +#endif + int main() { char c = 0; diff --git a/regression/cbmc-library/__atomic_thread_fence-01/main.c b/regression/cbmc-library/__atomic_thread_fence-01/main.c index b9001b81810..dd08b8e1801 100644 --- a/regression/cbmc-library/__atomic_thread_fence-01/main.c +++ b/regression/cbmc-library/__atomic_thread_fence-01/main.c @@ -1,5 +1,9 @@ #include +#ifndef __GNUC__ +void __atomic_thread_fence(int); +#endif + int main() { __atomic_thread_fence(0); diff --git a/regression/cbmc-library/__errno_location-01/main.c b/regression/cbmc-library/__errno_location-01/main.c index 24329d09ff5..c32d17bf73b 100644 --- a/regression/cbmc-library/__errno_location-01/main.c +++ b/regression/cbmc-library/__errno_location-01/main.c @@ -1,9 +1,9 @@ #include #include -int main() +int main(int arc, char *argv[]) { - __errno_location(); - assert(0); + // errno expands to use of __errno_location() with glibc + assert(errno == 0); return 0; } diff --git a/regression/cbmc-library/__errno_location-01/test.desc b/regression/cbmc-library/__errno_location-01/test.desc index 9542d988e8d..96c9b4bcd7b 100644 --- a/regression/cbmc-library/__errno_location-01/test.desc +++ b/regression/cbmc-library/__errno_location-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/_longjmp-01/main.c b/regression/cbmc-library/_longjmp-01/main.c index cdac71afdc5..5be8777c4ed 100644 --- a/regression/cbmc-library/_longjmp-01/main.c +++ b/regression/cbmc-library/_longjmp-01/main.c @@ -1,5 +1,9 @@ #include +#ifndef __GNUC__ +# define _longjmp(a, b) longjmp(a, b) +#endif + static jmp_buf env; int main() diff --git a/regression/cbmc-library/_longjmp-01/test.desc b/regression/cbmc-library/_longjmp-01/test.desc index c07910fc69d..b7d7e2001ce 100644 --- a/regression/cbmc-library/_longjmp-01/test.desc +++ b/regression/cbmc-library/_longjmp-01/test.desc @@ -1,8 +1,8 @@ CORE main.c --pointer-check --bounds-check -^\[_longjmp.assertion.1\] line 12 _longjmp requires instrumentation: FAILURE$ -^\[main.assertion.1\] line 8 unreachable: SUCCESS$ +^\[_?longjmp.assertion.1\] line 12 _?longjmp requires instrumentation: FAILURE$ +^\[main.assertion.1\] line 12 unreachable: SUCCESS$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/atexit-01/main.c b/regression/cbmc-library/atexit-01/main.c new file mode 100644 index 00000000000..40ee8f2201b --- /dev/null +++ b/regression/cbmc-library/atexit-01/main.c @@ -0,0 +1,12 @@ +#include +#include + +void cleanup() +{ + assert(0); +} + +int main() +{ + atexit(cleanup); +} diff --git a/regression/cbmc-library/atexit-01/test.desc b/regression/cbmc-library/atexit-01/test.desc new file mode 100644 index 00000000000..4b9176a942e --- /dev/null +++ b/regression/cbmc-library/atexit-01/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check --bounds-check +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-library/atexit-02/main.c b/regression/cbmc-library/atexit-02/main.c new file mode 100644 index 00000000000..696dc20eed0 --- /dev/null +++ b/regression/cbmc-library/atexit-02/main.c @@ -0,0 +1,13 @@ +#include +#include + +void cleanup() +{ + assert(0); +} + +int main() +{ + atexit(cleanup); + exit(0); +} diff --git a/regression/cbmc-library/atexit-02/test.desc b/regression/cbmc-library/atexit-02/test.desc new file mode 100644 index 00000000000..4b9176a942e --- /dev/null +++ b/regression/cbmc-library/atexit-02/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check --bounds-check +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-library/free-01/test.desc b/regression/cbmc-library/free-01/test.desc index 769ba573e7c..a727d0817d0 100644 --- a/regression/cbmc-library/free-01/test.desc +++ b/regression/cbmc-library/free-01/test.desc @@ -1,7 +1,7 @@ CORE main.c --pointer-check --bounds-check --stop-on-fail -free argument must be NULL or valid pointer +free argument must be (NULL or valid pointer|dynamic object) ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-library/memcpy-06/test.desc b/regression/cbmc-library/memcpy-06/test.desc index ab649ecc026..c0abaeddc09 100644 --- a/regression/cbmc-library/memcpy-06/test.desc +++ b/regression/cbmc-library/memcpy-06/test.desc @@ -2,8 +2,8 @@ CORE main.c function 'memcpy' is not declared -parameter "memcpy::dst" type mismatch -^EXIT=6$ +Linking library function 'memcpy' failed +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/cbmc-library/memcpy-07/main.c b/regression/cbmc-library/memcpy-07/main.c index 06ad39e2b74..971509901fc 100644 --- a/regression/cbmc-library/memcpy-07/main.c +++ b/regression/cbmc-library/memcpy-07/main.c @@ -1,4 +1,5 @@ // #include intentionally omitted +void *memcpy(); struct c { diff --git a/regression/cbmc-library/posix_memalign-02/test.desc b/regression/cbmc-library/posix_memalign-02/test.desc index 648263292fe..8a67b803b89 100644 --- a/regression/cbmc-library/posix_memalign-02/test.desc +++ b/regression/cbmc-library/posix_memalign-02/test.desc @@ -6,5 +6,6 @@ main.c ^VERIFICATION FAILED$ \[main.precondition_instance.1\] .* memcpy src/dst overlap: FAILURE \[main.precondition_instance.3\] .* memcpy destination region writeable: FAILURE +\*\* 2 of 24 failed -- ^warning: ignoring diff --git a/regression/cbmc-library/pthread_cond_wait-01/test.desc b/regression/cbmc-library/pthread_cond_wait-01/test.desc index adbd7d687d0..2a2cb693e76 100644 --- a/regression/cbmc-library/pthread_cond_wait-01/test.desc +++ b/regression/cbmc-library/pthread_cond_wait-01/test.desc @@ -3,7 +3,7 @@ main.c --bounds-check ^EXIT=10$ ^SIGNAL=0$ -^\*\* 1 of 2 failed +^\*\* 1 of 4 failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc index 31b58b17b85..23f8cefebfe 100644 --- a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc +++ b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc @@ -4,7 +4,7 @@ main.i ^EXIT=10$ ^SIGNAL=0$ array\.List dynamic object upper bound in p->List\[2\]: FAILURE -\*\* 1 of 11 failed +\*\* 1 of 18 failed -- ^warning: ignoring -- diff --git a/regression/cbmc/String_Abstraction17/test.desc b/regression/cbmc/String_Abstraction17/test.desc index ea2896bae68..9e85c0c54ed 100644 --- a/regression/cbmc/String_Abstraction17/test.desc +++ b/regression/cbmc/String_Abstraction17/test.desc @@ -1,7 +1,7 @@ CORE strcpy-no-decl.c --string-abstraction --validate-goto-model -Condition: strlen type inconsistency +^Condition: fct_type.parameters\(\).size\(\) == parameter_identifiers.size\(\)$ ^EXIT=(127|134)$ ^SIGNAL=0$ -- diff --git a/regression/cbmc/array-cell-sensitivity2/test.desc b/regression/cbmc/array-cell-sensitivity2/test.desc index 65b734796e9..429cfbdd7fc 100644 --- a/regression/cbmc/array-cell-sensitivity2/test.desc +++ b/regression/cbmc/array-cell-sensitivity2/test.desc @@ -6,7 +6,7 @@ main::1::array!0@1#3 = with\(main::1::array!0@1#2, 1, main::argc!0@1#1\) ^EXIT=0$ ^SIGNAL=0$ -- -\[\[[0-9]+\]\] +array.*\[\[[0-9]+\]\] -- This checks that arrays of uncertain size are always treated as aggregates and are not expanded into individual cell symbols (which use the [[index]] notation diff --git a/regression/cbmc/array_constraints1/test.desc b/regression/cbmc/array_constraints1/test.desc index 8040e5651bf..d38dbc8f225 100644 --- a/regression/cbmc/array_constraints1/test.desc +++ b/regression/cbmc/array_constraints1/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -^\*\* 2 of 14 +^\*\* 2 of 24 -- ^warning: ignoring diff --git a/regression/cbmc/array_of_bool_as_bitvec/main.c b/regression/cbmc/array_of_bool_as_bitvec/main.c index 19888bb1a45..07106dde3d2 100644 --- a/regression/cbmc/array_of_bool_as_bitvec/main.c +++ b/regression/cbmc/array_of_bool_as_bitvec/main.c @@ -3,6 +3,7 @@ #include __CPROVER_bool w[8]; +__CPROVER_bool v[__CPROVER_constant_infinity_uint]; void main() { diff --git a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc index ae228a04e44..a7ede3fc945 100644 --- a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc +++ b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc @@ -1,15 +1,15 @@ CORE broken-smt-backend main.c --smt2 --outfile - -\(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\) -\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\) -\(= \(select array\.3 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\) +\(= \(select array_of\.0 i\) \(ite false #b1 #b0\)\) +\(= \(select array\.1 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\) +\(= \(select array\.1 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\) ^EXIT=0$ ^SIGNAL=0$ -- -\(= \(select array_of\.2 i\) false\) -\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\) -\(= \(select array\.3 \(_ bv\d+ 64\)\) false\) +\(= \(select array_of\.0 i\) false\) +\(= \(select array\.1 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\) +\(= \(select array\.1 \(_ bv\d+ 64\)\) false\) -- This test checks for correctness of BitVec-array encoding of Boolean arrays. diff --git a/regression/cbmc/destructor1/main.c b/regression/cbmc/destructor1/main.c new file mode 100644 index 00000000000..275e04de283 --- /dev/null +++ b/regression/cbmc/destructor1/main.c @@ -0,0 +1,17 @@ +#include + +#ifdef __GNUC__ +static __attribute__((destructor)) void assert_false(void) +{ + assert(0); +} +#endif + +int main() +{ +#ifndef __GNUC__ + // explicitly invoke assert_false as __attribute__((destructor)) isn't + // supported + assert_false(); +#endif +} diff --git a/regression/cbmc/destructor1/test.desc b/regression/cbmc/destructor1/test.desc new file mode 100644 index 00000000000..7a0fc8c72e1 --- /dev/null +++ b/regression/cbmc/destructor1/test.desc @@ -0,0 +1,9 @@ +CORE +main.c + +^\[assert_false.assertion.1\] line 7 assertion 0: FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/cbmc/memory_allocation2/test.desc b/regression/cbmc/memory_allocation2/test.desc index c88637311c2..aa85298ef8b 100644 --- a/regression/cbmc/memory_allocation2/test.desc +++ b/regression/cbmc/memory_allocation2/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^\[main\.array_bounds\.[1-5]\] .*: SUCCESS$ ^\[main\.array_bounds\.[67]\] line 38 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$ -^\*\* 1 of 6 failed +^\*\* 2 of 9 failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/multiple-goto-traces/test.desc b/regression/cbmc/multiple-goto-traces/test.desc index f5009b36556..46ea40d5c4b 100644 --- a/regression/cbmc/multiple-goto-traces/test.desc +++ b/regression/cbmc/multiple-goto-traces/test.desc @@ -5,7 +5,7 @@ activate-multi-line-match ^EXIT=10$ ^SIGNAL=0$ VERIFICATION FAILED -Trace for main\.assertion\.1:(\n.*){22} assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){36} assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){50} assertion argc \+ 1 != 5 +Trace for main\.assertion\.1:(\n.*){150} assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){164} assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){178} assertion argc \+ 1 != 5 \*\* 3 of 4 failed -- ^warning: ignoring diff --git a/regression/cbmc/pragma_cprover1/test.desc b/regression/cbmc/pragma_cprover1/test.desc index 2ed565c0062..3ea73ad9572 100644 --- a/regression/cbmc/pragma_cprover1/test.desc +++ b/regression/cbmc/pragma_cprover1/test.desc @@ -2,7 +2,7 @@ CORE main.c --signed-overflow-check --bounds-check line 14 array 'y' upper bound in y\[\(signed long( long)? int\)1\]: FAILURE$ -^\*\* 1 of 1 failed +^\*\* 1 of 4 failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/pragma_cprover2/test.desc b/regression/cbmc/pragma_cprover2/test.desc index fc1f888dfcf..249a0cae2c6 100644 --- a/regression/cbmc/pragma_cprover2/test.desc +++ b/regression/cbmc/pragma_cprover2/test.desc @@ -3,7 +3,7 @@ main.c --signed-overflow-check ^\[main.overflow\.1\] line 21 arithmetic overflow on signed \+ in n \+ n: FAILURE$ ^\[main.overflow\.2\] line 22 arithmetic overflow on signed \+ in x \+ n: FAILURE$ -^\*\* 2 of 2 failed +^\*\* 2 of 3 failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/switch8/test.desc b/regression/cbmc/switch8/test.desc index 62e8b9730ae..5b963c0786f 100644 --- a/regression/cbmc/switch8/test.desc +++ b/regression/cbmc/switch8/test.desc @@ -13,7 +13,7 @@ main.c ^\[main\.pointer_dereference\.4\] line 42 dereference failure: dead object in \*p: FAILURE$ ^\[main\.assertion\.4\] line 49 assertion e == 42: FAILURE$ ^\[main\.assertion\.5\] line 51 assertion f == 42: FAILURE$ -^\*\* 4 of 10 failed +^\*\* 4 of 18 failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/union12/test.desc b/regression/cbmc/union12/test.desc index 6b04b86af6e..64dc24e15f6 100644 --- a/regression/cbmc/union12/test.desc +++ b/regression/cbmc/union12/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[main\.assertion\.2\] line 20 should fail: FAILURE$ -^\*\* 1 of 15 failed +^\*\* 1 of 25 failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_01/test-vsd.desc b/regression/goto-analyzer/constant_propagation_01/test-vsd.desc index 8eb05ff4f8d..741965ab2a5 100644 --- a/regression/goto-analyzer/constant_propagation_01/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_01/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc index 47aea19e28b..e0147b4ce18 100644 --- a/regression/goto-analyzer/constant_propagation_01/test.desc +++ b/regression/goto-analyzer/constant_propagation_01/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_02/test-vsd.desc b/regression/goto-analyzer/constant_propagation_02/test-vsd.desc index 89bcfe85984..db447649547 100644 --- a/regression/goto-analyzer/constant_propagation_02/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_02/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc index 0cc5f61bb73..f8465991235 100644 --- a/regression/goto-analyzer/constant_propagation_02/test.desc +++ b/regression/goto-analyzer/constant_propagation_02/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_03/test-vsd.desc b/regression/goto-analyzer/constant_propagation_03/test-vsd.desc index 89bcfe85984..db447649547 100644 --- a/regression/goto-analyzer/constant_propagation_03/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_03/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc index 0cc5f61bb73..f8465991235 100644 --- a/regression/goto-analyzer/constant_propagation_03/test.desc +++ b/regression/goto-analyzer/constant_propagation_03/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_04/test-vsd.desc b/regression/goto-analyzer/constant_propagation_04/test-vsd.desc index 89bcfe85984..db447649547 100644 --- a/regression/goto-analyzer/constant_propagation_04/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_04/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc index 0cc5f61bb73..f8465991235 100644 --- a/regression/goto-analyzer/constant_propagation_04/test.desc +++ b/regression/goto-analyzer/constant_propagation_04/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/test-vsd.desc b/regression/goto-analyzer/constant_propagation_07/test-vsd.desc index d4c16c2278f..14364a509af 100644 --- a/regression/goto-analyzer/constant_propagation_07/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_07/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 3, assigns: 9, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc index 22058dcb77e..3b836b8dad2 100644 --- a/regression/goto-analyzer/constant_propagation_07/test.desc +++ b/regression/goto-analyzer/constant_propagation_07/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 3, assigns: 9, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_08/test-vsd.desc b/regression/goto-analyzer/constant_propagation_08/test-vsd.desc index ccd63713bc4..bd028bcc6c5 100644 --- a/regression/goto-analyzer/constant_propagation_08/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_08/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-arrays every-element --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 2, assigns: 8, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 3, assigns: 14, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 2, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 3, assigns: 9, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_11/test-vsd.desc b/regression/goto-analyzer/constant_propagation_11/test-vsd.desc index 8d26811ac53..90e1b48f887 100644 --- a/regression/goto-analyzer/constant_propagation_11/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_11/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-arrays every-element --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 6, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc index e63b5b8a837..bba19b94b66 100644 --- a/regression/goto-analyzer/constant_propagation_11/test.desc +++ b/regression/goto-analyzer/constant_propagation_11/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 6, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_12/test-vsd.desc b/regression/goto-analyzer/constant_propagation_12/test-vsd.desc index bcc8b541c93..e8b6c2d034f 100644 --- a/regression/goto-analyzer/constant_propagation_12/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_12/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 7, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc index 79fcdf4a79b..614698c7277 100644 --- a/regression/goto-analyzer/constant_propagation_12/test.desc +++ b/regression/goto-analyzer/constant_propagation_12/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 7, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc b/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc index 2a8b2b0aa11..c1501370247 100644 --- a/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc +++ b/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc @@ -3,8 +3,8 @@ main.c --variable-sensitivity --vsd-liveness --show ^EXIT=0$ ^SIGNAL=0$ -globalX .* 0 @ \[25\] +globalX .* 0 @ \[15\] globalX .* 1 @ \[0\] globalX .* 2 @ \[3\] -globalX .* TOP @ \[28\] +globalX .* TOP @ \[18\] -- diff --git a/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc b/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc index dd242a3a3e6..2c13d44ae4b 100644 --- a/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc +++ b/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc @@ -3,8 +3,8 @@ main.c --variable-sensitivity --vsd-liveness --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -globalX .* 0 @ \[25\] +globalX .* 0 @ \[15\] globalX .* 1 @ \[0\] globalX .* 2 @ \[3\] -globalX .* TOP @ \[28\] +globalX .* TOP @ \[18\] -- diff --git a/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc b/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc index 8de3a82a5ef..f3fd23e0665 100644 --- a/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc +++ b/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --show ^EXIT=0$ ^SIGNAL=0$ -globalX .* 0 @ \[25\] +globalX .* 0 @ \[15\] globalX .* 1 @ \[0\] globalX .* TOP @ \[0, 3\] -- diff --git a/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc b/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc index c8daf2ef143..242a87dda34 100644 --- a/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc +++ b/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -globalX .* 0 @ \[25\] +globalX .* 0 @ \[15\] globalX .* 1 @ \[0\] globalX .* 2 @ \[3\] -- diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc index 92cff667e02..19398dce8fb 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc @@ -6,32 +6,26 @@ activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ main#return_value \(\) -> TOP @ \[1\] -__CPROVER_dead_object \(\) -> TOP @ \[5\] -__CPROVER_deallocated \(\) -> TOP @ \[6\] -__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\] -__CPROVER_memory_leak \(\) -> TOP @ \[9\] -__CPROVER_new_object \(\) -> TOP @ \[10\] -__CPROVER_next_thread_key \(\) -> 0ul @ \[12\] -__CPROVER_pipe_count \(\) -> 0u @ \[13\] -__CPROVER_rounding_mode \(\) -> 0 @ \[14\] -__CPROVER_thread_id \(\) -> 0ul @ \[15\] -__CPROVER_threads_exited \(\) -> TOP @ \[18\] -do_arrays::1::bool_ \(\) -> TOP @ \[20\] -do_arrays::1::bool_1 \(\) -> TOP @ \[21\] -do_arrays::1::bool_2 \(\) -> TOP @ \[22\] -do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[24\]\n\} @ \[24\] -do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[24\]\n\[1\] = 20 @ \[25\]\n\} @ \[25\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[26\]\n\[1\] = 20 @ \[25\]\n\} @ \[26\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[26\]\n\[1\] = 40 @ \[27\]\n\} @ \[27\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[26\]\n\[1\] = 30 @ \[28\]\n\} @ \[28\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[29\]\n\[1\] = 30 @ \[28\]\n\} @ \[29\] -do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[30\]\n\[1\] = 30 @ \[28\]\n\} @ \[30\] -do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[31\]\n\[1\] = 30 @ \[28\]\n\} @ \[31\] -do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[31\]\n\[1\] = 10 @ \[32\]\n\} @ \[32\] -do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[34\]\n\[1\] = 10 @ \[32\]\n\} @ \[34\] -do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[34\, 36\]\n\[1\] = 10 @ \[32\]\n\} @ \[34\, 36\] -do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[38]\n\[1\] = 10 @ \[32\]\n\} @ \[38\] -do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[40]\n\[1\] = 10 @ \[32\]\n\} @ \[40\] -do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[40\, 42]\n\[1\] = 10 @ \[32\]\n\} @ \[40\, 42\] -do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[40\, 42\, 45]\n\[1\] = 10 @ \[47\]\n\} @ \[47\] -do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[48]\n\[1\] = 10 @ \[47\]\n\} @ \[48\] +__CPROVER_dead_object \(\) -> TOP @ \[4\] +__CPROVER_deallocated \(\) -> TOP @ \[5\] +__CPROVER_memory_leak \(\) -> TOP @ \[7\] +__CPROVER_rounding_mode \(\) -> 0 @ \[8\] +do_arrays::1::bool_ \(\) -> TOP @ \[10\] +do_arrays::1::bool_1 \(\) -> TOP @ \[11\] +do_arrays::1::bool_2 \(\) -> TOP @ \[12\] +do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[14\]\n\} @ \[14\] +do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[14\]\n\[1\] = 20 @ \[15\]\n\} @ \[15\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 20 @ \[15\]\n\} @ \[16\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 40 @ \[17\]\n\} @ \[17\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 30 @ \[18\]\n\} @ \[18\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[19\]\n\[1\] = 30 @ \[18\]\n\} @ \[19\] +do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[20\]\n\[1\] = 30 @ \[18\]\n\} @ \[20\] +do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[21\]\n\[1\] = 30 @ \[18\]\n\} @ \[21\] +do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[21\]\n\[1\] = 10 @ \[22\]\n\} @ \[22\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[24\]\n\[1\] = 10 @ \[22\]\n\} @ \[24\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[24\, 26\]\n\[1\] = 10 @ \[22\]\n\} @ \[24\, 26\] +do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[28]\n\[1\] = 10 @ \[22\]\n\} @ \[28\] +do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[30]\n\[1\] = 10 @ \[22\]\n\} @ \[30\] +do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[30\, 32]\n\[1\] = 10 @ \[22\]\n\} @ \[30\, 32\] +do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[30\, 32\, 35]\n\[1\] = 10 @ \[37\]\n\} @ \[37\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[38]\n\[1\] = 10 @ \[37\]\n\} @ \[38\] diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc index bf14f6154f4..94a6ad7e383 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc @@ -6,31 +6,25 @@ activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ main#return_value \(\) -> TOP @ \[1\] -__CPROVER_dead_object \(\) -> TOP @ \[5\] -__CPROVER_deallocated \(\) -> TOP @ \[6\] -__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\] -__CPROVER_memory_leak \(\) -> TOP @ \[9\] -__CPROVER_new_object \(\) -> TOP @ \[10\] -__CPROVER_next_thread_key \(\) -> 0ul @ \[12\] -__CPROVER_pipe_count \(\) -> 0u @ \[13\] -__CPROVER_rounding_mode \(\) -> 0 @ \[14\] -__CPROVER_thread_id \(\) -> 0ul @ \[15\] -__CPROVER_threads_exited \(\) -> TOP @ \[18\] -do_pointers::1::bool_ \(\) -> TOP @ \[20\] -do_pointers::1::bool_1 \(\) -> TOP @ \[21\] -do_pointers::1::bool_2 \(\) -> TOP @ \[22\] -do_pointers::1::x \(\) -> TOP @ \[23\] -do_pointers::1::x \(\) -> 10 @ \[24\] -do_pointers::1::x_p \(\) -> TOP @ \[25\] -do_pointers::1::y \(\) -> TOP @ \[26\] -do_pointers::1::y \(\) -> 20 @ \[27\] -do_pointers::1::y_p \(\) -> TOP @ \[28\] -do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[29\] -do_pointers::1::x \(\) -> 30 @ \[30\] -do_pointers::1::x \(\) -> 40 @ \[31\] -do_pointers::1::x \(\) -> TOP @ \[32\] -do_pointers::1::x \(\) -> 50 @ \[33\] -do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[34\] -do_pointers::1::x \(\) -> 60 @ \[35\] -do_pointers::1::j \(\) -> TOP @ \[36\] -do_pointers::1::j \(\) -> 60 @ \[37\] +__CPROVER_dead_object \(\) -> TOP @ \[4\] +__CPROVER_deallocated \(\) -> TOP @ \[5\] +__CPROVER_memory_leak \(\) -> TOP @ \[7\] +__CPROVER_rounding_mode \(\) -> 0 @ \[8\] +do_pointers::1::bool_ \(\) -> TOP @ \[10\] +do_pointers::1::bool_1 \(\) -> TOP @ \[11\] +do_pointers::1::bool_2 \(\) -> TOP @ \[12\] +do_pointers::1::x \(\) -> TOP @ \[13\] +do_pointers::1::x \(\) -> 10 @ \[14\] +do_pointers::1::x_p \(\) -> TOP @ \[15\] +do_pointers::1::y \(\) -> TOP @ \[16\] +do_pointers::1::y \(\) -> 20 @ \[17\] +do_pointers::1::y_p \(\) -> TOP @ \[18\] +do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[19\] +do_pointers::1::x \(\) -> 30 @ \[20\] +do_pointers::1::x \(\) -> 40 @ \[21\] +do_pointers::1::x \(\) -> TOP @ \[22\] +do_pointers::1::x \(\) -> 50 @ \[23\] +do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[24\] +do_pointers::1::x \(\) -> 60 @ \[25\] +do_pointers::1::j \(\) -> TOP @ \[26\] +do_pointers::1::j \(\) -> 60 @ \[27\] diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc index 9b63fdf295e..c74416efa88 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc @@ -6,37 +6,31 @@ activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ main#return_value \(\) -> TOP @ \[1\] -__CPROVER_dead_object \(\) -> TOP @ \[5\] -__CPROVER_deallocated \(\) -> TOP @ \[6\] -__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\] -__CPROVER_memory_leak \(\) -> TOP @ \[9\] -__CPROVER_new_object \(\) -> TOP @ \[10\] -__CPROVER_next_thread_key \(\) -> 0ul @ \[12\] -__CPROVER_pipe_count \(\) -> 0u @ \[13\] -__CPROVER_rounding_mode \(\) -> 0 @ \[14\] -__CPROVER_thread_id \(\) -> 0ul @ \[15\] -__CPROVER_threads_exited \(\) -> TOP @ \[18\] -do_structs::1::bool_ \(\) -> TOP @ \[20\] -do_structs::1::bool_1 \(\) -> TOP @ \[21\] -do_structs::1::bool_2 \(\) -> TOP @ \[22\] -do_structs::1::st \(\) -> \{\} @ \[23\] -do_structs::1::st \(\) -> \{.x=10 @ \[24\]\} @ \[24\] -do_structs::1::st \(\) -> \{.x=10 @ \[24\]\, .y=20 @ \[25\]\} @ \[25\] -do_structs::1::st \(\) -> \{.x=30 @ \[26\]\, .y=20 @ \[25\]\} @ \[26\] -do_structs::1::st \(\) -> \{.x=30 @ \[26\]\, .y=40 @ \[27\]\} @ \[27\] -do_structs::1::st \(\) -> \{.x=30 @ \[26\]\, .y=30 @ \[28\]\} @ \[28\] -do_structs::1::st \(\) -> \{.x=30 @ \[29\]\, .y=30 @ \[28\]\} @ \[29\] -do_structs::1::st \(\) -> \{.x=5 @ \[30\]\, .y=30 @ \[28\]\} @ \[30\] -do_structs::1::st \(\) -> \{.x=15 @ \[31\]\, .y=30 @ \[28\]\} @ \[31\] -do_structs::1::st \(\) -> \{.x=15 @ \[31\]\, .y=10 @ \[32\]\} @ \[32\] -do_structs::1::st \(\) -> \{.x=20 @ \[34\]\, .y=10 @ \[32\]\} @ \[34\] -do_structs::1::st \(\) -> \{.x=20 @ \[34\, 36\]\, .y=10 @ \[32\]\} @ \[34\, 36\] -do_structs::1::st \(\) -> \{.x=0 @ \[38\]\, .y=10 @ \[32\]\} @ \[38\] -do_structs::1::st \(\) -> \{.x=3 @ \[40\]\, .y=10 @ \[32\]\} @ \[40\] -do_structs::1::st \(\) -> \{.x=TOP @ \[40\, 42\]\, .y=10 @ \[32\]\} @ \[40\, 42\] -do_structs::1::st \(\) -> \{.x=TOP @ \[40\, 42\, 45\]\, .y=10 @ \[32\]\} @ \[40\, 42\, 45\] -do_structs::1::st \(\) -> \{.x=TOP @ \[40\, 42\, 45\]\, .y=10 @ \[47\]\} @ \[47\] -do_structs::1::st \(\) -> \{.x=20 @ \[48\]\, .y=10 @ \[47\]\} @ \[48\] -do_structs::1::new_age \(\) -> \{\} @ \[49\] -do_structs::1::new_age \(\) -> \{.x=20 @ \[50\]\, .y=10 @ \[50\]\} @ \[50\] +__CPROVER_dead_object \(\) -> TOP @ \[4\] +__CPROVER_deallocated \(\) -> TOP @ \[5\] +__CPROVER_memory_leak \(\) -> TOP @ \[7\] +__CPROVER_rounding_mode \(\) -> 0 @ \[8\] +do_structs::1::bool_ \(\) -> TOP @ \[10\] +do_structs::1::bool_1 \(\) -> TOP @ \[11\] +do_structs::1::bool_2 \(\) -> TOP @ \[12\] +do_structs::1::st \(\) -> \{\} @ \[13\] +do_structs::1::st \(\) -> \{.x=10 @ \[14\]\} @ \[14\] +do_structs::1::st \(\) -> \{.x=10 @ \[14\]\, .y=20 @ \[15\]\} @ \[15\] +do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=20 @ \[15\]\} @ \[16\] +do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=40 @ \[17\]\} @ \[17\] +do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=30 @ \[18\]\} @ \[18\] +do_structs::1::st \(\) -> \{.x=30 @ \[19\]\, .y=30 @ \[18\]\} @ \[19\] +do_structs::1::st \(\) -> \{.x=5 @ \[20\]\, .y=30 @ \[18\]\} @ \[20\] +do_structs::1::st \(\) -> \{.x=15 @ \[21\]\, .y=30 @ \[18\]\} @ \[21\] +do_structs::1::st \(\) -> \{.x=15 @ \[21\]\, .y=10 @ \[22\]\} @ \[22\] +do_structs::1::st \(\) -> \{.x=20 @ \[24\]\, .y=10 @ \[22\]\} @ \[24\] +do_structs::1::st \(\) -> \{.x=20 @ \[24\, 26\]\, .y=10 @ \[22\]\} @ \[24\, 26\] +do_structs::1::st \(\) -> \{.x=0 @ \[28\]\, .y=10 @ \[22\]\} @ \[28\] +do_structs::1::st \(\) -> \{.x=3 @ \[30\]\, .y=10 @ \[22\]\} @ \[30\] +do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\]\, .y=10 @ \[22\]\} @ \[30\, 32\] +do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\, 35\]\, .y=10 @ \[22\]\} @ \[30\, 32\, 35\] +do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\, 35\]\, .y=10 @ \[37\]\} @ \[37\] +do_structs::1::st \(\) -> \{.x=20 @ \[38\]\, .y=10 @ \[37\]\} @ \[38\] +do_structs::1::new_age \(\) -> \{\} @ \[39\] +do_structs::1::new_age \(\) -> \{.x=20 @ \[40\]\, .y=10 @ \[40\]\} @ \[40\] -- diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc index 37eb13074fc..ccb6a2526dc 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc @@ -4,42 +4,35 @@ sensitivity_dependency_variables.c ^EXIT=0$ ^SIGNAL=0$ main#return_value \(\) -> TOP @ \[1\] -__CPROVER_alloca_object \(\) -> TOP @ \[4\] -__CPROVER_dead_object \(\) -> TOP @ \[5\] -__CPROVER_deallocated \(\) -> TOP @ \[6\] -__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\] -__CPROVER_memory_leak \(\) -> TOP @ \[9\] -__CPROVER_new_object \(\) -> TOP @ \[10\] -__CPROVER_next_thread_key \(\) -> 0ul @ \[12\] -__CPROVER_pipe_count \(\) -> 0u @ \[13\] -__CPROVER_rounding_mode \(\) -> 0 @ \[14\] -__CPROVER_thread_id \(\) -> 0ul @ \[15\] -__CPROVER_threads_exited \(\) -> TOP @ \[18\] -global_x \(\) -> 0 @ \[19\] -do_variables::1::bool_ \(\) -> TOP @ \[21\] -do_variables::1::bool_1 \(\) -> TOP @ \[22\] -do_variables::1::bool_2 \(\) -> TOP @ \[23\] -global_x \(\) -> 5 @ \[24\] -do_variables::1::x \(\) -> TOP @ \[25\] -do_variables::1::x \(\) -> 10 @ \[26\] -do_variables::1::y \(\) -> TOP @ \[27\] -do_variables::1::y \(\) -> 20 @ \[28\] -do_variables::1::x \(\) -> 30 @ \[29\] -do_variables::1::y \(\) -> 40 @ \[30\] -do_variables::1::y \(\) -> 30 @ \[31\] -do_variables::1::x \(\) -> 30 @ \[32\] -do_variables::1::x \(\) -> 5 @ \[33\] -do_variables::1::x \(\) -> 15 @ \[34\] -do_variables::1::y \(\) -> 10 @ \[35\] -do_variables::1::x \(\) -> 20 @ \[37\] -do_variables::1::x \(\) -> 20 @ \[37\, 39\] -do_variables::1::x \(\) -> 50 @ \[41\] -do_variables::1::x \(\) -> 20 @ \[43\] -do_variables::1::x \(\) -> TOP @ \[43\, 45\] -do_variables::1::x \(\) -> 0 @ \[47\] -do_variables::1::x \(\) -> 3 @ \[49\] -do_variables::1::x \(\) -> TOP @ \[49\, 51\] -do_variables::1::x \(\) -> TOP @ \[49\, 51\, 54\] -do_variables::1::y \(\) -> 10 @ \[56\] -do_variables::1::x \(\) -> 20 @ \[57\] +__CPROVER_dead_object \(\) -> TOP @ \[4\] +__CPROVER_deallocated \(\) -> TOP @ \[5\] +__CPROVER_memory_leak \(\) -> TOP @ \[7\] +__CPROVER_rounding_mode \(\) -> 0 @ \[8\] +global_x \(\) -> 0 @ \[9\] +do_variables::1::bool_ \(\) -> TOP @ \[11\] +do_variables::1::bool_1 \(\) -> TOP @ \[12\] +do_variables::1::bool_2 \(\) -> TOP @ \[13\] +global_x \(\) -> 5 @ \[14\] +do_variables::1::x \(\) -> TOP @ \[15\] +do_variables::1::x \(\) -> 10 @ \[16\] +do_variables::1::y \(\) -> TOP @ \[17\] +do_variables::1::y \(\) -> 20 @ \[18\] +do_variables::1::x \(\) -> 30 @ \[19\] +do_variables::1::y \(\) -> 40 @ \[20\] +do_variables::1::y \(\) -> 30 @ \[21\] +do_variables::1::x \(\) -> 30 @ \[22\] +do_variables::1::x \(\) -> 5 @ \[23\] +do_variables::1::x \(\) -> 15 @ \[24\] +do_variables::1::y \(\) -> 10 @ \[25\] +do_variables::1::x \(\) -> 20 @ \[27\] +do_variables::1::x \(\) -> 20 @ \[27\, 29\] +do_variables::1::x \(\) -> 50 @ \[31\] +do_variables::1::x \(\) -> 20 @ \[33\] +do_variables::1::x \(\) -> TOP @ \[33\, 35\] +do_variables::1::x \(\) -> 0 @ \[37\] +do_variables::1::x \(\) -> 3 @ \[39\] +do_variables::1::x \(\) -> TOP @ \[39\, 41\] +do_variables::1::x \(\) -> TOP @ \[39\, 41\, 44\] +do_variables::1::y \(\) -> 10 @ \[46\] +do_variables::1::x \(\) -> 20 @ \[47\] -- diff --git a/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc b/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc index e070c053f6f..a87879274f8 100644 --- a/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc +++ b/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc @@ -5,8 +5,8 @@ data-dependency-context.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -st \(\) -> \{.a=.* @ \[2, 52\]\[Data dependencies: 52, 2\]\[Data dominators: \], .b=.* @ \[5, 52\]\[Data dependencies: 52, 5\]\[Data dominators: \]\} @ \[2, 5, 52\]\[Data dependencies: 52, 5, 2\]\[Data dominators: 52\] -ar \(\) -> \{\[0\] = TOP @ \[11\, 46\]\[Data dependencies: 46\, 11\]\[Data dominators: \]\n\[1\] = TOP @ \[14\, 46\]\[Data dependencies: 46\, 14\]\[Data dominators: \]\n\} @ \[11\, 14\, 46\]\[Data dependencies: 46\, 14\, 11\]\[Data dominators: 46\] -arr \(\) -> \{\[0\] = 1 @ \[19\]\[Data dependencies: 19\]\[Data dominators: 19\]\n\[1\] = 2 @ \[20\]\[Data dependencies: 20\]\[Data dominators: 20\]\n\[2\] = TOP @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: \]\n\} @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: 47\] +st \(\) -> \{.a=.* @ \[2, 42\]\[Data dependencies: 42, 2\]\[Data dominators: \], .b=.* @ \[5, 42\]\[Data dependencies: 42, 5\]\[Data dominators: \]\} @ \[2, 5, 42\]\[Data dependencies: 42, 5, 2\]\[Data dominators: 42\] +ar \(\) -> \{\[0\] = TOP @ \[11\, 36\]\[Data dependencies: 36\, 11\]\[Data dominators: \]\n\[1\] = TOP @ \[14\, 36\]\[Data dependencies: 36\, 14\]\[Data dominators: \]\n\} @ \[11\, 14\, 36\]\[Data dependencies: 36\, 14\, 11\]\[Data dominators: 36\] +arr \(\) -> \{\[0\] = 1 @ \[19\]\[Data dependencies: 19\]\[Data dominators: 19\]\n\[1\] = 2 @ \[20\]\[Data dependencies: 20\]\[Data dominators: 20\]\n\[2\] = TOP @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: \]\n\} @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: 37\] -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc index 1bd4f4ec3b5..cd3a57851d6 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc @@ -3,24 +3,24 @@ main.c file1.c file2.c --dependence-graph-vs --vsd-structs every-field --vsd-arrays every-element --show ^EXIT=0$ ^SIGNAL=0$ -^Data dependencies: 58 \[st.a\]$ -^Data dependencies: 58 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 58 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 58 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 58 \[st.a, st.b\]$ -^Data dependencies: 52 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 52 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 52 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$ +^Data dependencies: 48 \[st.a\]$ +^Data dependencies: 48 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 48 \[st.a\]$ +^Data dependencies: 4 \[st.b\], 48 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\]$ +^Data dependencies: 42 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 42 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 42 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$ ^Data dependencies: 19 \[arr\[\([^)]*\)1\]\]$ ^Data dependencies: 18 \[arr\[\([^)]*\)0\]\]$ ^Data dependencies: 20 \[arr\[\([^)]*\)2\]\], 22 \[arr\[\([^)]*\)2\]\]$ -^Data dependencies: 1 \[st.a\], 58 \[st.a\], 62 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 58 \[st.b\], 65 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 58 \[st.a, st.b\], 62 \[st.a\], 65 \[st.b\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 52 \[ar\[\([^)]*\)0\]\], 73 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)1\]\], 76 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 73 \[ar\[\([^)]*\)0\]\], 76 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 1 \[st.a\], 48 \[st.a\], 52 \[st.a\]$ +^Data dependencies: 4 \[st.b\], 48 \[st.b\], 55 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\], 52 \[st.a\], 55 \[st.b\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 42 \[ar\[\([^)]*\)0\]\], 63 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)1\]\], 66 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 63 \[ar\[\([^)]*\)0\]\], 66 \[ar\[\([^)]*\)1\]\]$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc index a87e2b7a739..8abe0ffdcec 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc @@ -3,25 +3,25 @@ main.c file1.c file2.c --dependence-graph-vs --vsd-structs every-field --vsd-arrays every-element --show ^EXIT=0$ ^SIGNAL=0$ -^Data dependencies: 58 \[st.a\]$ -^Data dependencies: 58 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 58 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 58 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 58 \[st.a, st.b\]$ -^Data dependencies: 52 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 48 \[st.a\]$ +^Data dependencies: 48 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 48 \[st.a\]$ +^Data dependencies: 4 \[st.b\], 48 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\]$ +^Data dependencies: 42 \[ar\[\([^)]*\)0\]\]$ ^Data dependencies: 6 \[out1\]$ -^Data dependencies: 52 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 52 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$ +^Data dependencies: 42 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 42 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$ ^Data dependencies: 19 \[arr\[\([^)]*\)1\]\]$ ^Data dependencies: 18 \[arr\[\([^)]*\)0\]\]$ ^Data dependencies: 20 \[arr\[\([^)]*\)2\]\], 22 \[arr\[\([^)]*\)2\]\]$ -^Data dependencies: 1 \[st.a\], 58 \[st.a\], 62 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 58 \[st.b\], 65 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 58 \[st.a, st.b\], 62 \[st.a\], 65 \[st.b\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 52 \[ar\[\([^)]*\)0\]\], 73 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)1\]\], 76 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 73 \[ar\[\([^)]*\)0\]\], 76 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 1 \[st.a\], 48 \[st.a\], 52 \[st.a\]$ +^Data dependencies: 4 \[st.b\], 48 \[st.b\], 55 \[st.b\]$ +^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\], 52 \[st.a\], 55 \[st.b\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 42 \[ar\[\([^)]*\)0\]\], 63 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)1\]\], 66 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 63 \[ar\[\([^)]*\)0\]\], 66 \[ar\[\([^)]*\)1\]\]$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc index fc1a4eff163..8bae062cd04 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc @@ -4,5 +4,5 @@ main.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -\*\*\*\* 9 file .*main\.c line 22 function main\nControl dependencies: 34 \[UNCONDITIONAL\]\nData dependencies: 1 \[g_a\[\([^)]*\)i\]\], 2 \[g_a\[\([^)]*\)i\]\], 3 \[g_a\[\([^)]*\)i\]\], 7 \[g_a\[\([^)]*\)i\]\] +\*\*\*\* 9 file .*main\.c line 22 function main\nControl dependencies: 24 \[UNCONDITIONAL\]\nData dependencies: 1 \[g_a\[\([^)]*\)i\]\], 2 \[g_a\[\([^)]*\)i\]\], 3 \[g_a\[\([^)]*\)i\]\], 7 \[g_a\[\([^)]*\)i\]\] -- diff --git a/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c b/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c index 1c080c84ccd..ffe6ec1418d 100644 --- a/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c +++ b/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c @@ -1,3 +1,5 @@ +#include + // This file is highly reduced from some open source projects. // The following four lines are adapted from the openssl library // Full repository here: diff --git a/src/analyses/goto_check_c.cpp b/src/analyses/goto_check_c.cpp index dff22d10b3d..43e95c28aaa 100644 --- a/src/analyses/goto_check_c.cpp +++ b/src/analyses/goto_check_c.cpp @@ -2213,6 +2213,28 @@ void goto_check_ct::goto_check( i.turn_into_skip(); did_something = true; } + + if(enable_memory_leak_check && function_identifier == "exit") + { + const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak"); + const symbol_exprt leak_expr = leak.symbol_expr(); + + // add self-assignment to get helpful counterexample output + new_code.add(goto_programt::make_assignment(leak_expr, leak_expr)); + + source_locationt source_location; + source_location.set_function(function_identifier); + + equal_exprt eq( + leak_expr, null_pointer_exprt(to_pointer_type(leak.type))); + add_guarded_property( + eq, + "dynamically allocated memory never freed", + "memory-leak", + source_location, + eq, + identity); + } } else if(i.is_dead()) { @@ -2262,29 +2284,6 @@ void goto_check_ct::goto_check( } else if(i.is_end_function()) { - if( - function_identifier == goto_functionst::entry_point() && - enable_memory_leak_check) - { - const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak"); - const symbol_exprt leak_expr = leak.symbol_expr(); - - // add self-assignment to get helpful counterexample output - new_code.add(goto_programt::make_assignment(leak_expr, leak_expr)); - - source_locationt source_location; - source_location.set_function(function_identifier); - - equal_exprt eq( - leak_expr, null_pointer_exprt(to_pointer_type(leak.type))); - add_guarded_property( - eq, - "dynamically allocated memory never freed", - "memory-leak", - source_location, - eq, - identity); - } } for(auto &instruction : new_code.instructions) diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 41f134b6f1b..1f520ab1fd3 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -242,6 +242,8 @@ bool generate_ansi_c_start_function( const code_typet::parameterst ¶meters= to_code_type(symbol.type).parameters(); + const namespacet ns(symbol_table); + if(symbol.name==ID_main) { if(parameters.empty()) @@ -250,8 +252,6 @@ bool generate_ansi_c_start_function( } else if(parameters.size()==2 || parameters.size()==3) { - namespacet ns(symbol_table); - { symbolt argc_symbol; @@ -498,12 +498,47 @@ bool generate_ansi_c_start_function( parameters, init_code, symbol_table, object_factory_parameters); } + exprt return_value = call_main.lhs(); init_code.add(std::move(call_main)); + const symbolt &exit_symbol = ns.lookup("exit"); + const typet &arg_type = to_code_type(exit_symbol.type).parameters()[0].type(); + code_function_callt call_exit{exit_symbol.symbol_expr()}; + if(return_value.is_not_nil()) + { + call_exit.arguments().push_back( + typecast_exprt::conditional_cast(return_value, arg_type)); + } + else + call_exit.arguments().push_back(from_integer(0, arg_type)); + call_exit.add_source_location() = symbol.location; + call_exit.function().add_source_location() = symbol.location; + init_code.add(std::move(call_exit)); + // TODO: add read/modified (recursively in call graph) globals as INPUT/OUTPUT record_function_outputs(symbol, init_code, symbol_table); + // now call destructor functions (a GCC extension) + + for(const auto &symbol_table_entry : symbol_table.symbols) + { + const symbolt &symbol = symbol_table_entry.second; + + if(symbol.type.id() != ID_code) + continue; + + const code_typet &code_type = to_code_type(symbol.type); + if( + code_type.return_type().id() == ID_destructor && + code_type.parameters().empty()) + { + code_function_callt function_call(symbol.symbol_expr()); + function_call.add_source_location() = symbol.location; + init_code.add(std::move(function_call)); + } + } + // add the entry point symbol symbolt new_symbol; diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 1c39cb67b5c..1e75d51c01f 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -157,28 +157,15 @@ void ansi_c_internal_additions(std::string &code) "const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n" "typedef void " CPROVER_PREFIX "integer;\n" "typedef void " CPROVER_PREFIX "rational;\n" - CPROVER_PREFIX "thread_local unsigned long " CPROVER_PREFIX "thread_id=0;\n" - CPROVER_PREFIX "bool " CPROVER_PREFIX "threads_exited[" - CPROVER_PREFIX "constant_infinity_uint];\n" - "unsigned long " CPROVER_PREFIX "next_thread_id=0;\n" - CPROVER_PREFIX "thread_local const void* " CPROVER_PREFIX "thread_keys[" - CPROVER_PREFIX "constant_infinity_uint];\n" - CPROVER_PREFIX "thread_local void (*" CPROVER_PREFIX "thread_key_dtors[" - CPROVER_PREFIX "constant_infinity_uint])(void *);\n" - CPROVER_PREFIX "thread_local unsigned long " - CPROVER_PREFIX "next_thread_key = 0;\n" "extern unsigned char " CPROVER_PREFIX "memory[" CPROVER_PREFIX "constant_infinity_uint];\n" // malloc "const void *" CPROVER_PREFIX "deallocated=0;\n" "const void *" CPROVER_PREFIX "dead_object=0;\n" - "const void *" CPROVER_PREFIX "new_object=0;\n" // for C++ - CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=0;\n" // for C++ "const void *" CPROVER_PREFIX "memory_leak=0;\n" "void *" CPROVER_PREFIX "allocate(" CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n" - "const void *" CPROVER_PREFIX "alloca_object = 0;\n" CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+ integer2string(max_malloc_size(config.ansi_c.pointer_width, config @@ -199,6 +186,9 @@ void ansi_c_internal_additions(std::string &code) id2string(rounding_mode_identifier()) + '='+ std::to_string(config.ansi_c.rounding_mode)+";\n" + // atexit + "void exit(int);\n" + // pipes, write, read, close "struct " CPROVER_PREFIX "pipet {\n" " _Bool widowed;\n" @@ -206,11 +196,6 @@ void ansi_c_internal_additions(std::string &code) " short next_avail;\n" " short next_unread;\n" "};\n" - "extern struct " CPROVER_PREFIX "pipet " CPROVER_PREFIX "pipes[" - CPROVER_PREFIX "constant_infinity_uint];\n" - // offset to make sure we don't collide with other fds - "extern const int " CPROVER_PREFIX "pipe_offset;\n" - "unsigned " CPROVER_PREFIX "pipe_count=0;\n" "\n" // This function needs to be declared, or otherwise can't be called // by the entry-point construction. diff --git a/src/ansi-c/cprover_library.cpp b/src/ansi-c/cprover_library.cpp index 17386f3d457..45989869aa6 100644 --- a/src/ansi-c/cprover_library.cpp +++ b/src/ansi-c/cprover_library.cpp @@ -94,7 +94,8 @@ std::string get_cprover_library_text( void cprover_c_library_factory( const std::set &functions, - symbol_tablet &symbol_table, + const symbol_tablet &symbol_table, + symbol_tablet &dest_symbol_table, message_handlert &message_handler) { if(config.ansi_c.lib==configt::ansi_ct::libt::LIB_NONE) @@ -104,7 +105,7 @@ void cprover_c_library_factory( library_text=get_cprover_library_text(functions, symbol_table); - add_library(library_text, symbol_table, message_handler); + add_library(library_text, dest_symbol_table, message_handler); } void add_library( diff --git a/src/ansi-c/cprover_library.h b/src/ansi-c/cprover_library.h index 8a7804113b6..84b1eeffaa0 100644 --- a/src/ansi-c/cprover_library.h +++ b/src/ansi-c/cprover_library.h @@ -36,6 +36,7 @@ void add_library( void cprover_c_library_factory( const std::set &functions, + const symbol_tablet &, symbol_tablet &, message_handlert &); diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index beeb1501d9a..7b88f7cf65a 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -18,10 +18,10 @@ typedef __typeof__(sizeof(int)) __CPROVER_size_t; // NOLINTNEXTLINE(readability/identifiers) typedef signed long long __CPROVER_ssize_t; +#define __CPROVER_constant_infinity_uint 1 + void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero); extern const void *__CPROVER_deallocated; -extern const void *__CPROVER_new_object; -extern __CPROVER_bool __CPROVER_malloc_is_new_array; extern const void *__CPROVER_memory_leak; extern int __CPROVER_malloc_failure_mode; diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c index 849f217472f..73ac2892ffa 100644 --- a/src/ansi-c/library/pthread_lib.c +++ b/src/ansi-c/library/pthread_lib.c @@ -290,12 +290,15 @@ inline int pthread_mutex_destroy(pthread_mutex_t *mutex) #define __CPROVER_PTHREAD_H_INCLUDED #endif -extern __CPROVER_bool __CPROVER_threads_exited[]; -extern __CPROVER_thread_local unsigned long __CPROVER_thread_id; - -extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; -extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *); -extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key; +__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint]; +__CPROVER_thread_local unsigned long __CPROVER_thread_id = 0; +#if 0 +__CPROVER_thread_local const void + *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint]; +__CPROVER_thread_local void ( + *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *); +__CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0; +#endif inline void pthread_exit(void *value_ptr) { @@ -331,9 +334,11 @@ inline void pthread_exit(void *value_ptr) #define __CPROVER_ERRNO_H_INCLUDED #endif -extern __CPROVER_bool __CPROVER_threads_exited[]; -extern __CPROVER_thread_local unsigned long __CPROVER_thread_id; -extern unsigned long __CPROVER_next_thread_id; +__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint]; +#ifndef LIBRARY_CHECK +__CPROVER_thread_local unsigned long __CPROVER_thread_id = 0; +#endif +unsigned long __CPROVER_next_thread_id = 0; inline int pthread_join(pthread_t thread, void **value_ptr) { @@ -368,9 +373,11 @@ __CPROVER_HIDE:; #endif #ifdef __APPLE__ -extern __CPROVER_bool __CPROVER_threads_exited[]; -extern __CPROVER_thread_local unsigned long __CPROVER_thread_id; -extern unsigned long __CPROVER_next_thread_id; +__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint]; +#ifndef LIBRARY_CHECK +__CPROVER_thread_local unsigned long __CPROVER_thread_id = 0; +unsigned long __CPROVER_next_thread_id = 0; +#endif inline int _pthread_join(pthread_t thread, void **value_ptr) { @@ -533,12 +540,17 @@ inline int pthread_rwlock_wrlock(pthread_rwlock_t *lock) /* FUNCTION: __spawned_thread */ -extern __CPROVER_bool __CPROVER_threads_exited[]; -extern __CPROVER_thread_local unsigned long __CPROVER_thread_id; - -extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; -extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *); -extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key; +__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint]; +#ifndef LIBRARY_CHECK +__CPROVER_thread_local unsigned long __CPROVER_thread_id = 0; +#endif +#if 0 +__CPROVER_thread_local const void + *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint]; +__CPROVER_thread_local void ( + *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *); +#endif +__CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0; inline void __spawned_thread( unsigned long this_thread_id, @@ -596,7 +608,14 @@ __CPROVER_HIDE:; # define __CPROVER_PTHREAD_H_INCLUDED #endif -extern unsigned long __CPROVER_next_thread_id; +#ifndef LIBRARY_CHECK +unsigned long __CPROVER_next_thread_id = 0; +# if 0 +__CPROVER_thread_local void ( + *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *); +# endif +__CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0; +#endif void __spawned_thread( unsigned long this_thread_id, @@ -932,9 +951,15 @@ inline int pthread_barrier_wait(pthread_barrier_t *barrier) #define __CPROVER_PTHREAD_H_INCLUDED #endif -extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; -extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *); -extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key; +__CPROVER_thread_local const void + *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint]; +#ifndef LIBRARY_CHECK +# if 0 +__CPROVER_thread_local void ( + *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *); +# endif +__CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0; +#endif inline int pthread_key_create(pthread_key_t *key, void (*destructor)(void *)) { @@ -958,7 +983,8 @@ __CPROVER_HIDE:; #define __CPROVER_PTHREAD_H_INCLUDED #endif -extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; +__CPROVER_thread_local const void + *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint]; inline int pthread_key_delete(pthread_key_t key) { @@ -974,7 +1000,8 @@ __CPROVER_HIDE:; #define __CPROVER_PTHREAD_H_INCLUDED #endif -extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; +__CPROVER_thread_local const void + *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint]; inline void *pthread_getspecific(pthread_key_t key) { @@ -989,7 +1016,8 @@ __CPROVER_HIDE:; #define __CPROVER_PTHREAD_H_INCLUDED #endif -extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; +__CPROVER_thread_local const void + *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint]; inline int pthread_setspecific(pthread_key_t key, const void *value) { diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index bb3cd940290..28d7bd4eac1 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -32,9 +32,20 @@ inline long long int __builtin_llabs(long long int i) { return __CPROVER_llabs(i #undef exit +__CPROVER_thread_local void (*__CPROVER_atexit_table[32])(void); +__CPROVER_thread_local int __CPROVER_atexit_table_use = 0; + inline void exit(int status) { +__CPROVER_HIDE:; (void)status; + + while(__CPROVER_atexit_table_use > 0) + { + --__CPROVER_atexit_table_use; + __CPROVER_atexit_table[__CPROVER_atexit_table_use](); + } + __CPROVER_assume(0); #ifdef LIBRARY_CHECK __builtin_unreachable(); @@ -71,6 +82,7 @@ inline void abort(void) #undef calloc __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +_Bool __CPROVER_malloc_is_new_array = 0; inline void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size) { @@ -141,6 +153,9 @@ __CPROVER_HIDE:; #undef malloc __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +#ifndef LIBRARY_CHECK +_Bool __CPROVER_malloc_is_new_array = 0; +#endif inline void *malloc(__CPROVER_size_t malloc_size) { @@ -199,7 +214,10 @@ __CPROVER_HIDE:; /* FUNCTION: __builtin_alloca */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); -extern void *__CPROVER_alloca_object; +const void *__CPROVER_alloca_object = 0; +#ifndef LIBRARY_CHECK +_Bool __CPROVER_malloc_is_new_array = 0; +#endif inline void *__builtin_alloca(__CPROVER_size_t alloca_size) { @@ -242,7 +260,13 @@ __CPROVER_HIDE:; #undef free __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); -extern void *__CPROVER_alloca_object; +#ifndef LIBRARY_CHECK +const void *__CPROVER_alloca_object = 0; +#endif +const void *__CPROVER_new_object = 0; +#ifndef LIBRARY_CHECK +_Bool __CPROVER_malloc_is_new_array = 0; +#endif inline void free(void *ptr) { @@ -591,3 +615,28 @@ __CPROVER_HIDE:; __CPROVER_assume(result >= 0); return result; } + +/* FUNCTION: atexit */ + +#ifndef __CPROVER_ERRNO_H_INCLUDED +# include +# define __CPROVER_ERRNO_H_INCLUDED +#endif + +#ifndef LIBRARY_CHECK +__CPROVER_thread_local void (*__CPROVER_atexit_table[32])(void); +__CPROVER_thread_local int __CPROVER_atexit_table_use = 0; +#endif + +int atexit(void (*function)(void)) +{ +__CPROVER_HIDE:; + if(__CPROVER_atexit_table_use >= 32) + { + errno = ENOMEM; + return -1; + } + + __CPROVER_atexit_table[__CPROVER_atexit_table_use++] = function; + return 0; +} diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c index 096d8f9837d..f2c4408e5ed 100644 --- a/src/ansi-c/library/unistd.c +++ b/src/ansi-c/library/unistd.c @@ -45,10 +45,10 @@ int unlink(const char *s) #define __CPROVER_ERRNO_H_INCLUDED #endif -extern struct __CPROVER_pipet __CPROVER_pipes[]; +extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; -extern unsigned __CPROVER_pipe_count; +unsigned __CPROVER_pipe_count = 0; __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); @@ -96,7 +96,7 @@ __CPROVER_HIDE:; /* FUNCTION: close */ -extern struct __CPROVER_pipet __CPROVER_pipes[]; +extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; @@ -148,7 +148,7 @@ inline int _close(int fildes) #define size_type size_t #endif -extern struct __CPROVER_pipet __CPROVER_pipes[]; +extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; @@ -222,7 +222,7 @@ inline ret_type _write(int fildes, const void *buf, size_type nbyte) #define size_type size_t #endif -extern struct __CPROVER_pipet __CPROVER_pipes[]; +extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index c1365387c83..704587d80a3 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -67,36 +67,13 @@ void cpp_internal_additions(std::ostream &out) out << "const unsigned __CPROVER::constant_infinity_uint;" << '\n'; out << "typedef void " CPROVER_PREFIX "integer;" << '\n'; out << "typedef void " CPROVER_PREFIX "rational;" << '\n'; - // TODO: thread_local is still broken - // out << "thread_local unsigned long " - // << CPROVER_PREFIX "thread_id = 0;" << '\n'; - out << CPROVER_PREFIX "bool " - << CPROVER_PREFIX "threads_exited[__CPROVER::constant_infinity_uint];" - << '\n'; - out << "unsigned long " CPROVER_PREFIX "next_thread_id = 0;" << '\n'; - // TODO: thread_local is still broken - out << "void* " - << CPROVER_PREFIX "thread_keys[__CPROVER::constant_infinity_uint];" - << '\n'; - // TODO: thread_local is still broken - out << "void (*" - << CPROVER_PREFIX "thread_key_dtors[__CPROVER::constant_infinity_uint])" - << "(void *);" << '\n'; - // TODO: thread_local is still broken - out << "unsigned long " CPROVER_PREFIX "next_thread_key = 0;" << '\n'; - out << "extern unsigned char " - << CPROVER_PREFIX "memory[__CPROVER::constant_infinity_uint];" << '\n'; // malloc out << "const void *" CPROVER_PREFIX "deallocated = 0;" << '\n'; out << "const void *" CPROVER_PREFIX "dead_object = 0;" << '\n'; - out << "const void *" CPROVER_PREFIX "new_object = 0;" << '\n'; - out << "" CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array = 0;" - << '\n'; out << "const void *" CPROVER_PREFIX "memory_leak = 0;" << '\n'; out << "void *" CPROVER_PREFIX "allocate(" << CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);" << '\n'; - out << "const void *" CPROVER_PREFIX "alloca_object = 0;" << '\n'; // auxiliaries for new/delete out << "void *__new(__CPROVER::size_t);" << '\n'; @@ -112,6 +89,9 @@ void cpp_internal_additions(std::ostream &out) out << "int " << rounding_mode_identifier() << " = " << std::to_string(config.ansi_c.rounding_mode) << ';' << '\n'; + // atexit + out << "void exit(int);" << '\n'; + // pipes, write, read, close out << "struct " CPROVER_PREFIX "pipet {\n" << " bool widowed;\n" @@ -119,11 +99,6 @@ void cpp_internal_additions(std::ostream &out) << " short next_avail;\n" << " short next_unread;\n" << "};\n"; - out << "extern struct " CPROVER_PREFIX "pipet " - << "" CPROVER_PREFIX "pipes[__CPROVER::constant_infinity_uint];" << '\n'; - // offset to make sure we don't collide with other fds - out << "extern const int " CPROVER_PREFIX "pipe_offset;" << '\n'; - out << "unsigned " CPROVER_PREFIX "pipe_count=0;" << '\n'; // This function needs to be declared, or otherwise can't be called // by the entry-point construction. diff --git a/src/cpp/cprover_library.cpp b/src/cpp/cprover_library.cpp index fae330e1063..b5425b3dcc3 100644 --- a/src/cpp/cprover_library.cpp +++ b/src/cpp/cprover_library.cpp @@ -37,7 +37,8 @@ static std::string get_cprover_library_text( void cprover_cpp_library_factory( const std::set &functions, - symbol_tablet &symbol_table, + const symbol_tablet &symbol_table, + symbol_tablet &dest_symbol_table, message_handlert &message_handler) { if(config.ansi_c.lib == configt::ansi_ct::libt::LIB_NONE) @@ -46,5 +47,5 @@ void cprover_cpp_library_factory( const std::string library_text = get_cprover_library_text(functions, symbol_table); - add_library(library_text, symbol_table, message_handler); + add_library(library_text, dest_symbol_table, message_handler); } diff --git a/src/cpp/cprover_library.h b/src/cpp/cprover_library.h index 9f08436a2fe..c572fb597b3 100644 --- a/src/cpp/cprover_library.h +++ b/src/cpp/cprover_library.h @@ -18,6 +18,7 @@ class symbol_tablet; void cprover_cpp_library_factory( const std::set &functions, + const symbol_tablet &, symbol_tablet &, message_handlert &); diff --git a/src/cpp/library/cprover.h b/src/cpp/library/cprover.h index a89d9dce8d0..cfbc3a9d4d5 100644 --- a/src/cpp/library/cprover.h +++ b/src/cpp/library/cprover.h @@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com typedef __typeof__(sizeof(int)) __CPROVER_size_t; void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero); extern const void *__CPROVER_deallocated; -extern const void *__CPROVER_new_object; -extern _Bool __CPROVER_malloc_is_new_array; extern const void *__CPROVER_memory_leak; void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__)); diff --git a/src/cpp/library/new.c b/src/cpp/library/new.c index d0dcde466d1..6a549379924 100644 --- a/src/cpp/library/new.c +++ b/src/cpp/library/new.c @@ -1,6 +1,8 @@ /* FUNCTION: __new */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +const void *__CPROVER_new_object = 0; +_Bool __CPROVER_malloc_is_new_array = 0; inline void *__new(__typeof__(sizeof(int)) malloc_size) { @@ -28,6 +30,8 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size) /* FUNCTION: __new_array */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +const void *__CPROVER_new_object = 0; +_Bool __CPROVER_malloc_is_new_array = 0; inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size) { @@ -66,6 +70,8 @@ inline void *__placement_new(__typeof__(sizeof(int)) malloc_size, void *p) /* FUNCTION: __delete */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +const void *__CPROVER_new_object = 0; +_Bool __CPROVER_malloc_is_new_array = 0; inline void __delete(void *ptr) { @@ -101,6 +107,8 @@ inline void __delete(void *ptr) /* FUNCTION: __delete_array */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +const void *__CPROVER_new_object = 0; +_Bool __CPROVER_malloc_is_new_array = 0; inline void __delete_array(void *ptr) { diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp index 48b18553bb5..353fc8a4fd9 100644 --- a/src/goto-programs/link_to_library.cpp +++ b/src/goto-programs/link_to_library.cpp @@ -14,6 +14,60 @@ Author: Daniel Kroening, kroening@kroening.com #include "compute_called_functions.h" #include "goto_convert_functions.h" #include "goto_model.h" +#include "link_goto_model.h" + +#include + +/// Try to add \p missing_function from \p library to \p goto_model. +static optionalt add_one_function( + goto_modelt &goto_model, + message_handlert &message_handler, + const std::function &, + const symbol_tablet &, + symbol_tablet &, + message_handlert &)> &library, + const irep_idt &missing_function) +{ + goto_modelt library_model; + library( + {missing_function}, + goto_model.symbol_table, + library_model.symbol_table, + message_handler); + + // convert to CFG + if( + library_model.symbol_table.symbols.find(missing_function) != + library_model.symbol_table.symbols.end()) + { + goto_convert( + missing_function, + library_model.symbol_table, + library_model.goto_functions, + message_handler); + } + + // check whether additional initialization may be required + if( + goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION) != + goto_model.goto_functions.function_map.end()) + { + for(const auto &entry : library_model.symbol_table) + { + if( + entry.second.is_static_lifetime && !entry.second.is_type && + !entry.second.is_macro && entry.second.type.id() != ID_code && + !goto_model.symbol_table.has_symbol(entry.first)) + { + goto_model.unload(INITIALIZE_FUNCTION); + break; + } + } + } + + return link_goto_model(goto_model, std::move(library_model), message_handler); +} /// Complete missing function definitions using the \p library. /// \param goto_model: goto model that may contain function calls and symbols @@ -25,24 +79,27 @@ Author: Daniel Kroening, kroening@kroening.com void link_to_library( goto_modelt &goto_model, message_handlert &message_handler, - const std::function< - void(const std::set &, symbol_tablet &, message_handlert &)> - &library) + const std::function &, + const symbol_tablet &, + symbol_tablet &, + message_handlert &)> &library) { // this needs a fixedpoint, as library functions // may depend on other library functions std::set added_functions; + replace_symbolt::expr_mapt object_type_updates; + const bool had_init = + goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION) != + goto_model.goto_functions.function_map.end(); while(true) { std::unordered_set called_functions = compute_called_functions(goto_model.goto_functions); - // eliminate those for which we already have a body - - std::set missing_functions; - + bool changed = false; for(const auto &id : called_functions) { goto_functionst::function_mapt::const_iterator f_it = @@ -59,30 +116,44 @@ void link_to_library( // already added } else - missing_functions.insert(id); + { + changed = true; + added_functions.insert(id); + + auto updates_opt = + add_one_function(goto_model, message_handler, library, id); + if(!updates_opt.has_value()) + { + messaget log{message_handler}; + log.warning() << "Linking library function '" << id << "' failed" + << messaget::eom; + continue; + } + object_type_updates.insert(updates_opt->begin(), updates_opt->end()); + } } // done? - if(missing_functions.empty()) + if(!changed) break; + } - library(missing_functions, goto_model.symbol_table, message_handler); - - // convert to CFG - for(const auto &id : missing_functions) - { - if( - goto_model.symbol_table.symbols.find(id) != - goto_model.symbol_table.symbols.end()) - { - goto_convert( - id, - goto_model.symbol_table, - goto_model.goto_functions, - message_handler); - } - - added_functions.insert(id); - } + if( + had_init && + goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION) == + goto_model.goto_functions.function_map.end()) + { + static_lifetime_init( + goto_model.symbol_table, + goto_model.symbol_table.lookup_ref(INITIALIZE_FUNCTION).location); + goto_convert( + INITIALIZE_FUNCTION, + goto_model.symbol_table, + goto_model.goto_functions, + message_handler); + goto_model.goto_functions.update(); } + + if(!object_type_updates.empty()) + finalize_linking(goto_model, object_type_updates); } diff --git a/src/goto-programs/link_to_library.h b/src/goto-programs/link_to_library.h index 8f04f377ddc..8ddf2d3b0b8 100644 --- a/src/goto-programs/link_to_library.h +++ b/src/goto-programs/link_to_library.h @@ -24,7 +24,10 @@ class symbol_tablet; void link_to_library( goto_modelt &, message_handlert &, - const std::function< - void(const std::set &, symbol_tablet &, message_handlert &)> &); + const std::function &, + const symbol_tablet &, + symbol_tablet &, + message_handlert &)> &); #endif // CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp index 5258d149210..44a6c1be716 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -127,6 +127,7 @@ void remove_internal_symbols( special.insert("__placement_new_array"); special.insert("__delete"); special.insert("__delete_array"); + special.insert("exit"); for(symbol_tablet::symbolst::const_iterator it=symbol_table.symbols.begin();