Skip to content

Commit 924372d

Browse files
sim642sim642
authored
Merge pull request #1852 from goblint/yaml-witness-convert-2
Convert most old YAML witnesses to version 2.0
2 parents 9e5e869 + e31c82d commit 924372d

File tree

15 files changed

+1911
-2261
lines changed

15 files changed

+1911
-2261
lines changed

‎tests/regression/13-privatized/01-priv_nr.t‎

Lines changed: 124 additions & 128 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
`protection` privatization:
22

3-
$ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization protection 01-priv_nr.c
3+
$ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization protection 01-priv_nr.c
44
[Success][Assert] Assertion "glob1 == 5" will succeed (01-priv_nr.c:22:3-22:30)
55
[Success][Assert] Assertion "t == 5" will succeed (01-priv_nr.c:12:3-12:26)
66
[Success][Assert] Assertion "glob1 == -10" will succeed (01-priv_nr.c:14:3-14:32)
@@ -13,48 +13,47 @@
1313
location invariants: 3
1414
loop invariants: 0
1515
flow-insensitive invariants: 0
16-
total generation entries: 3
16+
total generation entries: 1
1717
[Info][Race] Memory locations race summary:
1818
safe: 1
1919
vulnerable: 0
2020
unsafe: 0
2121
total memory locations: 1
2222

2323
$ yamlWitnessStrip < witness.yml
24-
- entry_type: location_invariant
25-
location:
26-
file_name: 01-priv_nr.c
27-
line: 25
28-
column: 3
29-
function: main
30-
location_invariant:
31-
string: glob1 == 5
32-
type: assertion
33-
format: C
34-
- entry_type: location_invariant
35-
location:
36-
file_name: 01-priv_nr.c
37-
line: 11
38-
column: 3
39-
function: t_fun
40-
location_invariant:
41-
string: glob1 == 5
42-
type: assertion
43-
format: C
44-
- entry_type: location_invariant
45-
location:
46-
file_name: 01-priv_nr.c
47-
line: 11
48-
column: 3
49-
function: t_fun
50-
location_invariant:
51-
string: (unsigned long )arg == 0UL
52-
type: assertion
53-
format: C
24+
- entry_type: invariant_set
25+
content:
26+
- invariant:
27+
type: location_invariant
28+
location:
29+
file_name: 01-priv_nr.c
30+
line: 11
31+
column: 3
32+
function: t_fun
33+
value: (unsigned long )arg == 0UL
34+
format: c_expression
35+
- invariant:
36+
type: location_invariant
37+
location:
38+
file_name: 01-priv_nr.c
39+
line: 11
40+
column: 3
41+
function: t_fun
42+
value: glob1 == 5
43+
format: c_expression
44+
- invariant:
45+
type: location_invariant
46+
location:
47+
file_name: 01-priv_nr.c
48+
line: 25
49+
column: 3
50+
function: main
51+
value: glob1 == 5
52+
format: c_expression
5453

5554
`vojdani` privatization:
5655

57-
$ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization vojdani 01-priv_nr.c
56+
$ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization vojdani 01-priv_nr.c
5857
[Success][Assert] Assertion "glob1 == 5" will succeed (01-priv_nr.c:22:3-22:30)
5958
[Success][Assert] Assertion "t == 5" will succeed (01-priv_nr.c:12:3-12:26)
6059
[Success][Assert] Assertion "glob1 == -10" will succeed (01-priv_nr.c:14:3-14:32)
@@ -67,48 +66,47 @@
6766
location invariants: 3
6867
loop invariants: 0
6968
flow-insensitive invariants: 0
70-
total generation entries: 3
69+
total generation entries: 1
7170
[Info][Race] Memory locations race summary:
7271
safe: 1
7372
vulnerable: 0
7473
unsafe: 0
7574
total memory locations: 1
7675

