Skip to content

Commit ceaafdf

Browse files
Petr BauchPetr Bauch
Petr Bauch
authored and
Petr Bauch
committed
Add regression tests
For global int, global struct, multiple snapshot-ed symbols, multiple havoc-ed symbols.
1 parent fce288d commit ceaafdf

File tree

8 files changed

+676
-0
lines changed

8 files changed

+676
-0
lines changed

‎regression/goto-harness/havoc-global-int-01/main.c

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

‎regression/goto-harness/havoc-global-int-01/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-location main:0 --havoc-variables x
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] line [0-9]+ assertion x == 1: FAILURE
7+
--
8+
^warning: ignoring

‎regression/goto-harness/havoc-global-int-02/main.c

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
#include <assert.h>
2+
3+
unsigned int x;
4+
unsigned int y;
5+
6+
unsigned int nondet_int()
7+
{
8+
unsigned int z;
9+
return z;
10+
}
11+
12+
void checkpoint()
13+
{
14+
}
15+
16+
unsigned int complex_function_which_returns_one()
17+
{
18+
unsigned int i = 0;
19+
while(++i < 1000001)
20+
{
21+
if(nondet_int() && ((i & 1) == 1))
22+
break;
23+
}
24+
return i & 1;
25+
}
26+
27+
void fill_array(unsigned int *arr, unsigned int size)
28+
{
29+
for(unsigned int i = 0; i < size; i++)
30+
arr[i] = nondet_int();
31+
}
32+
33+
unsigned int array_sum(unsigned int *arr, unsigned int size)
34+
{
35+
unsigned int sum = 0;
36+
for(unsigned int i = 0; i < size; i++)
37+
sum += arr[i];
38+
return sum;
39+
}
40+
41+
const unsigned int array_size = 100000;
42+
43+
int main()
44+
{
45+
x = complex_function_which_returns_one();
46+
unsigned int large_array[array_size];
47+
fill_array(large_array, array_size);
48+
y = array_sum(large_array, array_size);
49+
checkpoint();
50+
assert(y + 2 > y); //y is nondet -- may overflow
51+
assert(0);
52+
return 0;
53+
}

‎regression/goto-harness/havoc-global-int-02/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-location main:9 --havoc-variables y
4+
^\[main.assertion.1\] line \d+ assertion y \+ 2 > y: FAILURE$
5+
^\[main.assertion.2\] line \d+ assertion 0: FAILURE$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring

‎regression/goto-harness/havoc-global-struct/main.c

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

‎regression/goto-harness/havoc-global-struct/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-location main:3 --havoc-variables simple
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] line \d+ assertion simple.j > simple.i: FAILURE$
7+
--
8+
^warning: ignoring

‎regression/goto-harness/load-snapshot-json-snapshots/global-int-x-y-snapshot.json

