Skip to content

Commit 841fb4f

Browse files
sim642sim642
authored
Merge pull request #1718 from goblint/yaml-witness-default
Change YAML witness generation default to version 2.0 with only `invariant_set`
2 parents 52a3bbb + 8a079a4 commit 841fb4f

File tree

70 files changed

+56
-370
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

70 files changed

+56
-370
lines changed

‎src/config/options.schema.json

+1-6
Original file line numberDiff line numberDiff line change
@@ -2812,7 +2812,7 @@
28122812
"2.0",
28132813
"2.1"
28142814
],
2815-
"default": "0.1"
2815+
"default": "2.0"
28162816
},
28172817
"entry-types": {
28182818
"title": "witness.yaml.entry-types",
@@ -2833,11 +2833,6 @@
28332833
]
28342834
},
28352835
"default": [
2836-
"location_invariant",
2837-
"loop_invariant",
2838-
"flow_insensitive_invariant",
2839-
"loop_invariant_certificate",
2840-
"precondition_loop_invariant_certificate",
28412836
"invariant_set"
28422837
]
28432838
},

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

-12
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,6 @@
2424
- entry_type: location_invariant
2525
location:
2626
file_name: 01-priv_nr.c
27-
file_hash: $FILE_HASH
2827
line: 25
2928
column: 3
3029
function: main
@@ -35,7 +34,6 @@
3534
- entry_type: location_invariant
3635
location:
3736
file_name: 01-priv_nr.c
38-
file_hash: $FILE_HASH
3937
line: 11
4038
column: 3
4139
function: t_fun
@@ -46,7 +44,6 @@
4644
- entry_type: location_invariant
4745
location:
4846
file_name: 01-priv_nr.c
49-
file_hash: $FILE_HASH
5047
line: 11
5148
column: 3
5249
function: t_fun
@@ -81,7 +78,6 @@
8178
- entry_type: location_invariant
8279
location:
8380
file_name: 01-priv_nr.c
84-
file_hash: $FILE_HASH
8581
line: 25
8682
column: 3
8783
function: main
@@ -92,7 +88,6 @@
9288
- entry_type: location_invariant
9389
location:
9490
file_name: 01-priv_nr.c
95-
file_hash: $FILE_HASH
9691
line: 11
9792
column: 3
9893
function: t_fun
@@ -103,7 +98,6 @@
10398
- entry_type: location_invariant
10499
location:
105100
file_name: 01-priv_nr.c
106-
file_hash: $FILE_HASH
107101
line: 11
108102
column: 3
109103
function: t_fun
@@ -138,7 +132,6 @@
138132
- entry_type: location_invariant
139133
location:
140134
file_name: 01-priv_nr.c
141-
file_hash: $FILE_HASH
142135
line: 25
143136
column: 3
144137
function: main
@@ -149,7 +142,6 @@
149142
- entry_type: location_invariant
150143
location:
151144
file_name: 01-priv_nr.c
152-
file_hash: $FILE_HASH
153145
line: 11
154146
column: 3
155147
function: t_fun
@@ -160,7 +152,6 @@
160152
- entry_type: location_invariant
161153
location:
162154
file_name: 01-priv_nr.c
163-
file_hash: $FILE_HASH
164155
line: 11
165156
column: 3
166157
function: t_fun
@@ -195,7 +186,6 @@
195186
- entry_type: location_invariant
196187
location:
197188
file_name: 01-priv_nr.c
198-
file_hash: $FILE_HASH
199189
line: 25
200190
column: 3
201191
function: main
@@ -206,7 +196,6 @@
206196
- entry_type: location_invariant
207197
location:
208198
file_name: 01-priv_nr.c
209-
file_hash: $FILE_HASH
210199
line: 11
211200
column: 3
212201
function: t_fun
@@ -217,7 +206,6 @@
217206
- entry_type: location_invariant
218207
location:
219208
file_name: 01-priv_nr.c
220-
file_hash: $FILE_HASH
221209
line: 11
222210
column: 3
223211
function: t_fun

