Skip to content

Commit 676b359

Browse files
kroeningkroening
committed
fix tests
1 parent c8e3c9e commit 676b359

26 files changed

+137
-137
lines changed

‎regression/cprover/arrays/array1.desc

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ array1.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(19\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[element_address\(❝array❞, 1\):=10\]\)$
7-
^\(20\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[element_address\(❝array❞, 2\):=20\]\)$
8-
^\(21\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(element_address\(❝array❞, 1\)\) = 10\)$
9-
^\(23\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝array❞, 2\)\) = 20\)$
10-
^\(25\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝array❞, 2\)\) = 30\)$
6+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[element_address\(❝array❞, 1\):=10\]\)$
7+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[element_address\(❝array❞, 2\):=20\]\)$
8+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(element_address\(❝array❞, 1\)\) = 10\)$
9+
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝array❞, 2\)\) = 20\)$
10+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝array❞, 2\)\) = 30\)$
1111
--

‎regression/cprover/arrays/array2.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ array2.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(23\) ∀ ς : state \. S23\(ς\) ⇒ \(\(ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S24\(ς\)\)$
7-
^\(24\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$
8-
^\(26\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(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 \. S23\(ς\) ⇒ \(\(ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S24\(ς\)\)$
7+
^\(\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\]\)\)\)\)$
8+
^\(\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\]\)\)\)\)$
99
--

‎regression/cprover/basic/assume1.desc

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ assume1.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^ \(1\) ∀ ς : state \. SInitial\(ς\)$
7-
^ \(2\) S0 = SInitial$
8-
^ \(3\) S1 = S0$
9-
^\(20\) ∀ ς : state \. S20\(ς\) ⇒ \(\(ς\(❝main::1::x❞\) ≥ 10\) ⇒ S21\(ς\)\)$
10-
^\(21\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
11-
^\(23\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
12-
^\(26\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝return'❞:=nondet25\]\)$
6+
^ \(\d+\) ∀ ς : state \. SInitial\(ς\)$
7+
^ \(\d+\) S0 = SInitial$
8+
^ \(\d+\) S1 = S0$
9+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(\(ς\(❝main::1::x❞\) ≥ 10\) ⇒ S21\(ς\)\)$
10+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
11+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
12+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝return'❞:=nondet25\]\)$
1313
--

‎regression/cprover/basic/basic1.desc

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ basic1.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^ \(1\) ∀ ς : state \. SInitial\(ς\)$
7-
^ \(2\) S0 = SInitial$
8-
^\(17\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
9-
^\(20\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
10-
^\(21\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
6+
^ \(\d+\) ∀ ς : state \. SInitial\(ς\)$
7+
^ \(\d+\) S0 = SInitial$
8+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
9+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
10+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
1111
--

‎regression/cprover/basic/basic2.desc

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ basic2.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(17\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
7-
^\(18\) S19 = S18$
8-
^\(19\) S20 = S19$
9-
^\(20\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
10-
^\(21\) S22 = S21$
11-
^\(22\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
6+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
7+
^\(\d+\) S19 = S18$
8+
^\(\d+\) S20 = S19$
9+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
10+
^\(\d+\) S22 = S21$
11+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
1212
--

‎regression/cprover/basic/basic3.desc

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ basic3.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
\(17\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)
7-
\(18\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝y❞:=0\]\)
8-
\(21\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=1\]\)
9-
\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝y❞:=2\]\)
10-
\(23\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝x❞\) = 1\)
6+
\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)
7+
\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝y❞:=0\]\)
8+
\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=1\]\)
9+
\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝y❞:=2\]\)
10+
\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝x❞\) = 1\)
1111
--

‎regression/cprover/basic/basic4.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ basic4.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(17\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
7-
^\(20\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
8-
^\(21\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=2\]\)$
9-
^\(22\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
6+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
7+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
8+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=2\]\)$
9+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
1010
--

