Skip to content

Commit e39b40c

Browse files
sim642sim642
committed
Add test 56-witness/72-shadowing-invariant (issue #1722)
1 parent 28f8f76 commit e39b40c

File tree

2 files changed

+174
-0
lines changed

2 files changed

+174
-0
lines changed

‎tests/regression/56-witness/72-shadowing-invariant.c‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
// CRAM PARAM: --set ana.activated[+] var_eq
2+
3+
int foo = 1;
4+
5+
int main() {
6+
int foo = 2; // shadows global
7+
8+
int bar = 3;
9+
{
10+
int bar = 4; // shadows outer block
11+
return 0;
12+
}
13+
}

‎tests/regression/56-witness/72-shadowing-invariant.t‎

Lines changed: 161 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,161 @@
1+
$ goblint --set ana.activated[+] var_eq --enable witness.yaml.enabled --enable witness.invariant.other 72-shadowing-invariant.c
2+
[Info][Deadcode] Logical lines of code (LLoC) summary:
3+
live: 5
4+
dead: 0
5+
total lines: 5
6+
[Info][Witness] witness generation summary:
7+
location invariants: 16
8+
loop invariants: 0
9+
flow-insensitive invariants: 0
10+
total generation entries: 1
11+
12+
Should not contain invariants containing shadowed variables.
13+
They can be wrong and contradicting.
14+
15+
$ yamlWitnessStrip < witness.yml
16+
- entry_type: invariant_set
17+
content:
18+
- invariant:
19+
type: location_invariant
20+
location:
21+
file_name: 72-shadowing-invariant.c
22+
line: 6
23+
column: 3
24+
function: main
25+
value: foo == 1
26+
format: c_expression
27+
- invariant:
28+
type: location_invariant
29+
location:
30+
file_name: 72-shadowing-invariant.c
31+
line: 8
32+
column: 3
33+
function: main
34+
value: 2 == foo
35+
format: c_expression
36+
- invariant:
37+
type: location_invariant
38+
location:
39+
file_name: 72-shadowing-invariant.c
40+
line: 8
41+
column: 3
42+
function: main
43+
value: foo == 1
44+
format: c_expression
45+
- invariant:
46+
type: location_invariant
47+
location:
48+
file_name: 72-shadowing-invariant.c
49+
line: 8
50+
column: 3
51+
function: main
52+
value: foo == 2
53+
format: c_expression
54+
- invariant:
55+
type: location_invariant
56+
location:
57+
file_name: 72-shadowing-invariant.c
58+
line: 10
59+
column: 5
60+
function: main
61+
value: 2 == foo
62+
format: c_expression
63+
- invariant:
64+
type: location_invariant
65+
location:
66+
file_name: 72-shadowing-invariant.c
67+
line: 10
68+
column: 5
69+
function: main
70+
value: 3 == bar
71+
format: c_expression
72+
- invariant:
73+
type: location_invariant
74+
location:
75+
file_name: 72-shadowing-invariant.c
76+
line: 10
77+
column: 5
78+
function: main
79+
value: bar == 3
80+
format: c_expression
81+
- invariant:
82+
type: location_invariant
83+
location:
84+
file_name: 72-shadowing-invariant.c
85+
line: 10
86+
column: 5
87+
function: main
88+
value: foo == 1
89+
format: c_expression
90+
- invariant:
91+
type: location_invariant
92+
location:
93+
file_name: 72-shadowing-invariant.c
94+
line: 10
95+
column: 5
96+
function: main
97+
value: foo == 2
98+
format: c_expression
99+
- invariant:
100+
type: location_invariant
101+
location:
102+
file_name: 72-shadowing-invariant.c
103+
line: 11
104+
column: 5
105+
function: main
106+
value: 2 == foo
107+
format: c_expression
108+
- invariant:
109+
type: location_invariant
110+
location:
111+
file_name: 72-shadowing-invariant.c
112+
line: 11
113+
column: 5
114+
function: main
115+
value: 3 == bar
116+
format: c_expression
117+
- invariant:
118+
type: location_invariant
119+
location:
120+
file_name: 72-shadowing-invariant.c
121+
line: 11
122+
column: 5
123+
function: main
124+
value: 4 == bar
125+
format: c_expression
126+
- invariant:
127+
type: location_invariant
128+
location:
129+
file_name: 72-shadowing-invariant.c
130+
line: 11
131+
column: 5
132+
function: main
133+
value: bar == 3
134+
format: c_expression
135+
- invariant:
136+
type: location_invariant
137+
location:
138+
file_name: 72-shadowing-invariant.c
139+
line: 11
140+
column: 5
141+
function: main
142+
value: bar == 4
143+
format: c_expression
144+
- invariant:
145+
type: location_invariant
146+
location:
147+
file_name: 72-shadowing-invariant.c
148+
line: 11
149+
column: 5
150+
function: main
151+
value: foo == 1
152+
format: c_expression
153+
- invariant:
154+
type: location_invariant
155+
location:
156+
file_name: 72-shadowing-invariant.c
157+
line: 11
158+
column: 5
159+
function: main
160+
value: foo == 2
161+
format: c_expression

0 commit comments

Comments
 (0)