Skip to content

Commit da4c6ec

Browse files
tautschnigtautschnig
committed
C/C++ library: move free/delete-only 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 memory (de-)allocation library functions.
1 parent 5f7e0de commit da4c6ec

File tree

72 files changed

+371
-366
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

72 files changed

+371
-366
lines changed

Diff for: ‎regression/cbmc-library/alloca-02/main.c

+5
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,14 @@
44
void *alloca(size_t alloca_size);
55
#endif
66

7+
// intentionally type conflicting: the built-in library uses const void*; this
8+
// is to check that object type updates are performed
9+
extern const char *__CPROVER_alloca_object;
10+
711
int *foo()
812
{
913
int *foo_ptr = alloca(sizeof(int));
14+
__CPROVER_assert(foo_ptr == __CPROVER_alloca_object, "may fail");
1015
return foo_ptr;
1116
}
1217

Diff for: ‎regression/cbmc-library/alloca-02/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE
22
main.c
33
--pointer-check
44
dereference failure: dead object in \*from_foo: FAILURE$
5-
^\*\* 1 of 6 failed
5+
^\*\* 2 of 7 failed
66
^VERIFICATION FAILED$
77
^EXIT=10$
88
^SIGNAL=0$

Diff for: ‎regression/cbmc/xml-escaping/debug_output.desc

-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@ main.c
44
^EXIT=10$
55
^SIGNAL=0$
66
VERIFICATION FAILED
7-
⇔ false
87
\¬main\:\:1\:\:x\!0\@1\#1
98
--
109
XML does not support escaping non-printable character

Diff for: ‎regression/cprover/arrays/array1.desc

+5-5
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ array1.c
33
--text --solve --inline --no-safety
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$
7-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$
8-
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$
9-
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$
10-
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 30\)$
6+
^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$
7+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$
8+
^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$
9+
^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$
10+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 30\)$
1111
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1212
^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
1313
^\[main\.assertion\.3\] line \d+ property 3: REFUTED$

Diff for: ‎regression/cprover/arrays/array2.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ array2.c
33
--text --solve --inline --no-safety
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. \(S22\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S23\(ς\)$
7-
^\(\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\]\)\)\)\)$
8-
^\(\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\]\)\)\)\)$
6+
^\(\d+\) ∀ ς : state \. \(S19\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S20\(ς\)$
7+
^\(\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\]\)\)\)\)$
8+
^\(\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\]\)\)\)\)$
99
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1010
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
1111
--

Diff for: ‎regression/cprover/basic/assume1.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,9 @@ assume1.c
66
^ \(\d+\) ∀ ς : state \. initial_state\(ς\) ⇒ SInitial\(ς\)$
77
^ \(\d+\) S0 = SInitial$
88
^ \(\d+\) S1 = S0$
9-
^\(\d+\) ∀ ς : state \. \(S19\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S20\(ς\)$
10-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
11-
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
9+
^\(\d+\) ∀ ς : state \. \(S16\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S17\(ς\)$
10+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
11+
^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
1212
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1313
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
1414
--

Diff for: ‎regression/cprover/basic/basic1.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ basic1.c
55
^SIGNAL=0$
66
^ \(\d+\) ∀ ς : state \. initial_state\(ς\) ⇒ SInitial\(ς\)$
77
^ \(\d+\) S0 = SInitial$
8-
^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\)$
9-
^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=1\]\)$
10-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
8+
^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝x❞:=0\]\)$
9+
^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=1\]\)$
10+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
1111
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1212
--

Diff for: ‎regression/cprover/basic/basic2.desc

+5-5
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ basic2.c
33
--text --solve --inline
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\)$
6+
^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝x❞:=0\]\)$
7+
^\(\d+\) S15 = S14$
8+
^\(\d+\) S16 = S15$
9+
^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=1\]\)$
710
^\(\d+\) S18 = S17$
8-
^\(\d+\) S19 = S18$
9-
^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=1\]\)$
10-
^\(\d+\) S21 = S20$
11-
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
11+
^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
1212
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1313
--