Lines changed: 212 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,212 @@
1+
{
2+
"symbolTable": {
3+
"__CPROVER_size_t": {
4+
"baseName": "__CPROVER_size_t",
5+
"isAuxiliary": false,
6+
"isExported": false,
7+
"isExtern": false,
8+
"isFileLocal": true,
9+
"isInput": false,
10+
"isLvalue": false,
11+
"isMacro": true,
12+
"isOutput": false,
13+
"isParameter": false,
14+
"isProperty": false,
15+
"isStateVar": false,
16+
"isStaticLifetime": false,
17+
"isThreadLocal": true,
18+
"isType": true,
19+
"isVolatile": false,
20+
"isWeak": false,
21+
"location": {
22+
"id": "",
23+
"namedSub": {
24+
"file": {
25+
"id": "<built-in-additions>"
26+
},
27+
"line": {
28+
"id": "1"
29+
},
30+
"working_directory": {
31+
"id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer"
32+
}
33+
}
34+
},
35+
"mode": "C",
36+
"module": "main",
37+
"name": "__CPROVER_size_t",
38+
"prettyName": "__CPROVER_size_t",
39+
"prettyType": "__CPROVER_size_t",
40+
"prettyValue": "",
41+
"type": {
42+
"id": "unsignedbv",
43+
"namedSub": {
44+
"#c_type": {
45+
"id": "unsigned_long_int"
46+
},
47+
"#source_location": {
48+
"id": "",
49+
"namedSub": {
50+
"file": {
51+
"id": "<built-in-additions>"
52+
},
53+
"line": {
54+
"id": "1"
55+
},
56+
"working_directory": {
57+
"id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer"
58+
}
59+
}
60+
},
61+
"#typedef": {
62+
"id": "__CPROVER_size_t"
63+
},
64+
"width": {
65+
"id": "64"
66+
}
67+
}
68+
},
69+
"value": {
70+
"id": "nil"
71+
}
72+
},
73+
"x": {
74+
"baseName": "x",
75+
"isAuxiliary": false,
76+
"isExported": false,
77+
"isExtern": false,
78+
"isFileLocal": false,
79+
"isInput": false,
80+
"isLvalue": true,
81+
"isMacro": false,
82+
"isOutput": false,
83+
"isParameter": false,
84+
"isProperty": false,
85+
"isStateVar": false,
86+
"isStaticLifetime": true,
87+
"isThreadLocal": false,
88+
"isType": false,
89+
"isVolatile": false,
90+
"isWeak": false,
91+
"location": {
92+
"id": "",
93+
"namedSub": {
94+
"file": {
95+
"id": "main.c"
96+
},
97+
"line": {
98+
"id": "3"
99+
},
100+
"working_directory": {
101+
"id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer"
102+
}
103+
}
104+
},
105+
"mode": "C",
106+
"module": "main",
107+
"name": "x",
108+
"prettyName": "x",
109+
"prettyType": "unsigned int",
110+
"prettyValue": "1u",
111+
"type": {
112+
"id": "unsignedbv",
113+
"namedSub": {
114+
"#c_type": {
115+
"id": "unsigned_int"
116+
},
117+
"width": {
118+
"id": "32"
119+
}
120+
}
121+
},
122+
"value": {
123+
"id": "constant",
124+
"namedSub": {
125+
"type": {
126+
"id": "unsignedbv",
127+
"namedSub": {
128+
"#c_type": {
129+
"id": "unsigned_int"
130+
},
131+
"width": {
132+
"id": "32"
133+
}
134+
}
135+
},
136+
"value": {
137+
"id": "1"
138+
}
139+
}
140+
}
141+
},
142+
"y": {
143+
"baseName": "y",
144+
"isAuxiliary": false,
145+
"isExported": false,
146+
"isExtern": false,
147+
"isFileLocal": false,
148+
"isInput": false,
149+
"isLvalue": true,
150+
"isMacro": false,
151+
"isOutput": false,
152+
"isParameter": false,
153+
"isProperty": false,
154+
"isStateVar": false,
155+
"isStaticLifetime": true,
156+
"isThreadLocal": false,
157+
"isType": false,
158+
"isVolatile": false,
159+
"isWeak": false,
160+
"location": {
161+
"id": "",
162+
"namedSub": {
163+
"file": {
164+
"id": "main.c"
165+
},
166+
"line": {
167+
"id": "4"
168+
},
169+
"working_directory": {
170+
"id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer"
171+
}
172+
}
173+
},
174+
"mode": "C",
175+
"module": "main",
176+
"name": "y",
177+
"prettyName": "y",
178+
"prettyType": "unsigned int",
179+
"prettyValue": "0u",
180+
"type": {
181+
"id": "unsignedbv",
182+
"namedSub": {
183+
"#c_type": {
184+
"id": "unsigned_int"
185+
},
186+
"width": {
187+
"id": "32"
188+
}
189+
}
190+
},
191+
"value": {
192+
"id": "constant",
193+
"namedSub": {
194+
"type": {
195+
"id": "unsignedbv",
196+
"namedSub": {
197+
"#c_type": {
198+
"id": "unsigned_int"
199+
},
200+
"width": {
201+
"id": "32"
202+
}
203+
}
204+
},
205+
"value": {
206+
"id": "0"
207+
}
208+
}
209+
}
210+
}
211+
}
212+
}

0 commit comments

Comments
 (0)