Skip to content

Commit 6023cbd

Browse files
sim642sim642
committed
Add ana.apron.invariant.diff-box test
1 parent 950cf9b commit 6023cbd

File tree

1 file changed

+280
-0
lines changed

1 file changed

+280
-0
lines changed

‎tests/regression/36-apron/52-queuesize.t‎

Lines changed: 280 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,280 @@
1+
`ana.apron.invariant.diff-box` test case from https://github.com/goblint/analyzer/pull/762.
2+
3+
Without diff-box:
4+
5+
$ goblint --enable witness.yaml.enabled --disable witness.invariant.other --disable ana.base.invariant.enabled --set ana.apron.privatization mutex-meet --set ana.activated[+] apron --enable ana.sv-comp.functions --set ana.apron.domain polyhedra --enable ana.apron.invariant.one-var --disable ana.apron.invariant.diff-box 52-queuesize.c
6+
[Success][Assert] Assertion "free >= 0" will succeed (52-queuesize.c:67:5-67:31)
7+
[Success][Assert] Assertion "free <= capacity" will succeed (52-queuesize.c:68:5-68:38)
8+
[Success][Assert] Assertion "used >= 0" will succeed (52-queuesize.c:69:5-69:31)
9+
[Success][Assert] Assertion "used <= capacity" will succeed (52-queuesize.c:70:5-70:38)
10+
[Success][Assert] Assertion "used + free == capacity" will succeed (52-queuesize.c:71:5-71:45)
11+
[Success][Assert] Assertion "free >= 0" will succeed (52-queuesize.c:15:3-15:29)
12+
[Success][Assert] Assertion "free <= capacity" will succeed (52-queuesize.c:16:3-16:36)
13+
[Success][Assert] Assertion "used >= 0" will succeed (52-queuesize.c:17:3-17:29)
14+
[Success][Assert] Assertion "used <= capacity" will succeed (52-queuesize.c:18:3-18:36)
15+
[Success][Assert] Assertion "used + free == capacity" will succeed (52-queuesize.c:19:3-19:43)
16+
[Success][Assert] Assertion "free >= 0" will succeed (52-queuesize.c:26:3-26:29)
17+
[Success][Assert] Assertion "free <= capacity" will succeed (52-queuesize.c:27:3-27:36)
18+
[Success][Assert] Assertion "used >= 0" will succeed (52-queuesize.c:28:3-28:29)
19+
[Success][Assert] Assertion "used <= capacity" will succeed (52-queuesize.c:29:3-29:36)
20+
[Success][Assert] Assertion "used + free == capacity" will succeed (52-queuesize.c:30:3-30:43)
21+
[Success][Assert] Assertion "free >= 0" will succeed (52-queuesize.c:36:3-36:29)
22+
[Success][Assert] Assertion "free <= capacity" will succeed (52-queuesize.c:37:3-37:36)
23+
[Success][Assert] Assertion "used >= 0" will succeed (52-queuesize.c:38:3-38:29)
24+
[Success][Assert] Assertion "used <= capacity" will succeed (52-queuesize.c:39:3-39:36)
25+
[Success][Assert] Assertion "used + free == capacity" will succeed (52-queuesize.c:40:3-40:43)
26+
[Success][Assert] Assertion "free >= 0" will succeed (52-queuesize.c:47:3-47:29)
27+
[Success][Assert] Assertion "free <= capacity" will succeed (52-queuesize.c:48:3-48:36)
28+
[Success][Assert] Assertion "used >= 0" will succeed (52-queuesize.c:49:3-49:29)
29+
[Success][Assert] Assertion "used <= capacity" will succeed (52-queuesize.c:50:3-50:36)
30+
[Success][Assert] Assertion "used + free == capacity" will succeed (52-queuesize.c:51:3-51:43)
31+
[Warning][Deadcode] Function 'worker' has dead code:
32+
on line 58 (52-queuesize.c:58-58)
33+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
34+
live: 53
35+
dead: 1
36+
total: 54
37+
[Warning][Deadcode][CWE-571] condition '1' is always true (52-queuesize.c:56:10-56:11)
38+
[Warning][Deadcode][CWE-571] condition '1' is always true (52-queuesize.c:78:12-78:13)
39+
[Info][Witness] witness generation summary:
40+
total: 8
41+
[Info][Race] Memory locations race summary:
42+
safe: 3
43+
vulnerable: 0
44+
unsafe: 0
45+
total: 3
46+
47+
$ yamlWitnessStrip < witness.yml | tee witness-disable-diff-box.yml
48+
- entry_type: loop_invariant
49+
location:
50+
file_name: 52-queuesize.c
51+
file_hash: $STRIPPED_FILE_HASH
52+
line: 36
53+
column: 2
54+
function: push
55+
loop_invariant:
56+
string: 2147483647LL - (long long )capacity >= 0LL
57+
type: assertion
58+
format: C
59+
- entry_type: loop_invariant
60+
location:
61+
file_name: 52-queuesize.c
62+
file_hash: $STRIPPED_FILE_HASH
63+
line: 36
64+
column: 2
65+
function: push
66+
loop_invariant:
67+
string: (long long )free >= 0LL
68+
type: assertion
69+
format: C
70+
- entry_type: loop_invariant
71+
location:
72+
file_name: 52-queuesize.c
73+
file_hash: $STRIPPED_FILE_HASH
74+
line: 36
75+
column: 2
76+
function: push
77+
loop_invariant:
78+
string: (long long )capacity - (long long )free >= 0LL
79+
type: assertion
80+
format: C
81+
- entry_type: loop_invariant
82+
location:
83+
file_name: 52-queuesize.c
84+
file_hash: $STRIPPED_FILE_HASH
85+
line: 36
86+
column: 2
87+
function: push
88+
loop_invariant:
89+
string: ((0LL - (long long )capacity) + (long long )free) + (long long )used ==
90+
0LL
91+
type: assertion
92+
format: C
93+
- entry_type: loop_invariant
94+
location:
95+
file_name: 52-queuesize.c
96+
file_hash: $STRIPPED_FILE_HASH
97+
line: 15
98+
column: 2
99+
function: pop
100+
loop_invariant:
101+
string: 2147483647LL - (long long )capacity >= 0LL
102+
type: assertion
103+
format: C
104+
- entry_type: loop_invariant
105+
location:
106+
file_name: 52-queuesize.c
107+
file_hash: $STRIPPED_FILE_HASH
108+
line: 15
109+
column: 2
110+
function: pop
111+
loop_invariant:
112+
string: (long long )free >= 0LL
113+
type: assertion
114+
format: C
115+
- entry_type: loop_invariant
116+
location:
117+
file_name: 52-queuesize.c
118+
file_hash: $STRIPPED_FILE_HASH
119+
line: 15
120+
column: 2
121+
function: pop
122+
loop_invariant:
123+
string: (long long )capacity - (long long )free >= 0LL
124+
type: assertion
125+
format: C
126+
- entry_type: loop_invariant
127+
location:
128+
file_name: 52-queuesize.c
129+
file_hash: $STRIPPED_FILE_HASH
130+
line: 15
131+
column: 2
132+
function: pop
133+
loop_invariant:
134+
string: ((0LL - (long long )capacity) + (long long )free) + (long long )used ==
135+
0LL
136+
type: assertion
137+
format: C
138+
139+
With diff-box:
140+
141+
$ goblint --enable witness.yaml.enabled --disable witness.invariant.other --disable ana.base.invariant.enabled --set ana.apron.privatization mutex-meet --set ana.activated[+] apron --enable ana.sv-comp.functions --set ana.apron.domain polyhedra --enable ana.apron.invariant.one-var --enable ana.apron.invariant.diff-box 52-queuesize.c
142+
[Success][Assert] Assertion "free >= 0" will succeed (52-queuesize.c:67:5-67:31)
143+
[Success][Assert] Assertion "free <= capacity" will succeed (52-queuesize.c:68:5-68:38)
144+
[Success][Assert] Assertion "used >= 0" will succeed (52-queuesize.c:69:5-69:31)
145+
[Success][Assert] Assertion "used <= capacity" will succeed (52-queuesize.c:70:5-70:38)
146+
[Success][Assert] Assertion "used + free == capacity" will succeed (52-queuesize.c:71:5-71:45)
147+
[Success][Assert] Assertion "free >= 0" will succeed (52-queuesize.c:15:3-15:29)
148+
[Success][Assert] Assertion "free <= capacity" will succeed (52-queuesize.c:16:3-16:36)
149+
[Success][Assert] Assertion "used >= 0" will succeed (52-queuesize.c:17:3-17:29)
150+
[Success][Assert] Assertion "used <= capacity" will succeed (52-queuesize.c:18:3-18:36)
151+
[Success][Assert] Assertion "used + free == capacity" will succeed (52-queuesize.c:19:3-19:43)
152+
[Success][Assert] Assertion "free >= 0" will succeed (52-queuesize.c:26:3-26:29)
153+
[Success][Assert] Assertion "free <= capacity" will succeed (52-queuesize.c:27:3-27:36)
154+
[Success][Assert] Assertion "used >= 0" will succeed (52-queuesize.c:28:3-28:29)
155+
[Success][Assert] Assertion "used <= capacity" will succeed (52-queuesize.c:29:3-29:36)
156+
[Success][Assert] Assertion "used + free == capacity" will succeed (52-queuesize.c:30:3-30:43)
157+
[Success][Assert] Assertion "free >= 0" will succeed (52-queuesize.c:36:3-36:29)
158+
[Success][Assert] Assertion "free <= capacity" will succeed (52-queuesize.c:37:3-37:36)
159+
[Success][Assert] Assertion "used >= 0" will succeed (52-queuesize.c:38:3-38:29)
160+
[Success][Assert] Assertion "used <= capacity" will succeed (52-queuesize.c:39:3-39:36)
161+
[Success][Assert] Assertion "used + free == capacity" will succeed (52-queuesize.c:40:3-40:43)
162+
[Success][Assert] Assertion "free >= 0" will succeed (52-queuesize.c:47:3-47:29)
163+
[Success][Assert] Assertion "free <= capacity" will succeed (52-queuesize.c:48:3-48:36)
164+
[Success][Assert] Assertion "used >= 0" will succeed (52-queuesize.c:49:3-49:29)
165+
[Success][Assert] Assertion "used <= capacity" will succeed (52-queuesize.c:50:3-50:36)
166+
[Success][Assert] Assertion "used + free == capacity" will succeed (52-queuesize.c:51:3-51:43)
167+
[Warning][Deadcode] Function 'worker' has dead code:
168+
on line 58 (52-queuesize.c:58-58)
169+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
170+
live: 53
171+
dead: 1
172+
total: 54
173+
[Warning][Deadcode][CWE-571] condition '1' is always true (52-queuesize.c:56:10-56:11)
174+
[Warning][Deadcode][CWE-571] condition '1' is always true (52-queuesize.c:78:12-78:13)
175+
[Info][Witness] witness generation summary:
176+
total: 6
177+
[Info][Race] Memory locations race summary:
178+
safe: 3
179+
vulnerable: 0
180+
unsafe: 0
181+
total: 3
182+
183+
$ yamlWitnessStrip < witness.yml | tee witness-enable-diff-box.yml
184+
- entry_type: loop_invariant
185+
location:
186+
file_name: 52-queuesize.c
187+
file_hash: $STRIPPED_FILE_HASH
188+
line: 36
189+
column: 2
190+
function: push
191+
loop_invariant:
192+
string: (long long )free >= 0LL
193+
type: assertion
194+
format: C
195+
- entry_type: loop_invariant
196+
location:
197+
file_name: 52-queuesize.c
198+
file_hash: $STRIPPED_FILE_HASH
199+
line: 36
200+
column: 2
201+
function: push
202+
loop_invariant:
203+
string: (long long )capacity - (long long )free >= 0LL
204+
type: assertion
205+
format: C
206+
- entry_type: loop_invariant
207+
location:
208+
file_name: 52-queuesize.c
209+
file_hash: $STRIPPED_FILE_HASH
210+
line: 36
211+
column: 2
212+
function: push
213+
loop_invariant:
214+
string: ((0LL - (long long )capacity) + (long long )free) + (long long )used ==
215+
0LL
216+
type: assertion
217+
format: C
218+
- entry_type: loop_invariant
219+
location:
220+
file_name: 52-queuesize.c
221+
file_hash: $STRIPPED_FILE_HASH
222+
line: 15
223+
column: 2
224+
function: pop
225+
loop_invariant:
226+
string: (long long )free >= 0LL
227+
type: assertion
228+
format: C
229+
- entry_type: loop_invariant
230+
location:
231+
file_name: 52-queuesize.c
232+
file_hash: $STRIPPED_FILE_HASH
233+
line: 15
234+
column: 2
235+
function: pop
236+
loop_invariant:
237+
string: (long long )capacity - (long long )free >= 0LL
238+
type: assertion
239+
format: C
240+
- entry_type: loop_invariant
241+
location:
242+
file_name: 52-queuesize.c
243+
file_hash: $STRIPPED_FILE_HASH
244+
line: 15
245+
column: 2
246+
function: pop
247+
loop_invariant:
248+
string: ((0LL - (long long )capacity) + (long long )free) + (long long )used ==
249+
0LL
250+
type: assertion
251+
format: C
252+
253+
Compare witnesses:
254+
255+
$ diff witness-disable-diff-box.yml witness-enable-diff-box.yml
256+
9,19d8
257+
< string: 2147483647LL - (long long )capacity >= 0LL
258+
< type: assertion
259+
< format: C
260+
< - entry_type: loop_invariant
261+
< location:
262+
< file_name: 52-queuesize.c
263+
< file_hash: $STRIPPED_FILE_HASH
264+
< line: 36
265+
< column: 2
266+
< function: push
267+
< loop_invariant:
268+
44,54d32
269+
< type: assertion
270+
< format: C
271+
< - entry_type: loop_invariant
272+
< location:
273+
< file_name: 52-queuesize.c
274+
< file_hash: $STRIPPED_FILE_HASH
275+
< line: 15
276+
< column: 2
277+
< function: pop
278+
< loop_invariant:
279+
< string: 2147483647LL - (long long )capacity >= 0LL
280+
[1]

0 commit comments

Comments
 (0)