‎regression/cprover/basic/basic5.desc

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ basic5.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(21\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$
7-
^\(22\) S23 = S22$
8-
^\(23\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$
9-
^\(24\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$
10-
^\(25\) S25 = S24$
11-
^\(26\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$
6+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$
7+
^\(\d+\) S23 = S22$
8+
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$
9+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$
10+
^\(\d+\) S25 = S24$
11+
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$
1212
--

‎regression/cprover/basic/nondet1.desc

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ nondet1.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(21\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=nondet22\]\)$
7-
^\(22\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$
8-
^\(23\) S23 = S22$
9-
^\(24\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::y❞:=nondet24\]\)$
10-
^\(25\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$
11-
^\(26\) S25 = S24$
12-
^\(27\) ∀ ς : state \. S25\(ς\) ⇒ S26\(ς\[❝return'❞:=0\]\)$
6+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=nondet22\]\)$
7+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$
8+
^\(\d+\) S23 = S22$
9+
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::y❞:=nondet24\]\)$
10+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$
11+
^\(\d+\) S25 = S24$
12+
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26\(ς\[❝return'❞:=0\]\)$
1313
--

‎regression/cprover/branching/branching1.desc

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -3,17 +3,17 @@ branching1.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(20\) ∀ ς : state \. S20\(ς\) ⇒ \(¬\(ς\(❝main::1::x❞\) ≥ 5\) \? S21T\(ς\) : S21\(ς\)\)$
7-
^\(21\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
8-
^\(22\) S22 = S21$
9-
^\(23\) ∀ ς : state \. S22\(ς\) ⇒ \(0 ≠ 0\)$
10-
^\(24\) S23 = S22$
11-
^\(25\) S24 = S23$
12-
^\(26\) ∀ ς : state \. S21T\(ς\) ⇒ \(ς\(❝main::1::x❞\) < 5\)$
13-
^\(27\) S25 = S21T$
14-
^\(28\) ∀ ς : state \. S25\(ς\) ⇒ \(0 ≠ 0\)$
15-
^\(29\) S26 = S25$
16-
^\(30\) ∀ ς : state \. S24\(ς\) ⇒ S27in\(ς\)$
17-
^\(31\) ∀ ς : state \. S26\(ς\) ⇒ S27in\(ς\)$
18-
^\(32\) S27 = S27in$
6+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(¬\(ς\(❝main::1::x❞\) ≥ 5\) \? S21T\(ς\) : S21\(ς\)\)$
7+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
8+
^\(\d+\) S22 = S21$
9+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(0 ≠ 0\)$
10+
^\(\d+\) S23 = S22$
11+
^\(\d+\) S24 = S23$
12+
^\(\d+\) ∀ ς : state \. S21T\(ς\) ⇒ \(ς\(❝main::1::x❞\) < 5\)$
13+
^\(\d+\) S25 = S21T$
14+
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(0 ≠ 0\)$
15+
^\(\d+\) S26 = S25$
16+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S27in\(ς\)$
17+
^\(\d+\) ∀ ς : state \. S26\(ς\) ⇒ S27in\(ς\)$
18+
^\(\d+\) S27 = S27in$
1919
--

‎regression/cprover/branching/branching2.desc

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ branching2.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(21\) ∀ ς : state \. S21\(ς\) ⇒ \(¬\(ς\(❝main::1::a❞\) ≥ 5\) \? S22T\(ς\) : S22\(ς\)\)$
7-
^\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::b❞:=1\]\)$
8-
^\(23\) S24 = S23$
9-
^\(24\) ∀ ς : state \. S22T\(ς\) ⇒ S25\(ς\[❝main::1::b❞:=0\]\)$
10-
^\(25\) ∀ ς : state \. S24\(ς\) ⇒ S26in\(ς\)$
11-
^\(26\) ∀ ς : state \. S25\(ς\) ⇒ S26in\(ς\)$
12-
^\(27\) S26 = S26in$
6+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(¬\(ς\(❝main::1::a❞\) ≥ 5\) \? S22T\(ς\) : S22\(ς\)\)$
7+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::b❞:=1\]\)$
8+
^\(\d+\) S24 = S23$
9+
^\(\d+\) ∀ ς : state \. S22T\(ς\) ⇒ S25\(ς\[❝main::1::b❞:=0\]\)$
10+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S26in\(ς\)$
11+
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26in\(ς\)$
12+
^\(\d+\) S26 = S26in$
1313
--

‎regression/cprover/pointers/char_pointers2.desc

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,14 @@ char_pointers2.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(20\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::x❞:=16909060\]\)$
7-
^\(21\) S22 = S21$
8-
^\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p❞:=cast\(address_of\(ς\(❝main::1::x❞\)\), signedbv\[8\]\*\)\]\)$
9-
^\(23\) ∀ ς : state \. S23\(ς\) ⇒ \(cast\(ς\(ς\(❝main::1::p❞\) \+ cast\(0, signedbv\[64\]\)\), signedbv\[32\]\) = 4\)$
10-
^\(24\) S24 = S23$
11-
^\(25\) ∀ ς : state \. S24\(ς\) ⇒ \(cast\(ς\(ς\(❝main::1::p❞\) \+ cast\(1, signedbv\[64\]\)\), signedbv\[32\]\) = 3\)$
12-
^\(26\) S25 = S24$
13-
^\(27\) ∀ ς : state \. S25\(ς\) ⇒ \(cast\(ς\(ς\(❝main::1::p❞\) \+ cast\(2, signedbv\[64\]\)\), signedbv\[32\]\) = 2\)$
14-
^\(28\) S26 = S25$
15-
^\(29\) ∀ ς : state \. S26\(ς\) ⇒ \(cast\(ς\(ς\(❝main::1::p❞\) \+ cast\(3, signedbv\[64\]\)\), signedbv\[32\]\) = 1\)$
6+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::x❞:=16909060\]\)$
7+
^\(\d+\) S22 = S21$
8+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p❞:=cast\(address_of\(ς\(❝main::1::x❞\)\), signedbv\[8\]\*\)\]\)$
9+
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(cast\(ς\(ς\(❝main::1::p❞\) \+ cast\(0, signedbv\[64\]\)\), signedbv\[32\]\) = 4\)$
10+
^\(\d+\) S24 = S23$
11+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(cast\(ς\(ς\(❝main::1::p❞\) \+ cast\(1, signedbv\[64\]\)\), signedbv\[32\]\) = 3\)$
12+
^\(\d+\) S25 = S24$
13+
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(cast\(ς\(ς\(❝main::1::p❞\) \+ cast\(2, signedbv\[64\]\)\), signedbv\[32\]\) = 2\)$
14+
^\(\d+\) S26 = S25$
15+
^\(\d+\) ∀ ς : state \. S26\(ς\) ⇒ \(cast\(ς\(ς\(❝main::1::p❞\) \+ cast\(3, signedbv\[64\]\)\), signedbv\[32\]\) = 1\)$
1616
--

