Skip to content

Commit d5c94a8

Browse files
danpoePetr Bauch
danpoe
authored and
Petr Bauch
committed
Squashed commits from prerequisite PR #4150 - Do not review
1 parent 3e19f36 commit d5c94a8

File tree

27 files changed

+920
-2
lines changed

27 files changed

+920
-2
lines changed

‎regression/goto-harness/chain.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,10 @@ if [ -e "${name}-mod.gb" ] ; then
2323
rm -f "${name}-mod.gb"
2424
fi
2525

26+
2627
# `# some comment` is an inline comment - basically, cause bash to execute an empty command
2728

29+
$cbmc --show-goto-functions "${name}.gb"
2830
$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args}
2931
$cbmc --function $entry_point "${name}-mod.gb" \
3032
--pointer-check `# because we want to see out of bounds errors` \

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

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
{
2+
"symbolTable": {
3+
"x": {
4+
"baseName": "x",
5+
"isAuxiliary": false,
6+
"isExported": false,
7+
"isExtern": false,
8+
"isFileLocal": false,
9+
"isInput": false,
10+
"isLvalue": true,
11+
"isMacro": false,
12+
"isOutput": false,
13+
"isParameter": false,
14+
"isProperty": false,
15+
"isStateVar": false,
16+
"isStaticLifetime": true,
17+
"isThreadLocal": false,
18+
"isType": false,
19+
"isVolatile": false,
20+
"isWeak": false,
21+
"location": {},
22+
"mode": "C",
23+
"module": "main",
24+
"name": "x",
25+
"prettyName": "x",
26+
"type": {
27+
"id": "signedbv",
28+
"namedSub": {
29+
"#c_type": {
30+
"id": "signed_int"
31+
},
32+
"width": {
33+
"id": "32"
34+
}
35+
}
36+
},
37+
"value": {
38+
"id": "constant",
39+
"namedSub": {
40+
"#base": {
41+
"id": "10"
42+
},
43+
"#source_location": {},
44+
"type": {
45+
"id": "signedbv",
46+
"namedSub": {
47+
"#c_type": {
48+
"id": "signed_int"
49+
},
50+
"width": {
51+
"id": "32"
52+
}
53+
}
54+
},
55+
"value": {
56+
"id": "1"
57+
}
58+
}
59+
}
60+
}
61+
}
62+
}

‎regression/goto-harness/load-snapshot-recursive-static-global-int-01/main.c

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
int x;
2+
int flag;
3+
4+
int main()
5+
{
6+
x = 0;
7+
8+
assert(flag != 0 || x == 1);
9+
assert(flag != 1 || x == 0);
10+
11+
if(flag == 0)
12+
{
13+
flag = 1;
14+
main();
15+
}
16+
17+
return 0;
18+
}

‎regression/goto-harness/load-snapshot-recursive-static-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:1
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
VERIFICATION SUCCESSFUL
7+
--
8+
^warning: ignoring

‎regression/goto-harness/load-snapshot-static-global-array-01/main.c

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

‎regression/goto-harness/load-snapshot-static-global-array-01/snapshot.json

