Skip to content

Commit 8f465ed

Browse files
Martin Brainmartin
Martin Brain
authored and
martin
committed
Lucas' rather fantastic regression tests with flags and status updated to match the refactoring.
Where the current precision is insufficient, the tests are marked FUTURE.
1 parent a8b5fc5 commit 8f465ed

File tree

58 files changed

+694
-16
lines changed

Some content is hidden

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

58 files changed

+694
-16
lines changed

‎regression/goto-analyzer/Makefile

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,3 +12,9 @@ show:
1212
vim -o "$$dir/*.java" "$$dir/*.out"; \
1313
fi; \
1414
done;
15+
16+
clean:
17+
find . -name *.*~ | xargs rm -f
18+
find . -name *.out | xargs rm -f
19+
find . -name *.goto | xargs rm -f
20+
rm -f tests.log

‎regression/goto-analyzer/constant_propagation_01/constant_propagation1.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int i, j=20;
6+
7+
if (j==20)
8+
{
9+
int x=1,y=2,z;
10+
z=x+y;
11+
assert(z==3);
12+
}
13+
14+
}

‎regression/goto-analyzer/constant_propagation_01/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
constant_propagation1.c
3+
--constants --simplify out.goto
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$
7+
^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
8+
--
9+
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int i=0, j=2;
6+
7+
if (i==0)
8+
{
9+
i++;
10+
j++;
11+
}
12+
assert(j!=3);
13+
}

‎regression/goto-analyzer/constant_propagation_02/original

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
Task defaults to --show
2+
Domain defaults to --constants
3+
GOTO-ANALYSER version 5.5 64-bit x86_64 linux

