Skip to content

Commit 3c156e8

Browse files
sim642sim642
committed
Add witness cram test 89-apron3/03-octagon_simplest
1 parent 155c2d6 commit 3c156e8

File tree

3 files changed

+332
-0
lines changed

3 files changed

+332
-0
lines changed

‎tests/regression/89-apron3/03-octagon_simplest.c‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
// SKIP CRAM PARAM: --set ana.activated[+] apron --enable ana.int.interval
2+
// Simplified from 36-apron/01-octagon_simple
3+
#include <goblint.h>
4+
5+
void main(void) {
6+
int X = 0;
7+
int Y = 0;
8+
int N = rand();
9+
if(N < 0) { N = 0; }
10+
11+
while(X < N) {
12+
X++;
13+
}
14+
}

‎tests/regression/89-apron3/03-octagon_simplest.t‎

Lines changed: 313 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,313 @@
1+
Without diff-box:
2+
3+
$ goblint --set ana.activated[+] apron --set ana.apron.domain octagon --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.invariant-types '["loop_invariant"]' --disable ana.base.invariant.enabled --enable ana.relation.invariant.one-var --disable ana.apron.invariant.diff-box 03-octagon_simplest.c
4+
[Info][Deadcode] Logical lines of code (LLoC) summary:
5+
live: 8
6+
dead: 0
7+
total lines: 8
8+
[Warning][Deadcode][CWE-570] condition 'N < 0' is always false (03-octagon_simplest.c:9:6-9:11)
9+
[Info][Witness] witness generation summary:
10+
location invariants: 0
11+
loop invariants: 15
12+
flow-insensitive invariants: 0
13+
total generation entries: 1
14+
15+
TODO: Should have Y == 0
16+
$ yamlWitnessStrip < witness.yml | tee witness-disable-diff-box.yml
17+
- entry_type: invariant_set
18+
content:
19+
- invariant:
20+
type: loop_invariant
21+
location:
22+
file_name: 03-octagon_simplest.c
23+
line: 11
24+
column: 3
25+
function: main
26+
value: (long long )N >= (long long )X
27+
format: c_expression
28+
- invariant:
29+
type: loop_invariant
30+
location:
31+
file_name: 03-octagon_simplest.c
32+
line: 11
33+
column: 3
34+
function: main
35+
value: (long long )N >= (long long )Y
36+
format: c_expression
37+
- invariant:
38+
type: loop_invariant
39+
location:
40+
file_name: 03-octagon_simplest.c
41+
line: 11
42+
column: 3
43+
function: main
44+
value: (long long )N >= 0LL
45+
format: c_expression
46+
- invariant:
47+
type: loop_invariant
48+
location:
49+
file_name: 03-octagon_simplest.c
50+
line: 11
51+
column: 3
52+
function: main
53+
value: (long long )X + (long long )N >= 0LL
54+
format: c_expression
55+
- invariant:
56+
type: loop_invariant
57+
location:
58+
file_name: 03-octagon_simplest.c
59+
line: 11
60+
column: 3
61+
function: main
62+
value: (long long )X + 2147483647LL >= (long long )N
63+
format: c_expression
64+
- invariant:
65+
type: loop_invariant
66+
location:
67+
file_name: 03-octagon_simplest.c
68+
line: 11
69+
column: 3
70+
function: main
71+
value: (long long )X >= (long long )Y
72+
format: c_expression
73+
- invariant:
74+
type: loop_invariant
75+
location:
76+
file_name: 03-octagon_simplest.c
77+
line: 11
78+
column: 3
79+
function: main
80+
value: (long long )Y + (long long )N >= 0LL
81+
format: c_expression
82+
- invariant:
83+
type: loop_invariant
84+
location:
85+
file_name: 03-octagon_simplest.c
86+
line: 11
87+
column: 3
88+
function: main
89+
value: (long long )Y + (long long )X >= 0LL
90+
format: c_expression
91+
- invariant:
92+
type: loop_invariant
93+
location:
94+
file_name: 03-octagon_simplest.c
95+
line: 11
96+
column: 3
97+
function: main
98+
value: (long long )Y + 2147483647LL >= (long long )N
99+
format: c_expression
100+
- invariant:
101+
type: loop_invariant
102+
location:
103+
file_name: 03-octagon_simplest.c
104+
line: 11
105+
column: 3
106+
function: main
107+
value: (long long )Y + 2147483647LL >= (long long )X
108+
format: c_expression
109+
- invariant:
110+
type: loop_invariant
111+
location:
112+
file_name: 03-octagon_simplest.c
113+
line: 11
114+
column: 3
115+
function: main
116+
value: 2147483647LL >= (long long )N
117+
format: c_expression
118+
- invariant:
119+
type: loop_invariant
120+
location:
121+
file_name: 03-octagon_simplest.c
122+
line: 11
123+
column: 3
124+
function: main
125+
value: 2147483647LL >= (long long )X
126+
format: c_expression
127+
- invariant:
128+
type: loop_invariant
129+
location:
130+
file_name: 03-octagon_simplest.c
131+
line: 11
132+
column: 3
133+
function: main
134+
value: 2147483647LL >= (long long )Y + (long long )N
135+
format: c_expression
136+
- invariant:
137+
type: loop_invariant
138+
location:
139+
file_name: 03-octagon_simplest.c
140+
line: 11
141+
column: 3
142+
function: main
143+
value: 2147483647LL >= (long long )Y + (long long )X
144+
format: c_expression
145+
- invariant:
146+
type: loop_invariant
147+
location:
148+
file_name: 03-octagon_simplest.c
149+
line: 11
150+
column: 3
151+
function: main
152+
value: 4294967294LL >= (long long )X + (long long )N
153+
format: c_expression
154+
155+
With diff-box:
156+
157+
$ goblint --set ana.activated[+] apron --set ana.apron.domain octagon --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.invariant-types '["loop_invariant"]' --disable ana.base.invariant.enabled --enable ana.relation.invariant.one-var --enable ana.apron.invariant.diff-box 03-octagon_simplest.c
158+
[Info][Deadcode] Logical lines of code (LLoC) summary:
159+
live: 8
160+
dead: 0
161+
total lines: 8
162+
[Warning][Deadcode][CWE-570] condition 'N < 0' is always false (03-octagon_simplest.c:9:6-9:11)
163+
[Info][Witness] witness generation summary:
164+
location invariants: 0
165+
loop invariants: 5
166+
flow-insensitive invariants: 0
167+
total generation entries: 1
168+
169+
TODO: diff-box isn't enough to get rid of invariants with Y (which is known to be 0)
170+
$ yamlWitnessStrip < witness.yml | tee witness-enable-diff-box.yml
171+
- entry_type: invariant_set
172+
content:
173+
- invariant:
174+
type: loop_invariant
175+
location:
176+
file_name: 03-octagon_simplest.c
177+
line: 11
178+
column: 3
179+
function: main
180+
value: (long long )N >= (long long )X
181+
format: c_expression
182+
- invariant:
183+
type: loop_invariant
184+
location:
185+
file_name: 03-octagon_simplest.c
186+
line: 11
187+
column: 3
188+
function: main
189+
value: (long long )Y + 2147483647LL >= (long long )X
190+
format: c_expression
191+
- invariant:
192+
type: loop_invariant
193+
location:
194+
file_name: 03-octagon_simplest.c
195+
line: 11
196+
column: 3
197+
function: main
198+
value: 2147483647LL >= (long long )X
199+
format: c_expression
200+
- invariant:
201+
type: loop_invariant
202+
location:
203+
file_name: 03-octagon_simplest.c
204+
line: 11
205+
column: 3
206+
function: main
207+
value: 2147483647LL >= (long long )Y + (long long )X
208+
format: c_expression
209+
- invariant:
210+
type: loop_invariant
211+
location:
212+
file_name: 03-octagon_simplest.c
213+
line: 11
214+
column: 3
215+
function: main
216+
value: 4294967294LL >= (long long )X + (long long )N
217+
format: c_expression
218+
219+
Compare witnesses:
220+
221+
$ yamlWitnessStripDiff witness-disable-diff-box.yml witness-enable-diff-box.yml
222+
# Left-only invariants:
223+
- invariant:
224+
type: loop_invariant
225+
location:
226+
file_name: 03-octagon_simplest.c
227+
line: 11
228+
column: 3
229+
function: main
230+
value: 2147483647LL >= (long long )Y + (long long )N
231+
format: c_expression
232+
- invariant:
233+
type: loop_invariant
234+
location:
235+
file_name: 03-octagon_simplest.c
236+
line: 11
237+
column: 3
238+
function: main
239+
value: 2147483647LL >= (long long )N
240+
format: c_expression
241+
- invariant:
242+
type: loop_invariant
243+
location:
244+
file_name: 03-octagon_simplest.c
245+
line: 11
246+
column: 3
247+
function: main
248+
value: (long long )Y + 2147483647LL >= (long long )N
249+
format: c_expression
250+
- invariant:
251+
type: loop_invariant
252+
location:
253+
file_name: 03-octagon_simplest.c
254+
line: 11
255+
column: 3
256+
function: main
257+
value: (long long )Y + (long long )X >= 0LL
258+
format: c_expression
259+
- invariant:
260+
type: loop_invariant
261+
location:
262+
file_name: 03-octagon_simplest.c
263+
line: 11
264+
column: 3
265+
function: main
266+
value: (long long )Y + (long long )N >= 0LL
267+
format: c_expression
268+
- invariant:
269+
type: loop_invariant
270+
location:
271+
file_name: 03-octagon_simplest.c
272+
line: 11
273+
column: 3
274+
function: main
275+
value: (long long )X >= (long long )Y
276+
format: c_expression
277+
- invariant:
278+
type: loop_invariant
279+
location:
280+
file_name: 03-octagon_simplest.c
281+
line: 11
282+
column: 3
283+
function: main
284+
value: (long long )X + 2147483647LL >= (long long )N
285+
format: c_expression
286+
- invariant:
287+
type: loop_invariant
288+
location:
289+
file_name: 03-octagon_simplest.c
290+
line: 11
291+
column: 3
292+
function: main
293+
value: (long long )X + (long long )N >= 0LL
294+
format: c_expression
295+
- invariant:
296+
type: loop_invariant
297+
location:
298+
file_name: 03-octagon_simplest.c
299+
line: 11
300+
column: 3
301+
function: main
302+
value: (long long )N >= 0LL
303+
format: c_expression
304+
- invariant:
305+
type: loop_invariant
306+
location:
307+
file_name: 03-octagon_simplest.c
308+
line: 11
309+
column: 3
310+
function: main
311+
value: (long long )N >= (long long )Y
312+
format: c_expression
313+
---

‎tests/regression/89-apron3/dune‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,8 @@
88
(glob_files ??-*.c))
99
(locks /update_suite)
1010
(action (chdir ../../.. (run %{update_suite} group apron3 -q))))
11+
12+
(cram
13+
(alias runaprontest)
14+
(enabled_if %{lib-available:apron})
15+
(deps (glob_files *.c)))

0 commit comments

Comments
 (0)