Skip to content

Commit c4416c0

Browse files
kroeningkroening
committed
set-encoding
1 parent 8cbe8ef commit c4416c0

Some content is hidden

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

80 files changed

+2540
-3
lines changed

‎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: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
array1.c
3+
4+
^EXIT=0$
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+
--

‎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: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
array2.c
3+
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+
--

‎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");
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+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^program is safe / function main is safe / line .* 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: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
assume1.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
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\]\)$
13+
--

‎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: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
basic1.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
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\)$
11+
--

‎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: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
basic2.c
3+
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+
--

‎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: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
basic3.c
3+
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+
--

‎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: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
basic4.c
3+
4+
^EXIT=0$
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+
--

‎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: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
basic5.c
3+
4+
^EXIT=0$
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+
--

‎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: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
nondet1.c
3+
4+
^EXIT=0$
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+
--

‎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");
7+
__CPROVER_assert(0, "property 2");
8+
}
9+
else
10+
{
11+
__CPROVER_assert(x < 5, "property 3");
12+
__CPROVER_assert(0, "property 4");
13+
}
14+
}

‎regression/cprover/branching/branching1.desc

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
CORE
2+
branching1.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
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$
19+
--

‎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");
11+
__CPROVER_assert(b != (a >= 5), "property 2");
12+
13+
return 0;
14+
}

‎regression/cprover/branching/branching2.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
branching2.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
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$
13+
--

‎regression/cprover/function_calls/call_no_body1.c

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

‎regression/cprover/function_calls/call_no_body1.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
call_no_body1.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet22\]\)$
7+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::x❞:=ς\(❝main::\$tmp::return_value_function_without_body❞\)\]\)$
8+
--

‎regression/cprover/pointers/char_pointers1.c

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

‎regression/cprover/pointers/char_pointers1.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
KNOWNBUG
2+
char_pointers1.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^program is safe / function main is safe / line .* property 1: SUCCESS$
7+
--

‎regression/cprover/pointers/char_pointers2.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
int main()
2+
{
3+
int x = 0x01020304;
4+
char *p = (char *)&x;
5+
6+
// passes on little endinan
7+
__CPROVER_assert(p[0] == 0x04, "property 1");
8+
__CPROVER_assert(p[1] == 0x03, "property 2");
9+
__CPROVER_assert(p[2] == 0x02, "property 3");
10+
__CPROVER_assert(p[3] == 0x01, "property 4");
11+
return 0;
12+
}

‎regression/cprover/pointers/char_pointers2.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
char_pointers2.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
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\)$
16+
--

‎regression/cprover/pointers/pointer_to_local1.c

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
void foo(int *p) __CPROVER_requires(__CPROVER_w_ok(p))
2+
{
3+
int i;
4+
5+
i = 123;
6+
*p = 456; // p cannot point to i as i is local
7+
__CPROVER_assert(i == 123, "property 1"); // should pass
8+
}

‎regression/cprover/pointers/pointer_to_local1.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
KNOWNBUG
2+
pointer_to_local1.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^program is safe / function foo is safe / line .* property 1: SUCCESS$
7+
--

‎regression/cprover/pointers/pointers1.c

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

0 commit comments

Comments
 (0)