‎regression/goto-analyzer/constant_propagation_02/simplified

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
Reading GOTO program from `out.goto'
2+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
3+
4+
main /* main */
5+
// 0 file constant_propagation_02.c line 5 function main
6+
signed int i;
7+
// 1 file constant_propagation_02.c line 5 function main
8+
i = 0;
9+
// 2 file constant_propagation_02.c line 5 function main
10+
signed int j;
11+
// 3 file constant_propagation_02.c line 5 function main
12+
j = 2;
13+
// 4 file constant_propagation_02.c line 7 function main
14+
IF FALSE THEN GOTO 1
15+
// 5 file constant_propagation_02.c line 9 function main
16+
0 = 1;
17+
// 6 file constant_propagation_02.c line 10 function main
18+
2 = 3;
19+
// 7 no location
20+
1: SKIP
21+
// 8 file constant_propagation_02.c line 12 function main
22+
ASSERT FALSE // assertion j!=3
23+
// 9 file constant_propagation_02.c line 12 function main
24+
GOTO 2
25+
// 10 file constant_propagation_02.c line 12 function main
26+
(void)0;
27+
// 11 no location
28+
2: SKIP
29+
// 12 file constant_propagation_02.c line 13 function main
30+
dead j;
31+
// 13 file constant_propagation_02.c line 13 function main
32+
dead i;
33+
// 14 file constant_propagation_02.c line 13 function main
34+
main#return_value = NONDET(signed int);
35+
// 15 file constant_propagation_02.c line 13 function main
36+
END_FUNCTION
37+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
38+
39+
_start /* _start */
40+
// 16 no location
41+
__CPROVER_initialize();
42+
// 17 file constant_propagation_02.c line 3
43+
main();
44+
// 18 file constant_propagation_02.c line 3
45+
return' = main#return_value;
46+
// 19 file constant_propagation_02.c line 3
47+
dead main#return_value;
48+
// 20 file constant_propagation_02.c line 3
49+
OUTPUT("return", return');
50+
// 21 no location
51+
END_FUNCTION
52+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
53+
54+
__CPROVER_initialize /* __CPROVER_initialize */
55+
// 22 no location
56+
// Labels: __CPROVER_HIDE
57+
SKIP
58+
// 23 file <built-in-additions> line 39
59+
__CPROVER_dead_object = NULL;
60+
// 24 file <built-in-additions> line 38
61+
__CPROVER_deallocated = NULL;
62+
// 25 file <built-in-additions> line 42
63+
__CPROVER_malloc_is_new_array = FALSE;
64+
// 26 file <built-in-additions> line 40
65+
__CPROVER_malloc_object = NULL;
66+
// 27 file <built-in-additions> line 41
67+
__CPROVER_malloc_size = 0ul;
68+
// 28 file <built-in-additions> line 43
69+
__CPROVER_memory_leak = NULL;
70+
// 29 file <built-in-additions> line 31
71+
__CPROVER_next_thread_id = 0ul;
72+
// 30 file <built-in-additions> line 85
73+
__CPROVER_pipe_count = 0u;
74+
// 31 file <built-in-additions> line 65
75+
__CPROVER_rounding_mode = 0;
76+
// 32 file <built-in-additions> line 29
77+
__CPROVER_thread_id = 0ul;
78+
// 33 file <built-in-additions> line 30
79+
__CPROVER_threads_exited = ARRAY_OF(FALSE);
80+
// 34 no location
81+
END_FUNCTION

‎regression/goto-analyzer/constant_propagation_02/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
constant_propagation_02.c
3+
--constants --simplify out.goto
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
7+
^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
8+
--
9+
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int i=0, j=2;
6+
7+
if (i==0)
8+
{
9+
i++;
10+
j++;
11+
}
12+
assert(j==3);
13+
}

‎regression/goto-analyzer/constant_propagation_03/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
constant_propagation_03.c
3+
--constants --simplify out.goto
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
7+
^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
8+
--
9+
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int i=0, j=2;
6+
7+
if (i<50)
8+
{
9+
i++;
10+
j++;
11+
}
12+
assert(j==3);
13+
}

‎regression/goto-analyzer/constant_propagation_04/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
constant_propagation_04.c
3+
--constants --simplify out.goto
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
7+
^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
8+
--
9+
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int i=0, j=2;
6+
7+
if (i<50)
8+
{
9+
i++;
10+
j++;
11+
}
12+
assert(j!=3);
13+
}

‎regression/goto-analyzer/constant_propagation_05/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
constant_propagation_05.c
3+
--constants --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] file constant_propagation_05.c line 12 function main, assertion j!=3: FAILURE (if reachable)$
7+
--
8+
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int i, j=20;
6+
7+
if(i>=20)
8+
assert(i>=10); // success
9+
10+
if(i>=10 && i<=20)
11+
assert(i!=30); // success
12+
13+
if(i>=10 && i<=20)
14+
assert(i!=15); // fails
15+
16+
if(i<1 && i>10)
17+
assert(0); // success
18+
19+
if(i>=10 && j>=i)
20+
assert(j>=10); // success
21+
22+
if(i>=j)
23+
assert(i>=j); // unknown
24+
25+
if(i>10)
26+
assert(i>=11); // success
27+
28+
if(i<=100 && j<i)
29+
assert(j<100); // success
30+
}

‎regression/goto-analyzer/constant_propagation_06/test.desc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
constant_propagation_06.c
3+
--intervals --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] file constant_propagation_06.c line 8 function main, assertion i>=10: SUCCESS$
7+
^\[main.assertion.2\] file constant_propagation_06.c line 11 function main, assertion i!=30: SUCCESS$
8+
^\[main.assertion.3\] file constant_propagation_06.c line 14 function main, assertion i!=15: UNKNOWN$
9+
^\[main.assertion.4\] file constant_propagation_06.c line 17 function main, assertion 0: SUCCESS$
10+
^\[main.assertion.5\] file constant_propagation_06.c line 20 function main, assertion j>=10: SUCCESS$
11+
^\[main.assertion.6\] file constant_propagation_06.c line 23 function main, assertion i>=j: UNKNOWN$
12+
^\[main.assertion.7\] file constant_propagation_06.c line 26 function main, assertion i>=11: SUCCESS$
13+
^\[main.assertion.8\] file constant_propagation_06.c line 29 function main, assertion j<100: SUCCESS$
14+
--
15+
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int i=0, j=2;
6+
7+
while (i<50)
8+
{
9+
i++;
10+
j++;
11+
}
12+
assert(i<51);
13+
}
14+

‎regression/goto-analyzer/constant_propagation_07/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
constant_propagation_07.c
3+
--constants --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<51: UNKNOWN$
7+
--
8+
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int i=0, j=2;
6+
7+
while (i<=50)
8+
{
9+
i++;
10+
j++;
11+
}
12+
assert(i<50);
13+
assert(i<51);
14+
assert(i<52);
15+
}
16+

‎regression/goto-analyzer/constant_propagation_08/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
FUTURE
2+
constant_propagation_08.c
3+
--intervals --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] file constant_propagation_08.c line 12 function main, assertion i<50: UNKNOWN$
7+
^\[main.assertion.2\] file constant_propagation_08.c line 13 function main, assertion i<51: UNKNOWN$
8+
^\[main.assertion.3\] file constant_propagation_08.c line 14 function main, assertion i<52: SUCCESS$
9+
--
10+
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int i=0, j=2;
6+
7+
while (i<=50)
8+
{
9+
i++;
10+
j++;
11+
}
12+
assert(j<52);
13+
}
14+

‎regression/goto-analyzer/constant_propagation_09/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
constant_propagation_09.c
3+
--intervals --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
******** Function main
7+
^\[main.assertion.1\] file constant_propagation_09.c line 12 function main, assertion j<52: UNKNOWN$
8+
--
9+
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
#include <assert.h>
2+
int main()
3+
{
4+
signed int i;
5+
signed int j;
6+
i = 0;
7+
if(!(i >= 2))
8+
{
9+
j = j + 1;
10+
i = i + 1;
11+
if(!(i >= 2))
12+
{
13+
j = j + 1;
14+
i = i + 1;
15+
if(!(i >= 2))
16+
{
17+
j = j + 1;
18+
i = i + 1;
19+
}
20+
assert(!(i < 2));
21+
}
22+
}
23+
return 0;
24+
}
25+

‎regression/goto-analyzer/constant_propagation_10/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
constant_propagation_10.c
3+
--constants --simplify out.goto
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^SIMPLIFIED: assert: 1, assume: 0, goto: 4, assigns: 10, function calls: 0$
7+
^UNMODIFIED: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
8+
--
9+
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
#include <assert.h>
2+
int main()
3+
{
4+
int a[2];
5+
int i;
6+
i = 0;
7+
8+
if (i==0)
9+
a[0]=1;
10+
else
11+
a[1]=2;
12+
13+
assert(a[0]==1 || a[1]==2);
14+
15+
return 0;
16+
}
17+

0 commit comments

Comments
 (0)