Skip to content

Commit fb5eef9

Browse files
Petr BauchPetr Bauch
Petr Bauch
authored and
Petr Bauch
committed
Add regression tests
At this point the JSON files could be generated as well.
1 parent 4849d70 commit fb5eef9

File tree

21 files changed

+3594
-0
lines changed

21 files changed

+3594
-0
lines changed

‎regression/goto-harness/pointer_01/main.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
#include <assert.h>
2+
3+
int x;
4+
int *p;
5+
6+
//not run here: it's what the snapshot should contain
7+
void initialize()
8+
{
9+
x = 3;
10+
p = &x;
11+
}
12+
13+
int main()
14+
{
15+
// initialize();
16+
assert(*p == x);
17+
}

‎regression/goto-harness/pointer_01/pointer_01.json

Lines changed: 292 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,292 @@
1+
[
2+
{
3+
"program": "MEMORY-ANALYZER 5.11 (cbmc-5.11-2090-g25aeb6e0f-dirty)"
4+
},
5+
{
6+
"symbolTable": {
7+
"x": {
8+
"baseName": "x",
9+
"isAuxiliary": false,
10+
"isExported": false,
11+
"isExtern": false,
12+
"isFileLocal": false,
13+
"isInput": false,
14+
"isLvalue": true,
15+
"isMacro": false,
16+
"isOutput": false,
17+
"isParameter": false,
18+
"isProperty": false,
19+
"isStateVar": false,
20+
"isStaticLifetime": true,
21+
"isThreadLocal": false,
22+
"isType": false,
23+
"isVolatile": false,
24+
"isWeak": false,
25+
"location": {
26+
"id": "",
27+
"namedSub": {
28+
"file": {
29+
"id": "main.c"
30+
},
31+
"function": {
32+
"id": ""
33+
},
34+
"line": {
35+
"id": "5"
36+
},
37+
"working_directory": {
38+
"id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer/pointer_01"
39+
}
40+
}
41+
},
42+
"mode": "C",
43+
"module": "main",
44+
"name": "x",
45+
"prettyName": "x",
46+
"prettyType": "signed int",
47+
"prettyValue": "3",
48+
"type": {
49+
"id": "signedbv",
50+
"namedSub": {
51+
"#c_type": {
52+
"id": "signed_int"
53+
},
54+
"width": {
55+
"id": "32"
56+
}
57+
}
58+
},
59+
"value": {
60+
"id": "constant",
61+
"namedSub": {
62+
"type": {
63+
"id": "signedbv",
64+
"namedSub": {
65+
"#c_type": {
66+
"id": "signed_int"
67+
},
68+
"width": {
69+
"id": "32"
70+
}
71+
}
72+
},
73+
"value": {
74+
"id": "3"
75+
}
76+
}
77+
}
78+
},
79+
"__CPROVER_size_t": {
80+
"baseName": "__CPROVER_size_t",
81+
"isAuxiliary": false,
82+
"isExported": false,
83+
"isExtern": false,
84+
"isFileLocal": true,
85+
"isInput": false,
86+
"isLvalue": false,
87+
"isMacro": true,
88+
"isOutput": false,
89+
"isParameter": false,
90+
"isProperty": false,
91+
"isStateVar": false,
92+
"isStaticLifetime": false,
93+
"isThreadLocal": true,
94+
"isType": true,
95+
"isVolatile": false,
96+
"isWeak": false,
97+
"location": {
98+
"id": "",
99+
"namedSub": {
100+
"file": {
101+
"id": "<built-in-additions>"
102+
},
103+
"line": {
104+
"id": "1"
105+
},
106+
"working_directory": {
107+
"id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer/pointer_01"
108+
}
109+
}
110+
},
111+
"mode": "C",
112+
"module": "main",
113+
"name": "__CPROVER_size_t",
114+
"prettyName": "__CPROVER_size_t",
115+
"prettyType": "__CPROVER_size_t",
116+
"prettyValue": "",
117+
"type": {
118+
"id": "unsignedbv",
119+
"namedSub": {
120+
"#c_type": {
121+
"id": "unsigned_long_int"
122+
},
123+
"#source_location": {
124+
"id": "",
125+
"namedSub": {
126+
"file": {
127+
"id": "<built-in-additions>"
128+
},
129+
"line": {
130+
"id": "1"
131+
},
132+
"working_directory": {
133+
"id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer/pointer_01"
134+
}
135+
}
136+
},
137+
"#typedef": {
138+
"id": "__CPROVER_size_t"
139+
},
140+
"width": {
141+
"id": "64"
142+
}
143+
}
144+
},
145+
"value": {
146+
"id": "nil"
147+
}
148+
},
149+
"p": {
150+
"baseName": "p",
151+
"isAuxiliary": false,
152+
"isExported": false,
153+
"isExtern": false,
154+
"isFileLocal": false,
155+
"isInput": false,
156+
"isLvalue": true,
157+
"isMacro": false,
158+
"isOutput": false,
159+
"isParameter": false,
160+
"isProperty": false,
161+
"isStateVar": false,
162+
"isStaticLifetime": true,
163+
"isThreadLocal": false,
164+
"isType": false,
165+
"isVolatile": false,
166+
"isWeak": false,
167+
"location": {
168+
"id": "",
169+
"namedSub": {
170+
"file": {
171+
"id": "main.c"
172+
},
173+
"function": {
174+
"id": ""
175+
},
176+
"line": {
177+
"id": "6"
178+
},
179+
"working_directory": {
180+
"id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer/pointer_01"
181+
}
182+
}
183+
},
184+
"mode": "C",
185+
"module": "main",
186+
"name": "p",
187+
"prettyName": "p",
188+
"prettyType": "signed int *",
189+
"prettyValue": "&((signed int)x)",
190+
"type": {
191+
"id": "pointer",
192+
"namedSub": {
193+
"#source_location": {
194+
"id": "",
195+
"namedSub": {
196+
"file": {
197+
"id": "main.c"
198+
},
199+
"function": {
200+
"id": ""
201+
},
202+
"line": {
203+
"id": "6"
204+
},
205+
"working_directory": {
206+
"id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer/pointer_01"
207+
}
208+
}
209+
},
210+
"width": {
211+
"id": "64"
212+
}
213+
},
214+
"sub": [
215+
{
216+
"id": "signedbv",
217+
"namedSub": {
218+
"#c_type": {
219+
"id": "signed_int"
220+
},
221+
"width": {
222+
"id": "32"
223+
}
224+
}
225+
}
226+
]
227+
},
228+
"value": {
229+
"id": "address_of",
230+
"namedSub": {
231+
"type": {
232+
"id": "pointer",
233+
"namedSub": {
234+
"width": {
235+
"id": "64"
236+
}
237+
},
238+
"sub": [
239+
{
240+
"id": "signedbv",
241+
"namedSub": {
242+
"#c_type": {
243+
"id": "signed_int"
244+
},
245+
"width": {
246+
"id": "32"
247+
}
248+
}
249+
}
250+
]
251+
}
252+
},
253+
"sub": [
254+
{
255+
"id": "typecast",
256+
"namedSub": {
257+
"type": {
258+
"id": "signedbv",
259+
"namedSub": {
260+
"#c_type": {
261+
"id": "signed_int"
262+
},
263+
"width": {
264+
"id": "32"
265+
}
266+
}
267+
}
268+
},
269+
"sub": [
270+
{
271+
"id": "symbol",
272+
"namedSub": {
273+
"identifier": {
274+
"id": "x"
275+
},
276+
"type": {
277+
"id": ""
278+
}
279+
}
280+
}
281+
]
282+
}
283+
]
284+
}
285+
}
286+
}
287+
},
288+
{
289+
"messageText": "",
290+
"messageType": "STATUS-MESSAGE"
291+
}
292+
]

‎regression/goto-harness/pointer_01/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 pointer_01.json --initial-location main:0
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] line [0-9]+ assertion \*p == x: SUCCESS
7+
VERIFICATION SUCCESSFUL
8+
--
9+
^warning: ignoring

‎regression/goto-harness/pointer_02/main.c

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
#include <assert.h>
2+
#include <malloc.h>
3+
4+
int x;
5+
int *p1;
6+
int *p2;
7+
int *p3;
8+
9+
void initialize()
10+
{
11+
x = 3;
12+
p1 = malloc(sizeof(int));
13+
p3 = malloc(sizeof(int));
14+
p2 = &x;
15+
}
16+
17+
void checkpoint()
18+
{
19+
}
20+
21+
int main()
22+
{
23+
//initialize();
24+
//checkpoint();
25+
26+
assert(*p2 == x);
27+
assert(p1 != p2);
28+
assert(p1 != p3);
29+
assert(*p1 != x);
30+
*p1 = x;
31+
assert(*p1 == x);
32+
}

0 commit comments

Comments
 (0)