‎regression/cprover/pointers/pointers1.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ pointers1.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=10\]\)$
7-
^\(23\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝p❞:=address_of\(ς\(❝x❞\)\)\]\)$
8-
^\(24\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝y❞:=ς\(ς\(❝p❞\)\)\]\)$
9-
^\(25\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝y❞\) = 10\)$
6+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=10\]\)$
7+
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝p❞:=address_of\(ς\(❝x❞\)\)\]\)$
8+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝y❞:=ς\(ς\(❝p❞\)\)\]\)$
9+
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝y❞\) = 10\)$
1010
--

‎regression/cprover/pointers/pointers10.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ pointers10.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(21\) ∀ ς : state \. S21\(ς\) ⇒ \(¬\(ς\(❝main::1::p❞\) = address_of\(ς\(❝main::1::x❞\)\)\) \? S22T\(ς\) : S22\(ς\)\)$
7-
^\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[ς\(❝main::1::p❞\):=123\]\)$
8-
^\(23\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 123\)$
6+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(¬\(ς\(❝main::1::p❞\) = address_of\(ς\(❝main::1::x❞\)\)\) \? S22T\(ς\) : S22\(ς\)\)$
7+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[ς\(❝main::1::p❞\):=123\]\)$
8+
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 123\)$
99
--

‎regression/cprover/pointers/pointers2.desc

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ pointers2.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(21\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=10\]\)$
7-
^\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝p❞:=address_of\(ς\(❝x❞\)\)\]\)$
8-
^\(23\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[ς\(❝p❞\):=20\]\)$
9-
^\(24\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝x❞\) = 20\)$
10-
^\(25\) S25 = S24$
11-
^\(26\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$
6+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=10\]\)$
7+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝p❞:=address_of\(ς\(❝x❞\)\)\]\)$
8+
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[ς\(❝p❞\):=20\]\)$
9+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝x❞\) = 20\)$
10+
^\(\d+\) S25 = S24$
11+
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$
1212
--

‎regression/cprover/pointers/pointers3.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ pointers3.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(20\) ∀ ς : state \. S20\(ς\) ⇒ \(\(ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S21\(ς\)\)$
7-
^\(21\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$
6+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(\(ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S21\(ς\)\)$
7+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$
88
--

‎regression/cprover/pointers/pointers4.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ pointers4.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(17\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
7-
^\(21\) ∀ ς : state \. S21\(ς\) ⇒ \(\(ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S22\(ς\)\)$
8-
^\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p❞:=address_of\(ς\(❝x❞\)\)\]\)$
9-
^\(23\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$
6+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
7+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(\(ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S22\(ς\)\)$
8+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p❞:=address_of\(ς\(❝x❞\)\)\]\)$
9+
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$
1010
--

‎regression/cprover/pointers/pointers5.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ pointers5.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(17\) ∀ ς18 : state \. S17\(ς18\) ⇒ S18\(ς18\[❝x❞:=0\]\)$
7-
^\(22\) ∀ ς23 : state \. S22\(ς23\) ⇒ \(\(S22\(❝main::1::p❞\) = S22\(❝main::1::q❞\)\) ⇒ S23\(ς23\)\)$
8-
^\(23\) ∀ ς24 : state \. S23\(ς24\) ⇒ \(ς24\(S23\(❝main::1::p❞\)\) = ς24\(S23\(❝main::1::q❞\)\)\)$
6+
^\(\d+\) ∀ ς18 : state \. S17\(ς18\) ⇒ S18\(ς18\[❝x❞:=0\]\)$
7+
^\(\d+\) ∀ ς23 : state \. S22\(ς23\) ⇒ \(\(S22\(❝main::1::p❞\) = S22\(❝main::1::q❞\)\) ⇒ S23\(ς23\)\)$
8+
^\(\d+\) ∀ ς24 : state \. S23\(ς24\) ⇒ \(ς24\(S23\(❝main::1::p❞\)\) = ς24\(S23\(❝main::1::q❞\)\)\)$
99
--

‎regression/cprover/pointers/pointers6.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ pointers6.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p❞:=address_of\(ς\(❝x❞\)\)\]\)$
7-
\(23\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[ς\(❝main::1::p❞\):=10\]\)$
8-
\(24\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝main::1::q❞:=address_of\(ς\(❝x❞\)\)\]\)$
9-
\(25\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(ς\(❝main::1::q❞\)\) = 10\)$
6+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p❞:=address_of\(ς\(❝x❞\)\)\]\)$
7+
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[ς\(❝main::1::p❞\):=10\]\)$
8+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝main::1::q❞:=address_of\(ς\(❝x❞\)\)\]\)$
9+
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(ς\(❝main::1::q❞\)\) = 10\)$
1010
--

‎regression/cprover/pointers/pointers7.desc

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,13 @@ pointers7.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(17\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝p❞:=NULL\]\)$
7-
^\(18\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝x❞:=0\]\)$
8-
^\(19\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝y❞:=0\]\)$
9-
^\(20\) S21 = S20$
10-
^\(21\) S22 = S21$
11-
^\(22\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=10\]\)$
12-
^\(23\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝p❞:=address_of\(ς\(❝y❞\)\)\]\)$
13-
^\(24\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[ς\(❝p❞\):=20\]\)$
14-
^\(25\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$
6+
^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝p❞:=NULL\]\)$
7+
^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝x❞:=0\]\)$
8+
^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝y❞:=0\]\)$
9+
^\(\d+\) S21 = S20$
10+
^\(\d+\) S22 = S21$
11+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=10\]\)$
12+
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝p❞:=address_of\(ς\(❝y❞\)\)\]\)$
13+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[ς\(❝p❞\):=20\]\)$
14+
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$
1515
--