Diff for: ‎regression/cprover/basic/basic3.desc

+5-5
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ basic3.c
33
--text --solve --inline
44
^EXIT=0$
55
^SIGNAL=0$
6-
\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\)
7-
\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝y❞:=0\]\)
8-
\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)
9-
\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝y❞:=2\]\)
10-
\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)
6+
\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝x❞:=0\]\)
7+
\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ S15\(ς\[❝y❞:=0\]\)
8+
\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=1\]\)
9+
\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝y❞:=2\]\)
10+
\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ \(ς\(❝x❞\) = 1\)
1111
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1212
--

Diff for: ‎regression/cprover/basic/basic4.desc

+4-4
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ basic4.c
33
--text --solve --inline
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=0\]\)$
7-
^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=1\]\)$
8-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=2\]\)$
9-
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
6+
^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝x❞:=0\]\)$
7+
^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=1\]\)$
8+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=2\]\)$
9+
^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
1010
^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
1111
--

Diff for: ‎regression/cprover/basic/basic5.desc

+6-6
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ basic5.c
33
--text --solve --inline
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$
7-
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(enter_scope_state\(ς, ❝main::1::c2❞\)\)$
8-
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$
9-
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$
10-
^\(\d+\) S24 = S23$
11-
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$
6+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$
7+
^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(enter_scope_state\(ς, ❝main::1::c2❞\)\)$
8+
^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$
9+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$
10+
^\(\d+\) S21 = S20$
11+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$
1212
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1313
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
1414
--

Diff for: ‎regression/cprover/basic/basic6.desc