Lines changed: 181 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,181 @@
1+
{
2+
"symbolTable": {
3+
"x": {
4+
"baseName": "x",
5+
"isAuxiliary": false,
6+
"isExported": false,
7+
"isExtern": false,
8+
"isFileLocal": false,
9+
"isInput": false,
10+
"isLvalue": true,
11+
"isMacro": false,
12+
"isOutput": false,
13+
"isParameter": false,
14+
"isProperty": false,
15+
"isStateVar": false,
16+
"isStaticLifetime": true,
17+
"isThreadLocal": false,
18+
"isType": false,
19+
"isVolatile": false,
20+
"isWeak": false,
21+
"location": {},
22+
"mode": "C",
23+
"module": "test",
24+
"name": "x",
25+
"prettyName": "x",
26+
"type": {
27+
"id": "array",
28+
"namedSub": {
29+
"#source_location": {},
30+
"size": {
31+
"id": "constant",
32+
"namedSub": {
33+
"type": {
34+
"id": "signedbv",
35+
"namedSub": {
36+
"#c_type": {
37+
"id": "signed_long_int"
38+
},
39+
"width": {
40+
"id": "64"
41+
}
42+
}
43+
},
44+
"value": {
45+
"id": "3"
46+
}
47+
}
48+
}
49+
},
50+
"sub": [
51+
{
52+
"id": "signedbv",
53+
"namedSub": {
54+
"#c_type": {
55+
"id": "signed_int"
56+
},
57+
"width": {
58+
"id": "32"
59+
}
60+
}
61+
}
62+
]
63+
},
64+
"value": {
65+
"id": "array",
66+
"namedSub": {
67+
"#source_location": {},
68+
"type": {
69+
"id": "array",
70+
"namedSub": {
71+
"#source_location": {},
72+
"size": {
73+
"id": "constant",
74+
"namedSub": {
75+
"type": {
76+
"id": "signedbv",
77+
"namedSub": {
78+
"#c_type": {
79+
"id": "signed_long_int"
80+
},
81+
"width": {
82+
"id": "64"
83+
}
84+
}
85+
},
86+
"value": {
87+
"id": "3"
88+
}
89+
}
90+
}
91+
},
92+
"sub": [
93+
{
94+
"id": "signedbv",
95+
"namedSub": {
96+
"#c_type": {
97+
"id": "signed_int"
98+
},
99+
"width": {
100+
"id": "32"
101+
}
102+
}
103+
}
104+
]
105+
}
106+
},
107+
"sub": [
108+
{
109+
"id": "constant",
110+
"namedSub": {
111+
"#base": {
112+
"id": "10"
113+
},
114+
"#source_location": {},
115+
"type": {
116+
"id": "signedbv",
117+
"namedSub": {
118+
"#c_type": {
119+
"id": "signed_int"
120+
},
121+
"width": {
122+
"id": "32"
123+
}
124+
}
125+
},
126+
"value": {
127+
"id": "4"
128+
}
129+
}
130+
},
131+
{
132+
"id": "constant",
133+
"namedSub": {
134+
"#base": {
135+
"id": "10"
136+
},
137+
"#source_location": {},
138+
"type": {
139+
"id": "signedbv",
140+
"namedSub": {
141+
"#c_type": {
142+
"id": "signed_int"
143+
},
144+
"width": {
145+
"id": "32"
146+
}
147+
}
148+
},
149+
"value": {
150+
"id": "5"
151+
}
152+
}
153+
},
154+
{
155+
"id": "constant",
156+
"namedSub": {
157+
"#base": {
158+
"id": "10"
159+
},
160+
"#source_location": {},
161+
"type": {
162+
"id": "signedbv",
163+
"namedSub": {
164+
"#c_type": {
165+
"id": "signed_int"
166+
},
167+
"width": {
168+
"id": "32"
169+
}
170+
}
171+
},
172+
"value": {
173+
"id": "6"
174+
}
175+
}
176+
}
177+
]
178+
}
179+
}
180+
}
181+
}

‎regression/goto-harness/load-snapshot-static-global-array-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 snapshot.json --initial-location main:0
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
VERIFICATION SUCCESSFUL
7+
--
8+
^warning: ignoring

‎regression/goto-harness/load-snapshot-static-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;
2+
3+
int main()
4+
{
5+
assert(x == 1);
6+
7+
return 0;
8+
}

‎regression/goto-harness/load-snapshot-static-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
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
VERIFICATION SUCCESSFUL
7+
--
8+
^warning: ignoring

‎regression/goto-harness/load-snapshot-static-global-int-02/main.c

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
int x;
2+
int y; // snapshot contains no value for y
3+
4+
int main()
5+
{
6+
assert(x == 1);
7+
assert(y == 1);
8+
9+
return 0;
10+
}

‎regression/goto-harness/load-snapshot-static-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-1-snapshot.json --initial-location main:0
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS
7+
\[main.assertion.2\] line [0-9]+ assertion y == 1: FAILURE
8+
--
9+
^warning: ignoring

‎regression/goto-harness/load-snapshot-static-global-int-03/main.c

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

‎regression/goto-harness/load-snapshot-static-global-int-03/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
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
VERIFICATION SUCCESSFUL
7+
--
8+
^warning: ignoring

‎regression/goto-harness/load-snapshot-static-global-int-04/main.c

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

‎regression/goto-harness/load-snapshot-static-global-int-04/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:1
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
VERIFICATION SUCCESSFUL
7+
--
8+
^warning: ignoring

‎regression/goto-harness/load-snapshot-static-global-pointer-01/main.c

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
int x;
2+
int *p; // has value &x in the snapshot
3+
4+
int main()
5+
{
6+
x = 1;
7+
8+
assert(*p == 1);
9+
10+
return 0;
11+
}

0 commit comments

Comments
 (0)