‎regression/cprover/pointers/pointers8.desc

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ pointers8.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(20\) ∀ ς : state \. S20\(ς\) ⇒ \(¬\(pointer_object\(cast\(ς\(❝main::1::p❞\), empty\*\)\) = pointer_object\(cast\(address_of\(ς\(❝main::1::p❞\)\), empty\*\)\)\) ⇒ S21\(ς\)\)$
7-
^\(21\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[ς\(❝main::1::p❞\):=123\]\)$
8-
^\(22\) S23 = S22$
9-
^\(23\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::p_value❞:=ς\(ς\(❝main::1::p❞\)\)\]\)$
10-
^\(24\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::p_value❞\) = 123\)$
11-
^\(25\) S25 = S24$
12-
^\(26\) ∀ ς : state \. S25\(ς\) ⇒ S26\(ς\[❝return'❞:=0\]\)$
6+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(¬\(pointer_object\(cast\(ς\(❝main::1::p❞\), empty\*\)\) = pointer_object\(cast\(address_of\(ς\(❝main::1::p❞\)\), empty\*\)\)\) ⇒ S21\(ς\)\)$
7+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[ς\(❝main::1::p❞\):=123\]\)$
8+
^\(\d+\) S23 = S22$
9+
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::p_value❞:=ς\(ς\(❝main::1::p❞\)\)\]\)$
10+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::p_value❞\) = 123\)$
11+
^\(\d+\) S25 = S24$
12+
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26\(ς\[❝return'❞:=0\]\)$
1313
--

‎regression/cprover/pointers/pointers9.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ pointers9.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(21\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=123\]\)$
7-
^\(22\) ∀ ς : state \. S22\(ς\) ⇒ \(¬\(ς\(❝main::1::p❞\) = address_of\(ς\(❝main::1::x❞\)\)\) \? S23T\(ς\) : S23\(ς\)\)$
8-
^\(23\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 123\)$
6+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=123\]\)$
7+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(¬\(ς\(❝main::1::p❞\) = address_of\(ς\(❝main::1::x❞\)\)\) \? S23T\(ς\) : S23\(ς\)\)$
8+
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 123\)$
99
--

‎regression/cprover/pointers/struct_pointer1.desc

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ struct_pointer1.c
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^\(20\) ∀ ς : state \. S20\(ς\) ⇒ \(¬\(pointer_object\(cast\(ς\(❝main::1::my_struct_ptr❞\), empty\*\)\) = pointer_object\(cast\(address_of\(ς\(❝main::1::my_struct_ptr❞\)\), empty\*\)\)\) ⇒ S21\(ς\)\)$
7-
^\(21\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[ς\(❝main::1::my_struct_ptr❞\)\.❝data❞:=123\]\)$
8-
^\(22\) S23 = S22$
9-
^\(23\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::my_struct_data❞:=ς\(ς\(❝main::1::my_struct_ptr❞\)\.❝data❞\)\]\)$
10-
^\(24\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::my_struct_data❞\) = 123\)$
6+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ \(¬\(pointer_object\(cast\(ς\(❝main::1::my_struct_ptr❞\), empty\*\)\) = pointer_object\(cast\(address_of\(ς\(❝main::1::my_struct_ptr❞\)\), empty\*\)\)\) ⇒ S21\(ς\)\)$
7+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[ς\(❝main::1::my_struct_ptr❞\)\.❝data❞:=123\]\)$
8+
^\(\d+\) S23 = S22$
9+
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::my_struct_data❞:=ς\(ς\(❝main::1::my_struct_ptr❞\)\.❝data❞\)\]\)$
10+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::my_struct_data❞\) = 123\)$
1111
--

0 commit comments

Comments
 (0)