+5-5
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ basic6.c
33
--text --solve --inline
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(22\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=1\]\)$
6+
^\(19\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=1\]\)$
7+
^\(20\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
8+
^\(21\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
9+
^\(22\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
710
^\(23\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
8-
^\(24\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
9-
^\(25\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
10-
^\(26\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
11-
^\(27\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝x❞\) = 5\)$
11+
^\(24\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 5\)$
1212
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1313
--

Diff for: ‎regression/cprover/basic/nondet1.desc

+7-7
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,13 @@ nondet1.c
33
--text --solve --inline
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state, nondet::S21-0 : signedbv\[32\] \. S20\(ς\) ⇒ S21\(ς\[❝main::1::x❞:=nondet::S21-0\]\)$
7-
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$
8-
^\(\d+\) S22 = S21$
9-
^\(\d+\) ∀ ς : state, nondet::S23-0 : signedbv\[32\] \. S22\(ς\) ⇒ S23\(ς\[❝main::1::y❞:=nondet::S23-0\]\)$
10-
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$
11-
^\(\d+\) S24 = S23$
12-
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝return'❞:=0\]\)$
6+
^\(\d+\) ∀ ς : state, nondet::S18-0 : signedbv\[32\] \. S17\(ς\) ⇒ S18\(ς\[❝main::1::x❞:=nondet::S18-0\]\)$
7+
^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$
8+
^\(\d+\) S19 = S18$
9+
^\(\d+\) ∀ ς : state, nondet::S20-0 : signedbv\[32\] \. S19\(ς\) ⇒ S20\(ς\[❝main::1::y❞:=nondet::S20-0\]\)$
10+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$
11+
^\(\d+\) S21 = S20$
12+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝return'❞:=0\]\)$
1313
^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
1414
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
1515
--

Diff for: ‎regression/cprover/branching/branching1.desc

+12-12
Original file line numberDiff line numberDiff line change
@@ -3,20 +3,20 @@ branching1.c
33
--text --solve --inline
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. \(S19\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) ≥ 5\)\) ⇒ S20T\(\ς\)$
7-
^\(\d+\) ∀ ς : state \. \(S19\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 5\) ⇒ S20\(ς\)$
8-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
9-
^\(\d+\) S21 = S20$
6+
^\(\d+\) ∀ ς : state \. \(S16\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) ≥ 5\)\) ⇒ S17T\(\ς\)$
7+
^\(\d+\) ∀ ς : state \. \(S16\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 5\) ⇒ S17\(ς\)$
8+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
9+
^\(\d+\) S18 = S17$
10+
^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(0 ≠ 0\)$
11+
^\(\d+\) S19 = S18$
12+
^\(\d+\) S20 = S19$
13+
^\(\d+\) ∀ ς : state \. S17T\(ς\) ⇒ \(ς\(❝main::1::x❞\) < 5\)$
14+
^\(\d+\) S21 = S17T$
1015
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(0 ≠ 0\)$
1116
^\(\d+\) S22 = S21$
12-
^\(\d+\) S23 = S22$
13-
^\(\d+\) ∀ ς : state \. S20T\(ς\) ⇒ \(ς\(❝main::1::x❞\) < 5\)$
14-
^\(\d+\) S24 = S20T$
15-
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(0 ≠ 0\)$
16-
^\(\d+\) S25 = S24$
17-
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S26in\(ς\)$
18-
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26in\(ς\)$
19-
^\(\d+\) S26 = S26in$
17+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S23in\(ς\)$
18+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23in\(ς\)$
19+
^\(\d+\) S23 = S23in$
2020
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
2121
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
2222
^\[main\.assertion\.3\] line \d+ property 3: SUCCESS$

Diff for: ‎regression/cprover/branching/branching2.desc

+8-8
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,14 @@ branching2.c
33
--text --solve --inline
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ¬\(ς\(❝main::1::a❞\) ≥ 5\)\) ⇒ S21T\(ς\)$
7-
^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(❝main::1::a❞\) ≥ 5\) ⇒ S21\(ς\)$
8-
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::b❞:=1\]\)$
9-
^\(\d+\) S23 = S22$
10-
^\(\d+\) ∀ ς : state \. S21T\(ς\) ⇒ S24\(ς\[❝main::1::b❞:=0\]\)$
11-
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S25in\(ς\)$
12-
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25in\(ς\)$
13-
^\(\d+\) S25 = S25in$
6+
^\(\d+\) ∀ ς : state \. \(S17\(ς\) ∧ ¬\(ς\(❝main::1::a❞\) ≥ 5\)\) ⇒ S18T\(ς\)$
7+
^\(\d+\) ∀ ς : state \. \(S17\(ς\) ∧ ς\(❝main::1::a❞\) ≥ 5\) ⇒ S18\(ς\)$
8+
^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝main::1::b❞:=1\]\)$
9+
^\(\d+\) S20 = S19$
10+
^\(\d+\) ∀ ς : state \. S18T\(ς\) ⇒ S21\(ς\[❝main::1::b❞:=0\]\)$
11+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S22in\(ς\)$
12+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22in\(ς\)$
13+
^\(\d+\) S22 = S22in$
1414
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1515
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
1616
--

Diff for: ‎regression/cprover/float/basic-float1.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ basic-float1.c
33
--text --solve --inline
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝main::1::f❞:=floatbv_typecast\(1, floatbv\[32\], ς\(❝__CPROVER_rounding_mode❞\)\)\]\)$
7-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ ieee_float_equal\(floatbv_plus\(ς\(❝main::1::f❞\), 0\.5, ς\(❝__CPROVER_rounding_mode❞\)\), 1\.5\)$
6+
^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝main::1::f❞:=floatbv_typecast\(1, floatbv\[32\], ς\(❝__CPROVER_rounding_mode❞\)\)\]\)$
7+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ ieee_float_equal\(floatbv_plus\(ς\(❝main::1::f❞\), 0\.5, ς\(❝__CPROVER_rounding_mode❞\)\), 1\.5\)$
88
^\[main\.assertion\.1\] line \d+ addition: SUCCESS$
99
--

