C library: atexit

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.

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.

regression/cbmc-library/__atomic_always_lock_free-01/main.c

@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+_Bool __atomic_always_lock_free(__CPROVER_size_t, void *);
+#endif
+
 int main()
 {
   assert(__atomic_always_lock_free(sizeof(int), 0));

regression/cbmc-library/__atomic_clear-01/main.c

@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+void __atomic_clear(_Bool *, int);
+#endif
+
 int main()
 {
   _Bool n;

regression/cbmc-library/__atomic_is_lock_free-01/main.c

@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+_Bool __atomic_is_lock_free(__CPROVER_size_t, void *);
+#endif
+
 int main()
 {
   assert(__atomic_is_lock_free(sizeof(int), 0));

regression/cbmc-library/__atomic_signal_fence-01/main.c

@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+void __atomic_signal_fence(int);
+#endif
+
 int main()
 {
   __atomic_signal_fence(0);

regression/cbmc-library/__atomic_test_and_set-01/main.c

@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+_Bool __atomic_test_and_set(void *, int);
+#endif
+
 int main()
 {
   char c = 0;

regression/cbmc-library/__atomic_thread_fence-01/main.c

@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+void __atomic_thread_fence(int);
+#endif
+
 int main()
 {
   __atomic_thread_fence(0);

regression/cbmc-library/__errno_location-01/main.c

@@ -1,9 +1,9 @@
 #include <assert.h>
 #include <errno.h>
 
-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;
 }

regression/cbmc-library/__errno_location-01/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

regression/cbmc-library/_longjmp-01/main.c

@@ -1,5 +1,9 @@
 #include <setjmp.h>
 
+#ifndef __GNUC__
+#  define _longjmp(a, b) longjmp(a, b)
+#endif
+
 static jmp_buf env;
 
 int main()

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$

regression/cbmc-library/atexit-01/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void cleanup()
+{
+  assert(0);
+}
+
+int main()
+{
+  atexit(cleanup);
+}

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

regression/cbmc-library/atexit-02/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void cleanup()
+{
+  assert(0);
+}
+
+int main()
+{
+  atexit(cleanup);
+  exit(0);
+}

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

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$

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

regression/cbmc-library/memcpy-07/main.c

@@ -1,4 +1,5 @@
 // #include <string.h> intentionally omitted
+void *memcpy();
 
 struct c
 {

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

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

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
 --

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$
 --

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

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

regression/cbmc/array_of_bool_as_bitvec/main.c

@@ -3,6 +3,7 @@
 #include <stdlib.h>
 
 __CPROVER_bool w[8];
+__CPROVER_bool v[__CPROVER_constant_infinity_uint];
 
 void main()
 {

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.
 

regression/cbmc/destructor1/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+#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
+}

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

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

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

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$

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$

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

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

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

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

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

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