7776
$ yamlWitnessStrip < witness.yml
78-
- entry_type: location_invariant
79-
location:
80-
file_name: 01-priv_nr.c
81-
line: 25
82-
column: 3
83-
function: main
84-
location_invariant:
85-
string: glob1 == 5
86-
type: assertion
87-
format: C
88-
- entry_type: location_invariant
89-
location:
90-
file_name: 01-priv_nr.c
91-
line: 11
92-
column: 3
93-
function: t_fun
94-
location_invariant:
95-
string: glob1 == 5
96-
type: assertion
97-
format: C
98-
- entry_type: location_invariant
99-
location:
100-
file_name: 01-priv_nr.c
101-
line: 11
102-
column: 3
103-
function: t_fun
104-
location_invariant:
105-
string: (unsigned long )arg == 0UL
106-
type: assertion
107-
format: C
77+
- entry_type: invariant_set
78+
content:
79+
- invariant:
80+
type: location_invariant
81+
location:
82+
file_name: 01-priv_nr.c
83+
line: 11
84+
column: 3
85+
function: t_fun
86+
value: (unsigned long )arg == 0UL
87+
format: c_expression
88+
- invariant:
89+
type: location_invariant
90+
location:
91+
file_name: 01-priv_nr.c
92+
line: 11
93+
column: 3
94+
function: t_fun
95+
value: glob1 == 5
96+
format: c_expression
97+
- invariant:
98+
type: location_invariant
99+
location:
100+
file_name: 01-priv_nr.c
101+
line: 25
102+
column: 3
103+
function: main
104+
value: glob1 == 5
105+
format: c_expression
108106

109107
`mutex-meet` privatization:
110108

111-
$ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization mutex-meet 01-priv_nr.c
109+
$ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization mutex-meet 01-priv_nr.c
112110
[Success][Assert] Assertion "glob1 == 5" will succeed (01-priv_nr.c:22:3-22:30)
113111
[Success][Assert] Assertion "t == 5" will succeed (01-priv_nr.c:12:3-12:26)
114112
[Success][Assert] Assertion "glob1 == -10" will succeed (01-priv_nr.c:14:3-14:32)
@@ -121,48 +119,47 @@
121119
location invariants: 3
122120
loop invariants: 0
123121
flow-insensitive invariants: 0
124-
total generation entries: 3
122+
total generation entries: 1
125123
[Info][Race] Memory locations race summary:
126124
safe: 1
127125
vulnerable: 0
128126
unsafe: 0
129127
total memory locations: 1
130128

131129
$ yamlWitnessStrip < witness.yml
132-
- entry_type: location_invariant
133-
location:
134-
file_name: 01-priv_nr.c
135-
line: 25
136-
column: 3
137-
function: main
138-
location_invariant:
139-
string: glob1 == 5
140-
type: assertion
141-
format: C
142-
- entry_type: location_invariant
143-
location:
144-
file_name: 01-priv_nr.c
145-
line: 11
146-
column: 3
147-
function: t_fun
148-
location_invariant:
149-
string: glob1 == 5
150-
type: assertion
151-
format: C
152-
- entry_type: location_invariant
153-
location:
154-
file_name: 01-priv_nr.c
155-
line: 11
156-
column: 3
157-
function: t_fun
158-
location_invariant:
159-
string: (unsigned long )arg == 0UL
160-
type: assertion
161-
format: C
130+
- entry_type: invariant_set
131+
content:
132+
- invariant:
133+
type: location_invariant
134+
location:
135+
file_name: 01-priv_nr.c
136+
line: 11
137+
column: 3
138+
function: t_fun
139+
value: (unsigned long )arg == 0UL
140+
format: c_expression
141+
- invariant:
142+
type: location_invariant
143+
location:
144+
file_name: 01-priv_nr.c
145+
line: 11
146+
column: 3
147+
function: t_fun
148+
value: glob1 == 5
149+
format: c_expression
150+
- invariant:
151+
type: location_invariant
152+
location:
153+
file_name: 01-priv_nr.c
154+
line: 25
155+
column: 3
156+
function: main
157+
value: glob1 == 5
158+
format: c_expression
162159

163160
`write+lock` privatization:
164161

165-
$ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization write+lock 01-priv_nr.c
162+
$ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable witness.invariant.other --set ana.base.privatization write+lock 01-priv_nr.c
166163
[Success][Assert] Assertion "glob1 == 5" will succeed (01-priv_nr.c:22:3-22:30)
167164
[Success][Assert] Assertion "t == 5" will succeed (01-priv_nr.c:12:3-12:26)
168165
[Success][Assert] Assertion "glob1 == -10" will succeed (01-priv_nr.c:14:3-14:32)
@@ -175,41 +172,40 @@
175172
location invariants: 3
176173
loop invariants: 0
177174
flow-insensitive invariants: 0
178-
total generation entries: 3
175+
total generation entries: 1
179176
[Info][Race] Memory locations race summary:
180177
safe: 1
181178
vulnerable: 0
182179
unsafe: 0
183180
total memory locations: 1
184181

