Skip to content

Commit dbf1f7d

Browse files
sim642sim642
committed
Add witness cram tests for 13-privatized/19-publish-precision and 20-publish-regression
1 parent e00bfb0 commit dbf1f7d

File tree

2 files changed

+539
-0
lines changed

2 files changed

+539
-0
lines changed

‎tests/regression/13-privatized/19-publish-precision.t‎

Lines changed: 245 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,3 +19,248 @@
1919
vulnerable: 0
2020
unsafe: 0
2121
total memory locations: 1
22+
23+
24+
Protection succeeds on check in t_fun.
25+
26+
$ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set witness.yaml.entry-types '["invariant_set"]' --disable witness.invariant.other 19-publish-precision.c
27+
[Success][Assert] Assertion "glob1 == 0" will succeed (19-publish-precision.c:27:3-27:30)
28+
[Success][Assert] Assertion "glob1 == 5" will succeed (19-publish-precision.c:17:3-17:30)
29+
[Warning][Assert] Assertion "glob1 == 0" is unknown. (19-publish-precision.c:30:3-30:30)
30+
[Warning][Assert] Assertion "glob1 == 5" is unknown. (19-publish-precision.c:31:3-31:30)
31+
[Info][Deadcode] Logical lines of code (LLoC) summary:
32+
live: 20
33+
dead: 0
34+
total lines: 20
35+
[Info][Witness] witness generation summary:
36+
location invariants: 10
37+
loop invariants: 0
38+
flow-insensitive invariants: 0
39+
total generation entries: 1
40+
[Info][Race] Memory locations race summary:
41+
safe: 1
42+
vulnerable: 0
43+
unsafe: 0
44+
total memory locations: 1
45+
46+
$ yamlWitnessStrip < witness.yml
47+
- entry_type: invariant_set
48+
content:
49+
- invariant:
50+
type: location_invariant
51+
location:
52+
file_name: 19-publish-precision.c
53+
line: 11
54+
column: 3
55+
function: t_fun
56+
value: (unsigned long )arg == 0UL
57+
format: c_expression
58+
- invariant:
59+
type: location_invariant
60+
location:
61+
file_name: 19-publish-precision.c
62+
line: 11
63+
column: 3
64+
function: t_fun
65+
value: 0 <= glob1
66+
format: c_expression
67+
- invariant:
68+
type: location_invariant
69+
location:
70+
file_name: 19-publish-precision.c
71+
line: 11
72+
column: 3
73+
function: t_fun
74+
value: glob1 <= 127
75+
format: c_expression
76+
- invariant:
77+
type: location_invariant
78+
location:
79+
file_name: 19-publish-precision.c
80+
line: 12
81+
column: 3
82+
function: t_fun
83+
value: (unsigned long )arg == 0UL
84+
format: c_expression
85+
- invariant:
86+
type: location_invariant
87+
location:
88+
file_name: 19-publish-precision.c
89+
line: 12
90+
column: 3
91+
function: t_fun
92+
value: 0 <= glob1
93+
format: c_expression
94+
- invariant:
95+
type: location_invariant
96+
location:
97+
file_name: 19-publish-precision.c
98+
line: 12
99+
column: 3
100+
function: t_fun
101+
value: glob1 <= 127
102+
format: c_expression
103+
- invariant:
104+
type: location_invariant
105+
location:
106+
file_name: 19-publish-precision.c
107+
line: 17
108+
column: 3
109+
function: t_fun
110+
value: (unsigned long )arg == 0UL
111+
format: c_expression
112+
- invariant:
113+
type: location_invariant
114+
location:
115+
file_name: 19-publish-precision.c
116+
line: 17
117+
column: 3
118+
function: t_fun
119+
value: glob1 == 5
120+
format: c_expression
121+
- invariant:
122+
type: location_invariant
123+
location:
124+
file_name: 19-publish-precision.c
125+
line: 30
126+
column: 3
127+
function: main
128+
value: 0 <= glob1
129+
format: c_expression
130+
- invariant:
131+
type: location_invariant
132+
location:
133+
file_name: 19-publish-precision.c
134+
line: 30
135+
column: 3
136+
function: main
137+
value: glob1 <= 127
138+
format: c_expression
139+
140+
141+
Vojdani does not succeed on check in t_fun.
142+
143+
$ goblint --set ana.base.privatization vojdani --enable witness.yaml.enabled --set witness.yaml.entry-types '["invariant_set"]' --disable witness.invariant.other 19-publish-precision.c
144+
[Success][Assert] Assertion "glob1 == 0" will succeed (19-publish-precision.c:27:3-27:30)
145+
[Warning][Assert] Assertion "glob1 == 5" is unknown. (19-publish-precision.c:17:3-17:30)
146+
[Warning][Assert] Assertion "glob1 == 0" is unknown. (19-publish-precision.c:30:3-30:30)
147+
[Warning][Assert] Assertion "glob1 == 5" is unknown. (19-publish-precision.c:31:3-31:30)
148+
[Info][Deadcode] Logical lines of code (LLoC) summary:
149+
live: 20
150+
dead: 0
151+
total lines: 20
152+
[Info][Witness] witness generation summary:
153+
location invariants: 11
154+
loop invariants: 0
155+
flow-insensitive invariants: 0
156+
total generation entries: 1
157+
[Info][Race] Memory locations race summary:
158+
safe: 1
159+
vulnerable: 0
160+
unsafe: 0
161+
total memory locations: 1
162+
163+
TODO: Vojdani should not have location_invariant-s on glob1 after locking mutex1 (line 11), only after mutex2.
164+
165+
$ yamlWitnessStrip < witness.yml
166+
- entry_type: invariant_set
167+
content:
168+
- invariant:
169+
type: location_invariant
170+
location:
171+
file_name: 19-publish-precision.c
172+
line: 11
173+
column: 3
174+
function: t_fun
175+
value: (unsigned long )arg == 0UL
176+
format: c_expression
177+
- invariant:
178+
type: location_invariant
179+
location:
180+
file_name: 19-publish-precision.c
181+
line: 11
182+
column: 3
183+
function: t_fun
184+
value: 0 <= glob1
185+
format: c_expression
186+
- invariant:
187+
type: location_invariant
188+
location:
189+
file_name: 19-publish-precision.c
190+
line: 11
191+
column: 3
192+
function: t_fun
193+
value: glob1 <= 127
194+
format: c_expression
195+
- invariant:
196+
type: location_invariant
197+
location:
198+
file_name: 19-publish-precision.c
199+
line: 12
200+
column: 3
201+
function: t_fun
202+
value: (unsigned long )arg == 0UL
203+
format: c_expression
204+
- invariant:
205+
type: location_invariant
206+
location:
207+
file_name: 19-publish-precision.c
208+
line: 12
209+
column: 3
210+
function: t_fun
211+
value: 0 <= glob1
212+
format: c_expression
213+
- invariant:
214+
type: location_invariant
215+
location:
216+
file_name: 19-publish-precision.c
217+
line: 12
218+
column: 3
219+
function: t_fun
220+
value: glob1 <= 127
221+
format: c_expression
222+
- invariant:
223+
type: location_invariant
224+
location:
225+
file_name: 19-publish-precision.c
226+
line: 17
227+
column: 3
228+
function: t_fun
229+
value: (unsigned long )arg == 0UL
230+
format: c_expression
231+
- invariant:
232+
type: location_invariant
233+
location:
234+
file_name: 19-publish-precision.c
235+
line: 17
236+
column: 3
237+
function: t_fun
238+
value: 0 <= glob1
239+
format: c_expression
240+
- invariant:
241+
type: location_invariant
242+
location:
243+
file_name: 19-publish-precision.c
244+
line: 17
245+
column: 3
246+
function: t_fun
247+
value: glob1 <= 127
248+
format: c_expression
249+
- invariant:
250+
type: location_invariant
251+
location:
252+
file_name: 19-publish-precision.c
253+
line: 30
254+
column: 3
255+
function: main
256+
value: 0 <= glob1
257+
format: c_expression
258+
- invariant:
259+
type: location_invariant
260+
location:
261+
file_name: 19-publish-precision.c
262+
line: 30
263+
column: 3
264+
function: main
265+
value: glob1 <= 127
266+
format: c_expression

0 commit comments

Comments
 (0)