C library: move pipe() 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
pipe-related library functions.

Author: tautschnig

regression/cprover/arrays/array1.desc

@@ -3,11 +3,11 @@ array1.c
 --text --solve --inline --no-safety
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 30\)$
+^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$
+^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(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 \. \(S23\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S24\(ς\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::k❞\), signedbv\[64\]\)\)\)\)$
+^\(\d+\) ∀ ς : state \. \(S22\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S23\(ς\)$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(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 \. \(S20\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S21\(ς\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
+^\(\d+\) ∀ ς : state \. \(S19\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S20\(ς\)$
+^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝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 \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
+^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=1\]\)$
+^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝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 \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\)$
+^\(\d+\) S18 = S17$
 ^\(\d+\) S19 = S18$
-^\(\d+\) S20 = S19$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
-^\(\d+\) S22 = S21$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
+^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=1\]\)$
+^\(\d+\) S21 = S20$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --

regression/cprover/basic/basic3.desc

@@ -3,10 +3,10 @@ basic3.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)
-\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝y❞:=0\]\)
-\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=1\]\)
-\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝y❞:=2\]\)
-\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝x❞\) = 1\)
+\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\)
+\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝y❞:=0\]\)
+\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)
+\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝y❞:=2\]\)
+\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --

regression/cprover/basic/basic4.desc

@@ -3,9 +3,9 @@ basic4.c
 --text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=2\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
+^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=1\]\)$
+^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=2\]\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
 ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
 --

regression/cprover/basic/basic5.desc

@@ -3,12 +3,12 @@ basic5.c
 --text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(enter_scope_state\(ς, ❝main::1::c2❞\)\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$
-^\(\d+\) S25 = S24$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$
+^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(enter_scope_state\(ς, ❝main::1::c2❞\)\)$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$
+^\(\d+\) S24 = S23$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
 --

regression/cprover/basic/basic6.desc

@@ -3,11 +3,11 @@ basic6.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-^\(23\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
+^\(22\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=1\]\)$
+^\(23\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
 ^\(24\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
 ^\(25\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
 ^\(26\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
-^\(27\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
-^\(28\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 5\)$
+^\(27\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝x❞\) = 5\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --

regression/cprover/basic/nondet1.desc

@@ -3,13 +3,13 @@ nondet1.c
 --text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state, nondet::S22-0 : signedbv\[32\] \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=nondet::S22-0\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$
-^\(\d+\) S23 = S22$
-^\(\d+\) ∀ ς : state, nondet::S24-0 : signedbv\[32\] \. S23\(ς\) ⇒ S24\(ς\[❝main::1::y❞:=nondet::S24-0\]\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$
-^\(\d+\) S25 = S24$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26\(ς\[❝return'❞:=0\]\)$
+^\(\d+\) ∀ ς : state, nondet::S21-0 : signedbv\[32\] \. S20\(ς\) ⇒ S21\(ς\[❝main::1::x❞:=nondet::S21-0\]\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$
+^\(\d+\) S22 = S21$
+^\(\d+\) ∀ ς : state, nondet::S23-0 : signedbv\[32\] \. S22\(ς\) ⇒ S23\(ς\[❝main::1::y❞:=nondet::S23-0\]\)$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$
+^\(\d+\) S24 = S23$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝return'❞:=0\]\)$
 ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
 ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
 --