Skip to content

Commit 02996ab

Browse files
committed
Remove remaining references to YAML 0.1 entry types
1 parent 752bd8c commit 02996ab

File tree

6 files changed

+11
-10
lines changed

6 files changed

+11
-10
lines changed

tests/regression/46-apron2/96-witness-mm-escape2.t

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
1-
$ goblint --disable ana.dead-code.lines --disable warn.race --enable warn.deterministic --disable warn.behavior --set witness.yaml.entry-types '["location_invariant"]' --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --enable witness.yaml.enabled --disable witness.invariant.other --disable witness.invariant.loop-head 96-witness-mm-escape2.c --set witness.yaml.path 96-witness-mm-escape2.yml
1+
$ goblint --disable ana.dead-code.lines --disable warn.race --enable warn.deterministic --disable warn.behavior --set witness.yaml.invariant-types '["location_invariant"]' --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --enable witness.yaml.enabled --disable witness.invariant.other --disable witness.invariant.loop-head 96-witness-mm-escape2.c --set witness.yaml.path 96-witness-mm-escape2.yml
22
[Info][Witness] witness generation summary:
33
location invariants: 4
44
loop invariants: 0
55
flow-insensitive invariants: 0
6-
total generation entries: 4
6+
total generation entries: 1
77

8-
$ goblint --disable ana.dead-code.lines --disable warn.race --enable warn.deterministic --disable warn.behavior --set witness.yaml.entry-types '["location_invariant"]' --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 96-witness-mm-escape2.yml 96-witness-mm-escape2.c
8+
$ goblint --disable ana.dead-code.lines --disable warn.race --enable warn.deterministic --disable warn.behavior --set witness.yaml.invariant-types '["location_invariant"]' --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 96-witness-mm-escape2.yml 96-witness-mm-escape2.c
99
[Info][Witness] witness validation summary:
1010
confirmed: 4
1111
unconfirmed: 0

tests/regression/56-witness/08-witness-all-locals.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// CRAM PARAM: --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.all-locals
1+
// CRAM PARAM: --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable witness.invariant.all-locals
22
int main() {
33
int x;
44
x = 5;

tests/regression/56-witness/46-top-bool-invariant.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// PARAM: --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set --disable witness.invariant.inexact-type-bounds
1+
// PARAM: --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set --disable witness.invariant.inexact-type-bounds
22
// CRAM
33
int main() {
44
_Bool x;

tests/regression/56-witness/47-top-int-invariant.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// PARAM: --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set --disable witness.invariant.inexact-type-bounds
1+
// PARAM: --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set --disable witness.invariant.inexact-type-bounds
22
// CRAM
33
int main() {
44
int x;

tests/regression/56-witness/62-tm-inv-transfer-protection-witness.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// PARAM: --set solvers.td3.side_widen never --enable ana.int.interval --set ana.base.privatization protection --set witness.yaml.entry-types[*] location_invariant --set "ana.activated[+]" unassume --set witness.yaml.unassume 62-tm-inv-transfer-protection-witness.yml --enable ana.widen.tokens
1+
// PARAM: --set solvers.td3.side_widen never --enable ana.int.interval --set ana.base.privatization protection --set witness.yaml.invariant-types[*] location_invariant --set "ana.activated[+]" unassume --set witness.yaml.unassume 62-tm-inv-transfer-protection-witness.yml --enable ana.widen.tokens
22
#include <pthread.h>
33
#include <goblint.h>
44

tests/regression/cfg/issue-1356.t/run.t

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,7 @@
9292

9393

9494

95-
$ goblint --enable ana.sv-comp.functions --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' issue-1356.c
95+
$ goblint --enable ana.sv-comp.functions --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' issue-1356.c
9696
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (issue-1356.c:11:10-11:15)
9797
[Info][Deadcode] Logical lines of code (LLoC) summary:
9898
live: 13
@@ -102,7 +102,8 @@
102102
location invariants: 0
103103
loop invariants: 0
104104
flow-insensitive invariants: 0
105-
total generation entries: 0
105+
total generation entries: 1
106106

107107
$ yamlWitnessStrip < witness.yml
108-
[]
108+
- entry_type: invariant_set
109+
content: []

0 commit comments

Comments
 (0)