C library: move pthreads related definitions to library

With the support of building initialisers while adding the library we
can move library-only symbols to the library. This avoids polluting the
initialisation function for all cases that don't actually use
pthreads-related library functions.

This removal of unused symbols required adding a symbol into the
array_of_bool_as_bitvec test, which previously implicitly relied on
those library-specific symbols in the patterns being tested for.

Author: tautschnig

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/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/xml-trace/test.desc

@@ -7,7 +7,7 @@ activate-multi-line-match
 VERIFICATION FAILED
 <assignment assignment_type="actual_parameter" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>union myunion</full_lhs_type>\n\s*<full_lhs>u</full_lhs>
 <value>\{ \.i=\d+ll? \}</value>\n\s*<value_expression>\n\s*<union>\n\s*<member member_name="i">\n\s*<integer binary="\d+" c_type=".*int.*" width="\d+">\d+</integer>\n\s*</member>\n\s*</union>\n\s*</value_expression>
-<assignment assignment_type="state" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" function="test" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>signed long( long)? int</full_lhs_type>\n\s*<full_lhs>u\.i</full_lhs>\n\s*<full_lhs_value binary="[01]+">\d+ll?</full_lhs_value>\n\s*</assignment>
+<assignment assignment_type="state" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" function="test" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>(signed long( long)? int|int64_t)</full_lhs_type>\n\s*<full_lhs>u\.i</full_lhs>\n\s*<full_lhs_value binary="[01]+">\d+ll?</full_lhs_value>\n\s*</assignment>
 --
 ^warning: ignoring
 --

regression/cprover/arrays/array1.desc

@@ -3,11 +3,11 @@ array1.c
 --text --solve --inline --no-safety
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$
-^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$
-^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$
-^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 30\)$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 30\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
 ^\[main\.assertion\.3\] line \d+ property 3: REFUTED$

regression/cprover/arrays/array2.desc

@@ -3,9 +3,9 @@ array2.c
 --text --solve --inline --no-safety
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. \(S19\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S20\(ς\)$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::k❞\), signedbv\[64\]\)\)\)\)$
+^\(\d+\) ∀ ς : state \. \(S13\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S14\(ς\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::k❞\), signedbv\[64\]\)\)\)\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
 --

regression/cprover/basic/assume1.desc

@@ -6,9 +6,9 @@ assume1.c
 ^ \(\d+\) ∀ ς : state \. initial_state\(ς\) ⇒ SInitial\(ς\)$
 ^ \(\d+\) S0 = SInitial$
 ^ \(\d+\) S1 = S0$
-^\(\d+\) ∀ ς : state \. \(S16\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S17\(ς\)$
-^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
-^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
+^\(\d+\) ∀ ς : state \. \(S10\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S11\(ς\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
 --

regression/cprover/basic/basic1.desc

@@ -5,8 +5,8 @@ basic1.c
 ^SIGNAL=0$
 ^ \(\d+\) ∀ ς : state \. initial_state\(ς\) ⇒ SInitial\(ς\)$
 ^ \(\d+\) S0 = SInitial$
-^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝x❞:=0\]\)$
-^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=1\]\)$
-^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
+^\(\d+\) ∀ ς : state \. S7\(ς\) ⇒ S8\(ς\[❝x❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝x❞:=1\]\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --

regression/cprover/basic/basic2.desc

@@ -3,11 +3,11 @@ basic2.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝x❞:=0\]\)$
-^\(\d+\) S15 = S14$
-^\(\d+\) S16 = S15$
-^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=1\]\)$
-^\(\d+\) S18 = S17$
-^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
+^\(\d+\) ∀ ς : state \. S7\(ς\) ⇒ S8\(ς\[❝x❞:=0\]\)$
+^\(\d+\) S9 = S8$
+^\(\d+\) S10 = S9$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝x❞:=1\]\)$
+^\(\d+\) S12 = S11$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --