Skip to content

Commit e0801da

Browse files
kroeningkroening
committed
state encoding
1 parent c25f6fb commit e0801da

File tree

275 files changed

+6401
-26
lines changed

Some content is hidden

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

275 files changed

+6401
-26
lines changed

‎.clang-format-ignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
11
jbmc/src/miniz/miniz.cpp
2+
src/cprover/wcwidth.c
23
src/nonstd/optional.hpp
34
unit/catch/catch.hpp

‎regression/cprover/Makefile

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
default: tests.log
2+
3+
include ../../src/config.inc
4+
include ../../src/common
5+
6+
test:
7+
@../test.pl -e -p -c '../../../src/cprover/cprover'
8+
9+
tests.log:
10+
@../test.pl -e -p -c '../../../src/cprover/cprover'
11+
12+
clean:
13+
$(RM) tests.log

‎regression/cprover/arrays/array1.c

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
int array[10];
2+
3+
int main()
4+
{
5+
array[1l] = 10;
6+
array[2l] = 20;
7+
__CPROVER_assert(array[1l] == 10, "property 1"); // passes
8+
__CPROVER_assert(array[2l] == 20, "property 2"); // passes
9+
__CPROVER_assert(array[2l] == 30, "property 3"); // fails
10+
}

‎regression/cprover/arrays/array1.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
array1.c
3+
--text --solve
4+
^EXIT=10$
5+
^SIGNAL=0$
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\)$
11+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
12+
^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
13+
^\[main\.assertion\.3\] line \d+ property 3: REFUTED$
14+
--

‎regression/cprover/arrays/array2.c

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int main()
2+
{
3+
int array[10];
4+
int i, j, k;
5+
__CPROVER_assume(i == j);
6+
__CPROVER_assert(array[i] == array[j], "property 1"); // passes
7+
__CPROVER_assert(array[i] == array[k], "property 2"); // fails
8+
}

‎regression/cprover/arrays/array2.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
KNOWNBUG
2+
array2.c
3+
--text --solve
4+
^EXIT=0$
5+
^SIGNAL=0$
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\]\)\)\)\)$
9+
^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
10+
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
11+
--

‎regression/cprover/arrays/array4.c

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
int main()
2+
{
3+
int a[100];
4+
int *p = a;
5+
__CPROVER_assert(p[23] == a[23], "property 1"); // should pass
6+
return 0;
7+
}

‎regression/cprover/arrays/array4.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
KNOWNBUG
2+
array4.c
3+
--text --solve
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
7+
--

‎regression/cprover/basic/assume1.c

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int main()
2+
{
3+
int x;
4+
5+
__CPROVER_assume(x >= 10);
6+
__CPROVER_assert(x >= 5, "property 1"); // should pass
7+
__CPROVER_assert(x >= 15, "property 2"); // should fail
8+
}

‎regression/cprover/basic/assume1.desc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
assume1.c
3+
--text --solve
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^ \(\d+\) ∀ ς : state \. true ⇒ 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\]\)$
13+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
14+
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
15+
--

‎regression/cprover/basic/basic1.c

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int x;
2+
3+
int main()
4+
{
5+
x = 1;
6+
__CPROVER_assert(x == 1, "property 1");
7+
return 0;
8+
}

‎regression/cprover/basic/basic1.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
basic1.c
3+
--text --solve
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^ \(\d+\) ∀ ς : state \. true ⇒ 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\)$
11+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
12+
--

‎regression/cprover/basic/basic2.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
int x;
2+
3+
int main()
4+
{
5+
x = 1;
6+
;
7+
__CPROVER_assert(x == 1, "property 1");
8+
return 0;
9+
}

‎regression/cprover/basic/basic2.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
basic2.c
3+
--text --solve
4+
^EXIT=0$
5+
^SIGNAL=0$
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\)$
12+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
13+
--

‎regression/cprover/basic/basic3.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
int x, y;
2+
3+
int main()
4+
{
5+
x = 1;
6+
y = 2;
7+
__CPROVER_assert(x == 1, "property 1");
8+
return 0;
9+
}

‎regression/cprover/basic/basic3.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
basic3.c
3+
--text --solve
4+
^EXIT=0$
5+
^SIGNAL=0$
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\)
11+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
12+
--

‎regression/cprover/basic/basic4.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
int x;
2+
3+
int main()
4+
{
5+
x = 1;
6+
x = 2;
7+
__CPROVER_assert(x == 1, "property 1");
8+
return 0;
9+
}

‎regression/cprover/basic/basic4.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
basic4.c
3+
--text --solve
4+
^EXIT=10$
5+
^SIGNAL=0$
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\)$
10+
^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
11+
--

‎regression/cprover/basic/basic5.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
int main()
2+
{
3+
int x;
4+
__CPROVER_bool c1 = (x >= 10);
5+
__CPROVER_bool c2 = (x >= 5);
6+
__CPROVER_assert(c1 ==> c2, "property 1"); // passes
7+
__CPROVER_assert(c2 ==> c1, "property 2"); // fails
8+
return 0;
9+
}

‎regression/cprover/basic/basic5.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
basic5.c
3+
--text --solve
4+
^EXIT=10$
5+
^SIGNAL=0$
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❞\)\)$
12+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
13+
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
14+
--

‎regression/cprover/basic/basic6.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
int x;
2+
3+
int main()
4+
{
5+
x = 1;
6+
x++;
7+
x++;
8+
x++;
9+
x++;
10+
__CPROVER_assert(x == 5, "property 1");
11+
return 0;
12+
}

‎regression/cprover/basic/basic6.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
basic6.c
3+
--text --solve
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\(23\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
7+
^\(24\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
8+
^\(25\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
9+
^\(26\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
10+
^\(27\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
11+
^\(28\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 5\)$
12+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
13+
--

‎regression/cprover/basic/nondet1.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
int nondet_int();
2+
3+
int main()
4+
{
5+
int x, y;
6+
7+
x = nondet_int();
8+
__CPROVER_assert(x == 20, "property 1"); // fails
9+
10+
y = nondet_int();
11+
__CPROVER_assert(x == y, "property 2"); // fails
12+
13+
return 0;
14+
}

‎regression/cprover/basic/nondet1.desc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
nondet1.c
3+
--text --solve
4+
^EXIT=10$
5+
^SIGNAL=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\]\)$
13+
^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
14+
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
15+
--

‎regression/cprover/branching/branching1.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
int main()
2+
{
3+
int x;
4+
if(x >= 5)
5+
{
6+
__CPROVER_assert(x >= 5, "property 1"); // should pass
7+
__CPROVER_assert(0, "property 2"); // should fail
8+
}
9+
else
10+
{
11+
__CPROVER_assert(x < 5, "property 3"); // should pass
12+
__CPROVER_assert(0, "property 4"); // should fail
13+
}
14+
}

‎regression/cprover/branching/branching1.desc

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
CORE
2+
branching1.c
3+
--text --solve
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) ≥ 5\)\) ⇒ S21T\(\ς\)$
7+
^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 5\) ⇒ S21\(ς\)$
8+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
9+
^\(\d+\) S22 = S21$
10+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(0 ≠ 0\)$
11+
^\(\d+\) S23 = S22$
12+
^\(\d+\) S24 = S23$
13+
^\(\d+\) ∀ ς : state \. S21T\(ς\) ⇒ \(ς\(❝main::1::x❞\) < 5\)$
14+
^\(\d+\) S25 = S21T$
15+
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(0 ≠ 0\)$
16+
^\(\d+\) S26 = S25$
17+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S27in\(ς\)$
18+
^\(\d+\) ∀ ς : state \. S26\(ς\) ⇒ S27in\(ς\)$
19+
^\(\d+\) S27 = S27in$
20+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
21+
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
22+
^\[main\.assertion\.3\] line \d+ property 3: SUCCESS$
23+
^\[main\.assertion\.4\] line \d+ property 4: REFUTED$
24+
--

‎regression/cprover/branching/branching2.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
int main()
2+
{
3+
int a, b;
4+
5+
if(a >= 5)
6+
b = 1;
7+
else
8+
b = 0;
9+
10+
__CPROVER_assert(b == (a >= 5), "property 1"); // should pass
11+
__CPROVER_assert(b != (a >= 5), "property 2"); // should fail
12+
13+
return 0;
14+
}

‎regression/cprover/branching/branching2.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
branching2.c
3+
--text --solve
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ¬\(ς\(❝main::1::a❞\) ≥ 5\)\) ⇒ S22T\(ς\)$
7+
^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ς\(❝main::1::a❞\) ≥ 5\) ⇒ S22\(ς\)$
8+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::b❞:=1\]\)$
9+
^\(\d+\) S24 = S23$
10+
^\(\d+\) ∀ ς : state \. S22T\(ς\) ⇒ S25\(ς\[❝main::1::b❞:=0\]\)$
11+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S26in\(ς\)$
12+
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26in\(ς\)$
13+
^\(\d+\) S26 = S26in$
14+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
15+
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
16+
--

‎regression/cprover/contracts/check_assigns1.c

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
int global;
2+
3+
void my_function1(void)
4+
__CPROVER_assigns(global) // passes
5+
{
6+
global = 10;
7+
}
8+
9+
void my_function2(int parameter)
10+
__CPROVER_assigns() // fails
11+
{
12+
global = 10;
13+
}
14+
15+
void my_function3(int *pointer)
16+
__CPROVER_requires(__CPROVER_w_ok(pointer))
17+
__CPROVER_assigns(*pointer) // passes
18+
{
19+
*pointer = 10;
20+
}

‎regression/cprover/contracts/check_assigns1.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
check_assigns1.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^program is safe / function my_function1 is safe: SUCCESS$
7+
^program is safe / function my_function2 is safe / assigns clause line .*: REFUTED$
8+
^program is safe / function my_function3 is safe / dereference line .*: SUCCESS$
9+
--

0 commit comments

Comments
 (0)