‎tests/regression/13-privatized/04-priv_multi.t

+3-25
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,6 @@
5151
ghost_updates:
5252
- location:
5353
file_name: 04-priv_multi.c
54-
file_hash: $FILE_HASH
5554
line: 15
5655
column: 5
5756
function: generate
@@ -61,7 +60,6 @@
6160
format: c_expression
6261
- location:
6362
file_name: 04-priv_multi.c
64-
file_hash: $FILE_HASH
6563
line: 18
6664
column: 5
6765
function: generate
@@ -71,7 +69,6 @@
7169
format: c_expression
7270
- location:
7371
file_name: 04-priv_multi.c
74-
file_hash: $FILE_HASH
7572
line: 26
7673
column: 5
7774
function: process
@@ -81,7 +78,6 @@
8178
format: c_expression
8279
- location:
8380
file_name: 04-priv_multi.c
84-
file_hash: $FILE_HASH
8581
line: 29
8682
column: 7
8783
function: process
@@ -91,7 +87,6 @@
9187
format: c_expression
9288
- location:
9389
file_name: 04-priv_multi.c
94-
file_hash: $FILE_HASH
9590
line: 32
9691
column: 7
9792
function: process
@@ -101,7 +96,6 @@
10196
format: c_expression
10297
- location:
10398
file_name: 04-priv_multi.c
104-
file_hash: $FILE_HASH
10599
line: 34
106100
column: 7
107101
function: process
@@ -111,7 +105,6 @@
111105
format: c_expression
112106
- location:
113107
file_name: 04-priv_multi.c
114-
file_hash: $FILE_HASH
115108
line: 46
116109
column: 5
117110
function: dispose
@@ -121,7 +114,6 @@
121114
format: c_expression
122115
- location:
123116
file_name: 04-priv_multi.c
124-
file_hash: $FILE_HASH
125117
line: 49
126118
column: 7
127119
function: dispose
@@ -131,7 +123,6 @@
131123
format: c_expression
132124
- location:
133125
file_name: 04-priv_multi.c
134-
file_hash: $FILE_HASH
135126
line: 63
136127
column: 3
137128
function: main
@@ -141,7 +132,6 @@
141132
format: c_expression
142133
- location:
143134
file_name: 04-priv_multi.c
144-
file_hash: $FILE_HASH
145135
line: 68
146136
column: 5
147137
function: main
@@ -151,7 +141,6 @@
151141
format: c_expression
152142
- location:
153143
file_name: 04-priv_multi.c
154-
file_hash: $FILE_HASH
155144
line: 69
156145
column: 5
157146
function: main
@@ -161,7 +150,6 @@
161150
format: c_expression
162151
- location:
163152
file_name: 04-priv_multi.c
164-
file_hash: $FILE_HASH
165153
line: 73
166154
column: 5
167155
function: main
@@ -171,7 +159,6 @@
171159
format: c_expression
172160
- location:
173161
file_name: 04-priv_multi.c
174-
file_hash: $FILE_HASH
175162
line: 74
176163
column: 5
177164
function: main
@@ -230,38 +217,35 @@ Flow-insensitive invariants as location invariants.
230217
Location invariant at `for` loop in `main` should be on column 3, not 7.
231218

