Skip to content

Commit b65fee1

Browse files
TGWDBTGWDB
authored
Merge pull request #6257 from TGWDB/dump-c-var-overlap
Dump c var overlap
2 parents b249ac4 + 8a224be commit b65fee1

File tree

7 files changed

+731
-3
lines changed

7 files changed

+731
-3
lines changed

‎regression/contracts/assigns_enforce_scoping_01/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ main.c
33
--enforce-all-contracts
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[f1.\d+\] line \d+ Check that b is assignable: SUCCESS$
7-
^\[f1.\d+\] line \d+ Check that \*b is assignable: SUCCESS$
6+
^\[f1.\d+\] line \d+ Check that f1\$\$1\$\$1\$\$b is assignable: SUCCESS$
7+
^\[f1.\d+\] line \d+ Check that \*f1\$\$1\$\$1\$\$b is assignable: SUCCESS$
88
^\[f1.\d+\] line \d+ Check that \*b is assignable: FAILURE$
99
^VERIFICATION FAILED$
1010
--

‎regression/contracts/assigns_enforce_scoping_02/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--enforce-all-contracts
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[f1.\d+\] line \d+ Check that \*b is assignable: SUCCESS$
6+
^\[f1.\d+\] line \d+ Check that \*f1\$\$1\$\$1\$\$b is assignable: SUCCESS$
77
^\[f1.\d+\] line \d+ Check that \*b is assignable: FAILURE$
88
^VERIFICATION FAILED$
99
--

‎regression/goto-instrument-json/var_overlap1/test.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
test.json
3+
--dump-c
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
int helper\$\$1\$\$var_2\$\$x;
7+
int helper\$\$1\$\$var_3\$\$x;
8+
--
9+
int x;
10+
--
11+
This tests that variable conflicts are correctly converted to ugly but
12+
no-collision names. The json file declares "x" in the arguments and also
13+
twice in the "helper" function, both instances inside "helper" should
14+
have non-collision names in the dump-c output.

‎regression/goto-instrument-json/var_overlap1/test.json

Lines changed: 335 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,335 @@
1+
{
2+
"symbolTable": {
3+
"helper": {
4+
"baseName": "helper",
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": false,
17+
"isThreadLocal": false,
18+
"isType": false,
19+
"isVolatile": false,
20+
"isWeak": false,
21+
"mode": "C",
22+
"module": "",
23+
"name": "helper",
24+
"prettyName": "helper",
25+
"type": {
26+
"id": "code",
27+
"namedSub": {
28+
"parameters": {
29+
"id": "",
30+
"sub": [
31+
{
32+
"id": "parameter",
33+
"namedSub": {
34+
"#base_name": {
35+
"id": "helper::1::var_1::x"
36+
},
37+
"#identifier": {
38+
"id": "helper::1::var_1::x"
39+
},
40+
"type": {
41+
"id": "unsignedbv",
42+
"namedSub": {
43+
"width": {
44+
"id": "32"
45+
}
46+
}
47+
}
48+
}
49+
}
50+
]
51+
},
52+
"return_type": {
53+
"id": "empty"
54+
}
55+
}
56+
},
57+
"value": {
58+
"id": "code",
59+
"namedSub": {
60+
"statement": {
61+
"id": "block"
62+
}
63+
},
64+
"sub": [
65+
{
66+
"id": "code",
67+
"namedSub": {
68+
"statement": {
69+
"id": "decl"
70+
}
71+
},
72+
"sub": [
73+
{
74+
"id": "symbol",
75+
"namedSub": {
76+
"identifier": {
77+
"id": "helper::1::var_2::x"
78+
},
79+
"type": {
80+
"id": "signedbv",
81+
"namedSub": {
82+
"width": {
83+
"id": "32"
84+
}
85+
}
86+
}
87+
}
88+
}
89+
]
90+
},
91+
{
92+
"id": "code",
93+
"namedSub": {
94+
"statement": {
95+
"id": "decl"
96+
}
97+
},
98+
"sub": [
99+
{
100+
"id": "symbol",
101+
"namedSub": {
102+
"identifier": {
103+
"id": "helper::1::var_3::x"
104+
},
105+
"type": {
106+
"id": "signedbv",
107+
"namedSub": {
108+
"width": {
109+
"id": "32"
110+
}
111+
}
112+
}
113+
}
114+
}
115+
]
116+
}
117+
]
118+
}
119+
},
120+
"helper::1::var_1::x": {
121+
"baseName": "x",
122+
"isAuxiliary": false,
123+
"isExported": false,
124+
"isExtern": false,
125+
"isFileLocal": false,
126+
"isInput": false,
127+
"isLvalue": true,
128+
"isMacro": false,
129+
"isOutput": false,
130+
"isParameter": false,
131+
"isProperty": false,
132+
"isStateVar": true,
133+
"isStaticLifetime": false,
134+
"isThreadLocal": true,
135+
"isType": false,
136+
"isVolatile": false,
137+
"isWeak": false,
138+
"mode": "C",
139+
"module": "",
140+
"name": "helper::1::var_1::x",
141+
"prettyName": "",
142+
"type": {
143+
"id": "unsignedbv",
144+
"namedSub": {
145+
"width": {
146+
"id": "32"
147+
}
148+
}
149+
},
150+
"value": {
151+
"id": "nil"
152+
}
153+
},
154+
"helper::1::var_2::x": {
155+
"baseName": "x",
156+
"isAuxiliary": false,
157+
"isExported": false,
158+
"isExtern": false,
159+
"isFileLocal": false,
160+
"isInput": false,
161+
"isLvalue": true,
162+
"isMacro": false,
163+
"isOutput": false,
164+
"isParameter": false,
165+
"isProperty": false,
166+
"isStateVar": true,
167+
"isStaticLifetime": false,
168+
"isThreadLocal": true,
169+
"isType": false,
170+
"isVolatile": false,
171+
"isWeak": false,
172+
"mode": "C",
173+
"module": "",
174+
"name": "helper::1::var_2::x",
175+
"prettyName": "",
176+
"type": {
177+
"id": "signedbv",
178+
"namedSub": {
179+
"width": {
180+
"id": "32"
181+
}
182+
}
183+
},
184+
"value": {
185+
"id": "nil"
186+
}
187+
},
188+
"helper::1::var_3::x": {
189+
"baseName": "x",
190+
"isAuxiliary": false,
191+
"isExported": false,
192+
"isExtern": false,
193+
"isFileLocal": false,
194+
"isInput": false,
195+
"isLvalue": true,
196+
"isMacro": false,
197+
"isOutput": false,
198+
"isParameter": false,
199+
"isProperty": false,
200+
"isStateVar": true,
201+
"isStaticLifetime": false,
202+
"isThreadLocal": true,
203+
"isType": false,
204+
"isVolatile": false,
205+
"isWeak": false,
206+
"mode": "C",
207+
"module": "",
208+
"name": "helper::1::var_3::x",
209+
"prettyName": "",
210+
"type": {
211+
"id": "signedbv",
212+
"namedSub": {
213+
"width": {
214+
"id": "32"
215+
}
216+
}
217+
},
218+
"value": {
219+
"id": "nil"
220+
}
221+
},
222+
"main": {
223+
"baseName": "main",
224+
"isAuxiliary": false,
225+
"isExported": false,
226+
"isExtern": false,
227+
"isFileLocal": false,
228+
"isInput": false,
229+
"isLvalue": true,
230+
"isMacro": false,
231+
"isOutput": false,
232+
"isParameter": false,
233+
"isProperty": false,
234+
"isStateVar": false,
235+
"isStaticLifetime": false,
236+
"isThreadLocal": false,
237+
"isType": false,
238+
"isVolatile": false,
239+
"isWeak": false,
240+
"mode": "C",
241+
"module": "",
242+
"name": "main",
243+
"prettyName": "main",
244+
"type": {
245+
"id": "code",
246+
"namedSub": {
247+
"parameters": {
248+
"id": ""
249+
},
250+
"return_type": {
251+
"id": "empty"
252+
}
253+
}
254+
},
255+
"value": {
256+
"id": "code",
257+
"namedSub": {
258+
"statement": {
259+
"id": "expression"
260+
}
261+
},
262+
"sub": [
263+
{
264+
"id": "side_effect",
265+
"namedSub": {
266+
"statement": {
267+
"id": "function_call"
268+
},
269+
"type": {
270+
"id": "empty"
271+
}
272+
},
273+
"sub": [
274+
{
275+
"id": "symbol",
276+
"namedSub": {
277+
"identifier": {
278+
"id": "helper"
279+
},
280+
"type": {
281+
"id": "code",
282+
"namedSub": {
283+
"parameters": {
284+
"id": "",
285+
"sub": [
286+
{
287+
"id": "parameter",
288+
"namedSub": {
289+
"type": {
290+
"id": "unsignedbv",
291+
"namedSub": {
292+
"width": {
293+
"id": "32"
294+
}
295+
}
296+
}
297+
}
298+
}
299+
]
300+
},
301+
"return_type": {
302+
"id": "empty"
303+
}
304+
}
305+
}
306+
}
307+
},
308+
{
309+
"id": "arguments",
310+
"sub": [
311+
{
312+
"id": "constant",
313+
"namedSub": {
314+
"type": {
315+
"id": "unsignedbv",
316+
"namedSub": {
317+
"width": {
318+
"id": "32"
319+
}
320+
}
321+
},
322+
"value": {
323+
"id": "5"
324+
}
325+
}
326+
}
327+
]
328+
}
329+
]
330+
}
331+
]
332+
}
333+
}
334+
}
335+
}

‎regression/goto-instrument-json/var_overlap2/test.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
test.json
3+
--dump-c
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
void x\(unsigned int x\$\$1\$\$var_1\$\$x\);
7+
void x\(unsigned int x\$\$1\$\$var_1\$\$x\)
8+
int x\$\$1\$\$var_2\$\$x;
9+
int x\$\$1\$\$var_3\$\$x;
10+
--
11+
int x;
12+
--
13+
This tests that variable conflicts are correctly converted to ugly but
14+
no-collision names. The json file declares "x" as a function name, in the
15+
arguments and also twice in the "x" function. All instances except the
16+
function name "x" should have non-collision names in the dump-c output.

0 commit comments

Comments
 (0)