Diff for: ‎regression/cprover/function_calls/call_no_body1.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ call_no_body1.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^\*\*\*\* WARNING: no body for function function_without_body$
7-
^\(\d+\) ∀ ς : state, nondet::S27\.2-0 : signedbv\[32\] \. S27\.1\(ς\) ⇒ S27\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet::S27\.2-0\]\)$
8-
^\(\d+\) ∀ ς : state \. S27\.2\(ς\) ⇒ S27\.3\(ς\[❝main::1::x❞:=ς\(❝main::\$tmp::return_value_function_without_body❞\)\]\)$
7+
^\(\d+\) ∀ ς : state, nondet::S24\.2-0 : signedbv\[32\] \. S24\.1\(ς\) ⇒ S24\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet::S24\.2-0\]\)$
8+
^\(\d+\) ∀ ς : state \. S24\.2\(ς\) ⇒ S24\.3\(ς\[❝main::1::x❞:=ς\(❝main::\$tmp::return_value_function_without_body❞\)\]\)$
99
--

Diff for: ‎regression/cprover/function_calls/call_no_body2.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,5 @@ call_no_body2.c
33
--text
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state, nondet::S27\.2-0 : signedbv\[32\] \. S27\.1\(ς\) ⇒ S27\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S27\.2-0\]\)$
6+
^\(\d+\) ∀ ς : state, nondet::S24\.2-0 : signedbv\[32\] \. S24\.1\(ς\) ⇒ S24\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S24\.2-0\]\)$
77
--

Diff for: ‎regression/cprover/loops/do_while1.desc

+6-6
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ do_while1.c
33
--text --solve --inline
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝x❞:=10\]\)$
7-
^\(\d+\) ∀ ς : state \. S22T\(ς\) ⇒ S21in\(ς\)$
8-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21in\(ς\)$
9-
^\(\d+\) ∀ ς : state \. S21in\(ς\) ⇒ S21\(ς\[❝x❞:=20\]\)$
10-
^\(\d+\) ∀ ς : state . \(S21\(ς\) ∧ ς\(❝x❞\) ≠ 20\) ⇒ S22T\(ς\)$
11-
^\(\d+\) ∀ ς : state . \(S21\(ς\) ∧ ¬\(ς\(❝x❞\) ≠ 20\)\) ⇒ S22\(ς\)$
6+
^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17\(ς\[❝x❞:=10\]\)$
7+
^\(\d+\) ∀ ς : state \. S19T\(ς\) ⇒ S18in\(ς\)$
8+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18in\(ς\)$
9+
^\(\d+\) ∀ ς : state \. S18in\(ς\) ⇒ S18\(ς\[❝x❞:=20\]\)$
10+
^\(\d+\) ∀ ς : state . \(S18\(ς\) ∧ ς\(❝x❞\) ≠ 20\) ⇒ S19T\(ς\)$
11+
^\(\d+\) ∀ ς : state . \(S18\(ς\) ∧ ¬\(ς\(❝x❞\) ≠ 20\)\) ⇒ S19\(ς\)$
1212
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1313
--
1414
--

Diff for: ‎regression/cprover/loops/for1.desc

+8-8
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,14 @@ for1.c
33
--text --solve --inline
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S21in\(ς\)$
7-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21in\(ς\)$
8-
^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ ¬\(ς\(❝main::1::i❞\) < 10\)\) ⇒ S21T\(ς\)$
9-
^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ ς\(❝main::1::i❞\) < 10\) ⇒ S21\(ς\)$
10-
^\(\d+\) S22 = S21$
11-
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::i❞:=ς\(❝main::1::i❞\) \+ 1\]\)$
12-
^\(\d+\) S24 = S23$
13-
^\(\d+\) S25 = S21T$
6+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S18in\(ς\)$
7+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18in\(ς\)$
8+
^\(\d+\) ∀ ς : state \. \(S18in\(ς\) ∧ ¬\(ς\(❝main::1::i❞\) < 10\)\) ⇒ S18T\(ς\)$
9+
^\(\d+\) ∀ ς : state \. \(S18in\(ς\) ∧ ς\(❝main::1::i❞\) < 10\) ⇒ S18\(ς\)$
10+
^\(\d+\) S19 = S18$
11+
^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝main::1::i❞:=ς\(❝main::1::i❞\) \+ 1\]\)$
12+
^\(\d+\) S21 = S20$
13+
^\(\d+\) S22 = S18T$
1414
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1515
--
1616
--

Diff for: ‎regression/cprover/loops/for2.desc

+6-6
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ for2.c
33
--text --solve --unwind 10 --inline
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S21in\(ς\)$
7-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21in\(ς\)$
8-
^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ ¬\(ς\(❝main::1::1::x❞\) ≠ 10\)\) ⇒ S21T\(ς\)$
9-
^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ ς\(❝main::1::1::x❞\) ≠ 10\) ⇒ S21\(ς\)$
10-
^\(\d+\) S22 = S21$
11-
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::1::x❞:=ς\(❝main::1::1::x❞\) \+ 1\]\)$
6+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S18in\(ς\)$
7+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18in\(ς\)$
8+
^\(\d+\) ∀ ς : state \. \(S18in\(ς\) ∧ ¬\(ς\(❝main::1::1::x❞\) ≠ 10\)\) ⇒ S18T\(ς\)$
9+
^\(\d+\) ∀ ς : state \. \(S18in\(ς\) ∧ ς\(❝main::1::1::x❞\) ≠ 10\) ⇒ S18\(ς\)$
10+
^\(\d+\) S19 = S18$
11+
^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝main::1::1::x❞:=ς\(❝main::1::1::x❞\) \+ 1\]\)$
1212
^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
1313
--
1414
--

Diff for: ‎regression/cprover/loops/while-break1.desc

+9-9
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,15 @@ while-break1.c
33
--text --solve --inline
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. S27\(ς\) ⇒ S21in\(ς\)$
7-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21in\(ς\)$
8-
^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ ¬\(1 ≠ 0\)\) ⇒ S21T\(ς\)$
9-
^\(\d+\) ∀ ς : state \. \(S21in\(ς\) ∧ 1 ≠ 0\) ⇒ S21\(ς\)$
10-
^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) = 0\)\) ⇒ S22T\(ς\)$
11-
^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ς\(❝main::1::x❞\) = 0\) ⇒ S22\(ς\)$
12-
^\(\d+\) ∀ ς : state \. S21T\(ς\) ⇒ S28in\(ς\)$
13-
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S28in\(ς\)$
14-
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S28in\(ς\)$
6+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S18in\(ς\)$
7+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18in\(ς\)$
8+
^\(\d+\) ∀ ς : state \. \(S18in\(ς\) ∧ ¬\(1 ≠ 0\)\) ⇒ S18T\(ς\)$
9+
^\(\d+\) ∀ ς : state \. \(S18in\(ς\) ∧ 1 ≠ 0\) ⇒ S18\(ς\)$
10+
^\(\d+\) ∀ ς : state \. \(S18\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) = 0\)\) ⇒ S19T\(ς\)$
11+
^\(\d+\) ∀ ς : state \. \(S18\(ς\) ∧ ς\(❝main::1::x❞\) = 0\) ⇒ S19\(ς\)$
12+
^\(\d+\) ∀ ς : state \. S18T\(ς\) ⇒ S25in\(ς\)$
13+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S25in\(ς\)$
14+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S25in\(ς\)$
1515
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
1616
--
1717
--

Diff for: ‎regression/cprover/pointers/malloc1.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ malloc1.c
33
--text --solve --inline
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4 \* cast\(10, unsignedbv\[64\]\)\)\]\)$
6+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4 \* cast\(10, unsignedbv\[64\]\)\)\]\)$
77
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
88
--

Diff for: ‎regression/cprover/pointers/pointers0.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ pointers0.c
33
--text --solve --inline --no-safety
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::p❞:=❝main::1::x❞\]\)$
7-
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = ς\(❝main::1::x❞\)\)$
6+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝main::1::p❞:=❝main::1::x❞\]\)$
7+
^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = ς\(❝main::1::x❞\)\)$
88
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
99
--

0 commit comments

Comments
 (0)