232219
$ diff witness.flow_insensitive.yml witness.location.yml
233-
153,154c153,160
220+
140,141c140,146
234221
< - entry_type: flow_insensitive_invariant
235222
< flow_insensitive_invariant:
236223
---
237224
> - entry_type: location_invariant
238225
> location:
239226
> file_name: 04-priv_multi.c
240-
> file_hash: $FILE_HASH
241227
> line: 67
242228
> column: 3
243229
> function: main
244230
> location_invariant:
245-
158,159c164,171
231+
145,146c150,156
246232
< - entry_type: flow_insensitive_invariant
247233
< flow_insensitive_invariant:
248234
---
249235
> - entry_type: location_invariant
250236
> location:
251237
> file_name: 04-priv_multi.c
252-
> file_hash: $FILE_HASH
253238
> line: 67
254239
> column: 3
255240
> function: main
256241
> location_invariant:
257-
163,164c175,248
242+
150,151c160,226
258243
< - entry_type: flow_insensitive_invariant
259244
< flow_insensitive_invariant:
260245
---
261246
> - entry_type: location_invariant
262247
> location:
263248
> file_name: 04-priv_multi.c
264-
> file_hash: $FILE_HASH
265249
> line: 67
266250
> column: 3
267251
> function: main
@@ -272,7 +256,6 @@ Location invariant at `for` loop in `main` should be on column 3, not 7.
272256
> - entry_type: location_invariant
273257
> location:
274258
> file_name: 04-priv_multi.c
275-
> file_hash: $FILE_HASH
276259
> line: 65
277260
> column: 3
278261
> function: main
@@ -283,7 +266,6 @@ Location invariant at `for` loop in `main` should be on column 3, not 7.
283266
> - entry_type: location_invariant
284267
> location:
285268
> file_name: 04-priv_multi.c
286-
> file_hash: $FILE_HASH
287269
> line: 65
288270
> column: 3
289271
> function: main
@@ -294,7 +276,6 @@ Location invariant at `for` loop in `main` should be on column 3, not 7.
294276
> - entry_type: location_invariant
295277
> location:
296278
> file_name: 04-priv_multi.c
297-
> file_hash: $FILE_HASH
298279
> line: 65
299280
> column: 3
300281
> function: main
@@ -305,7 +286,6 @@ Location invariant at `for` loop in `main` should be on column 3, not 7.
305286
> - entry_type: location_invariant
306287
> location:
307288
> file_name: 04-priv_multi.c
308-
> file_hash: $FILE_HASH
309289
> line: 64
310290
> column: 3
311291
> function: main
@@ -316,7 +296,6 @@ Location invariant at `for` loop in `main` should be on column 3, not 7.
316296
> - entry_type: location_invariant
317297
> location:
318298
> file_name: 04-priv_multi.c
319-
> file_hash: $FILE_HASH
320299
> line: 64
321300
> column: 3
322301
> function: main
@@ -327,7 +306,6 @@ Location invariant at `for` loop in `main` should be on column 3, not 7.
327306
> - entry_type: location_invariant
328307
> location:
329308
> file_name: 04-priv_multi.c
330-
> file_hash: $FILE_HASH
331309
> line: 64
332310
> column: 3
333311
> function: main

‎tests/regression/13-privatized/25-struct_nr.t

-5
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,6 @@
3737
ghost_updates:
3838
- location:
3939
file_name: 25-struct_nr.c
40-
file_hash: $FILE_HASH
4140
line: 14
4241
column: 3
4342
function: t_fun
@@ -47,7 +46,6 @@
4746
format: c_expression
4847
- location:
4948
file_name: 25-struct_nr.c
50-
file_hash: $FILE_HASH
5149
line: 20
5250
column: 3
5351
function: t_fun
@@ -57,7 +55,6 @@
5755
format: c_expression
5856
- location:
5957
file_name: 25-struct_nr.c
60-
file_hash: $FILE_HASH
6158
line: 27
6259
column: 3
6360
function: main
@@ -67,7 +64,6 @@
6764
format: c_expression
6865
- location:
6966
file_name: 25-struct_nr.c
70-
file_hash: $FILE_HASH
7167
line: 28
7268
column: 3
7369
function: main
@@ -77,7 +73,6 @@
7773
format: c_expression
7874
- location:
7975
file_name: 25-struct_nr.c
80-
file_hash: $FILE_HASH
8176
line: 32
8277
column: 3
8378
function: main

0 commit comments

Comments
 (0)