185182
$ yamlWitnessStrip < witness.yml
186-
- entry_type: location_invariant
187-
location:
188-
file_name: 01-priv_nr.c
189-
line: 25
190-
column: 3
191-
function: main
192-
location_invariant:
193-
string: glob1 == 5
194-
type: assertion
195-
format: C
196-
- entry_type: location_invariant
197-
location:
198-
file_name: 01-priv_nr.c
199-
line: 11
200-
column: 3
201-
function: t_fun
202-
location_invariant:
203-
string: glob1 == 5
204-
type: assertion
205-
format: C
206-
- entry_type: location_invariant
207-
location:
208-
file_name: 01-priv_nr.c
209-
line: 11
210-
column: 3
211-
function: t_fun
212-
location_invariant:
213-
string: (unsigned long )arg == 0UL
214-
type: assertion
215-
format: C
183+
- entry_type: invariant_set
184+
content:
185+
- invariant:
186+
type: location_invariant
187+
location:
188+
file_name: 01-priv_nr.c
189+
line: 11
190+
column: 3
191+
function: t_fun
192+
value: (unsigned long )arg == 0UL
193+
format: c_expression
194+
- invariant:
195+
type: location_invariant
196+
location:
197+
file_name: 01-priv_nr.c
198+
line: 11
199+
column: 3
200+
function: t_fun
201+
value: glob1 == 5
202+
format: c_expression
203+
- invariant:
204+
type: location_invariant
205+
location:
206+
file_name: 01-priv_nr.c
207+
line: 25
208+
column: 3
209+
function: main
210+
value: glob1 == 5
211+
format: c_expression

‎tests/regression/36-apron/12-traces-min-rpb1.t‎

Lines changed: 31 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
$ goblint --enable witness.yaml.enabled --enable warn.deterministic --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.other --disable ana.base.invariant.enabled --set ana.relation.privatization mutex-meet --set ana.activated[+] apron --enable ana.sv-comp.functions --set ana.apron.domain polyhedra 12-traces-min-rpb1.c
1+
$ goblint --enable witness.yaml.enabled --enable warn.deterministic --set witness.yaml.invariant-types '["location_invariant"]' --disable witness.invariant.other --disable ana.base.invariant.enabled --set ana.relation.privatization mutex-meet --set ana.activated[+] apron --enable ana.sv-comp.functions --set ana.apron.domain polyhedra 12-traces-min-rpb1.c
22
[Warning][Assert] Assertion "g == h" is unknown. (12-traces-min-rpb1.c:27:3-27:26)
33
[Success][Assert] Assertion "g == h" will succeed (12-traces-min-rpb1.c:16:3-16:26)
44
[Success][Assert] Assertion "g == h" will succeed (12-traces-min-rpb1.c:29:3-29:26)
@@ -21,39 +21,38 @@
2121
location invariants: 3
2222
loop invariants: 0
2323
flow-insensitive invariants: 0
24-
total generation entries: 3
24+
total generation entries: 1
2525

2626
$ yamlWitnessStrip < witness.yml
27-
- entry_type: location_invariant
28-
location:
29-
file_name: 12-traces-min-rpb1.c
30-
line: 29
31-
column: 3
32-
function: main
33-
location_invariant:
34-
string: (long long )h == (long long )g
35-
type: assertion
36-
format: C
37-
- entry_type: location_invariant
38-
location:
39-
file_name: 12-traces-min-rpb1.c
40-
line: 19
41-
column: 3
42-
function: t_fun
43-
location_invariant:
44-
string: (long long )h == (long long )g
45-
type: assertion
46-
format: C
47-
- entry_type: location_invariant
48-
location:
49-
file_name: 12-traces-min-rpb1.c
50-
line: 14
51-
column: 3
52-
function: t_fun
53-
location_invariant:
54-
string: (long long )h == (long long )g
55-
type: assertion
56-
format: C
27+
- entry_type: invariant_set
28+
content:
29+
- invariant:
30+
type: location_invariant
31+
location:
32+
file_name: 12-traces-min-rpb1.c
33+
line: 14
34+
column: 3
35+
function: t_fun
36+
value: (long long )h == (long long )g
37+
format: c_expression
38+
- invariant:
39+
type: location_invariant
40+
location:
41+
file_name: 12-traces-min-rpb1.c
42+
line: 19
43+
column: 3
44+
function: t_fun
45+
value: (long long )h == (long long )g
46+
format: c_expression
47+
- invariant:
48+
type: location_invariant
49+
location:
50+
file_name: 12-traces-min-rpb1.c
51+
line: 29
52+
column: 3
53+
function: main
54+
value: (long long )h == (long long )g
55+
format: c_expression
5756

5857

5958
$ goblint --enable warn.deterministic --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.sv-comp.functions --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 12-traces-min-rpb1.c --enable ana.apron.invariant.diff-box

0 commit comments

Comments
 (0)