Convert unassume precision YAML witnesses to invariant_set

sim642 · sim642 · commit d155e9e29a4d · 2025-09-02T11:45:58.000+03:00
diff --git a/tests/regression/56-witness/26-mine-tutorial-ex4.6.c b/tests/regression/56-witness/26-mine-tutorial-ex4.6.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 26-mine-tutorial-ex4.6.yml
+// PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 26-mine-tutorial-ex4.6.yml
 #include <goblint.h>
 int main() {
   int x = 40;
diff --git a/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml b/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml
@@ -1,6 +1,6 @@
-- entry_type: loop_invariant
+- entry_type: invariant_set
   metadata:
-    format_version: "0.1"
+    format_version: "2.0"
     uuid: 0e84a9de-b9f6-44dd-ab8d-ebdeca941482
     creation_time: 2022-10-07T09:14:31Z
     producer:
@@ -13,13 +13,13 @@
         26-mine-tutorial-ex4.6.c: e119cc77f5ce2a60d7c2b65c5dfbe8037f877b5621deab62b9580c5bbdebd97b
       data_model: LP64
       language: C
-  location:
-    file_name: 26-mine-tutorial-ex4.6.c
-    file_hash: e119cc77f5ce2a60d7c2b65c5dfbe8037f877b5621deab62b9580c5bbdebd97b
-    line: 5
-    column: 3
-    function: main
-  loop_invariant:
-    string: 0 <= x && x <= 40
-    type: assertion
-    format: C
+  content:
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 26-mine-tutorial-ex4.6.c
+        line: 5
+        column: 3
+        function: main
+      value: 0 <= x && x <= 40
+      format: c_expression
diff --git a/tests/regression/56-witness/27-mine-tutorial-ex4.7.c b/tests/regression/56-witness/27-mine-tutorial-ex4.7.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 27-mine-tutorial-ex4.7.yml
+// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions --set ana.activated[+] unassume --set witness.yaml.unassume 27-mine-tutorial-ex4.7.yml
 #include <goblint.h>
 extern _Bool __VERIFIER_nondet_bool();
 int main() {
diff --git a/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml b/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml
@@ -1,6 +1,6 @@
-- entry_type: loop_invariant
+- entry_type: invariant_set
   metadata:
-    format_version: "0.1"
+    format_version: "2.0"
     uuid: e17f9860-95af-4213-a767-ab4876ead27e
     creation_time: 2022-10-07T10:33:01Z
     producer:
@@ -13,13 +13,13 @@
         27-mine-tutorial-ex4.7.c: 4d06e38718d405171bd503e630f6c7a247bb3b0d3c1c6c951466e4989883b43c
       data_model: LP64
       language: C
-  location:
-    file_name: 27-mine-tutorial-ex4.7.c
-    file_hash: 4d06e38718d405171bd503e630f6c7a247bb3b0d3c1c6c951466e4989883b43c
-    line: 6
-    column: 3
-    function: main
-  loop_invariant:
-    string: 0 <= x && x <= 40
-    type: assertion
-    format: C
+  content:
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 27-mine-tutorial-ex4.7.c
+        line: 6
+        column: 3
+        function: main
+      value: 0 <= x && x <= 40
+      format: c_expression
diff --git a/tests/regression/56-witness/28-mine-tutorial-ex4.8.c b/tests/regression/56-witness/28-mine-tutorial-ex4.8.c
@@ -1,4 +1,4 @@
-// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 28-mine-tutorial-ex4.8.yml
+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.activated[+] unassume --set witness.yaml.unassume 28-mine-tutorial-ex4.8.yml
 #include <goblint.h>
 extern _Bool __VERIFIER_nondet_bool();
 int main() {
diff --git a/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml b/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml
@@ -1,6 +1,6 @@
-- entry_type: loop_invariant
+- entry_type: invariant_set
   metadata:
-    format_version: "0.1"
+    format_version: "2.0"
     uuid: 299c2080-fb13-4879-be2b-5d2758465577
     creation_time: 2022-10-07T10:36:41Z
     producer:
@@ -13,13 +13,13 @@
         28-mine-tutorial-ex4.8.c: bd5b719b0d268dd7669edc1dd21b55a2bacab3187f26f112839093b910c91347
       data_model: LP64
       language: C
-  location:
-    file_name: 28-mine-tutorial-ex4.8.c
-    file_hash: bd5b719b0d268dd7669edc1dd21b55a2bacab3187f26f112839093b910c91347
-    line: 6
-    column: 3
-    function: main
-  loop_invariant:
-    string: 0 <= v && v <= 1
-    type: assertion
-    format: C
+  content:
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 28-mine-tutorial-ex4.8.c
+        line: 6
+        column: 3
+        function: main
+      value: 0 <= v && v <= 1
+      format: c_expression
diff --git a/tests/regression/56-witness/29-mine-tutorial-ex4.10.c b/tests/regression/56-witness/29-mine-tutorial-ex4.10.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 29-mine-tutorial-ex4.10.yml
+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set ana.activated[+] unassume --set witness.yaml.unassume 29-mine-tutorial-ex4.10.yml
 // Using Apron polyhedra to have no narrowing.
 #include <goblint.h>
 int main() {
diff --git a/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml b/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml
@@ -1,6 +1,6 @@
-- entry_type: loop_invariant
+- entry_type: invariant_set
   metadata:
-    format_version: "0.1"
+    format_version: "2.0"
     uuid: f04fe372-3d6e-4a80-9567-80c64bd7fd03
     creation_time: 2022-10-07T10:47:08Z
     producer:
@@ -13,13 +13,13 @@
         29-mine-tutorial-ex4.10.c: e0399cba2a1ab555c14e500606561777d5f029de891ea5bf3cfd8bda880a7ac8
       data_model: LP64
       language: C
-  location:
-    file_name: 29-mine-tutorial-ex4.10.c
-    file_hash: e0399cba2a1ab555c14e500606561777d5f029de891ea5bf3cfd8bda880a7ac8
-    line: 6
-    column: 3
-    function: main
-  loop_invariant:
-    string: 1 <= v && v <= 52
-    type: assertion
-    format: C
+  content:
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 29-mine-tutorial-ex4.10.c
+        line: 6
+        column: 3
+        function: main
+      value: 1 <= v && v <= 52
+      format: c_expression
diff --git a/tests/regression/56-witness/35-hh-ex1b.c b/tests/regression/56-witness/35-hh-ex1b.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --disable solvers.td3.remove-wpoint --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 35-hh-ex1b.yml
+// PARAM: --enable ana.int.interval --disable solvers.td3.remove-wpoint --set ana.activated[+] unassume --set witness.yaml.unassume 35-hh-ex1b.yml
 #include <goblint.h>
 int main() {
   int i = 0;
diff --git a/tests/regression/56-witness/35-hh-ex1b.yml b/tests/regression/56-witness/35-hh-ex1b.yml
@@ -1,6 +1,6 @@
-- entry_type: loop_invariant
+- entry_type: invariant_set
   metadata:
-    format_version: "0.1"
+    format_version: "2.0"
     uuid: 1a354f1e-76e8-40e9-808a-8d5efbe35496
     creation_time: 2022-10-12T10:45:49Z
     producer:
@@ -13,13 +13,13 @@
         35-hh-ex1b.c: 9fe07d5f950140350848bae4342d9d1b7c6c9f625f6985746089a36a37243600
       data_model: LP64
       language: C
-  location:
-    file_name: 35-hh-ex1b.c
-    file_hash: 9fe07d5f950140350848bae4342d9d1b7c6c9f625f6985746089a36a37243600
-    line: 7
-    column: 5
-    function: main
-  loop_invariant:
-    string: 0 <= i && i <= 99
-    type: assertion
-    format: C
+  content:
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 35-hh-ex1b.c
+        line: 7
+        column: 5
+        function: main
+      value: 0 <= i && i <= 99
+      format: c_expression
diff --git a/tests/regression/56-witness/36-hh-ex2b.c b/tests/regression/56-witness/36-hh-ex2b.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 36-hh-ex2b.yml
+// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions --set ana.activated[+] unassume --set witness.yaml.unassume 36-hh-ex2b.yml
 #include <goblint.h>
 extern _Bool __VERIFIER_nondet_bool();
 int main() {
diff --git a/tests/regression/56-witness/36-hh-ex2b.yml b/tests/regression/56-witness/36-hh-ex2b.yml
@@ -1,6 +1,6 @@
-- entry_type: loop_invariant
+- entry_type: invariant_set
   metadata:
-    format_version: "0.1"
+    format_version: "2.0"
     uuid: 9589b9d4-edce-4043-8413-279703946762
     creation_time: 2022-10-12T10:38:16Z
     producer:
@@ -13,13 +13,13 @@
         36-hh-ex2b.c: e4a0ecee56af00cc83ce75411061e74f80edce8c562310a7ea11499eb606d133
       data_model: LP64
       language: C
-  location:
-    file_name: 36-hh-ex2b.c
-    file_hash: e4a0ecee56af00cc83ce75411061e74f80edce8c562310a7ea11499eb606d133
-    line: 6
-    column: 3
-    function: main
-  loop_invariant:
-    string: 0 <= n && n <= 60
-    type: assertion
-    format: C
+  content:
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 36-hh-ex2b.c
+        line: 6
+        column: 3
+        function: main
+      value: 0 <= n && n <= 60
+      format: c_expression
diff --git a/tests/regression/56-witness/37-hh-ex3.c b/tests/regression/56-witness/37-hh-ex3.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --enable ana.apron.strengthening --disable solvers.td3.remove-wpoint --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 37-hh-ex3.yml
+// SKIP PARAM: --set ana.activated[+] apron --enable ana.apron.strengthening --disable solvers.td3.remove-wpoint --set ana.activated[+] unassume --set witness.yaml.unassume 37-hh-ex3.yml
 #include <goblint.h>
 int main() {
   int i = 0;
diff --git a/tests/regression/56-witness/37-hh-ex3.yml b/tests/regression/56-witness/37-hh-ex3.yml
@@ -1,6 +1,6 @@
-- entry_type: location_invariant
+- entry_type: invariant_set
   metadata:
-    format_version: "0.1"
+    format_version: "2.0"
     uuid: d834761a-d0d7-4fea-bf42-2ff2b9a19143
     creation_time: 2022-10-12T10:59:25Z
     producer:
@@ -13,13 +13,13 @@
         37-hh-ex3.c: 9c984e89a790b595d2b37ca8a05e5967a15130592cb2567fac2fae4aff668a4f
       data_model: LP64
       language: C
-  location:
-    file_name: 37-hh-ex3.c
-    file_hash: 9c984e89a790b595d2b37ca8a05e5967a15130592cb2567fac2fae4aff668a4f
-    line: 6
-    column: 5
-    function: main
-  location_invariant:
-    string: 0 <= i && i <= 3
-    type: assertion
-    format: C
+  content:
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 37-hh-ex3.c
+        line: 6
+        column: 5
+        function: main
+      value: 0 <= i && i <= 3
+      format: c_expression
diff --git a/tests/regression/56-witness/38-bh-ex3.c b/tests/regression/56-witness/38-bh-ex3.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 38-bh-ex3.yml
+// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions --set ana.activated[+] unassume --set witness.yaml.unassume 38-bh-ex3.yml
 #include <goblint.h>
 extern _Bool __VERIFIER_nondet_bool();
 int main() {
diff --git a/tests/regression/56-witness/38-bh-ex3.yml b/tests/regression/56-witness/38-bh-ex3.yml
@@ -1,6 +1,6 @@
-- entry_type: loop_invariant
+- entry_type: invariant_set
   metadata:
-    format_version: "0.1"
+    format_version: "2.0"
     uuid: bd436e09-244f-45db-a5f4-9337ca997424
     creation_time: 2022-10-12T11:13:15Z
     producer:
@@ -13,13 +13,13 @@
         38-bh-ex3.c: 9d2cb05c2decf8564defade7194c336478ec5ae4be1ee79202269ff09830dada
       data_model: LP64
       language: C
-  location:
-    file_name: 38-bh-ex3.c
-    file_hash: 9d2cb05c2decf8564defade7194c336478ec5ae4be1ee79202269ff09830dada
-    line: 7
-    column: 3
-    function: main
-  loop_invariant:
-    string: 0 <= m && m <= 60 && 0 <= n && n <= 60
-    type: assertion
-    format: C
+  content:
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 38-bh-ex3.c
+        line: 7
+        column: 3
+        function: main
+      value: 0 <= m && m <= 60 && 0 <= n && n <= 60
+      format: c_expression
diff --git a/tests/regression/56-witness/39-bh-ex-add.c b/tests/regression/56-witness/39-bh-ex-add.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 39-bh-ex-add.yml
+// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions --set ana.activated[+] unassume --set witness.yaml.unassume 39-bh-ex-add.yml
 #include <goblint.h>
 extern _Bool __VERIFIER_nondet_bool();
 int main() {
diff --git a/tests/regression/56-witness/39-bh-ex-add.yml b/tests/regression/56-witness/39-bh-ex-add.yml
@@ -1,6 +1,6 @@
-- entry_type: loop_invariant
+- entry_type: invariant_set
   metadata:
-    format_version: "0.1"
+    format_version: "2.0"
     uuid: bd436e09-244f-45db-a5f4-9337ca997424
     creation_time: 2022-10-12T11:13:15Z
     producer:
@@ -13,13 +13,13 @@
         39-bh-ex-add.c: 9d2cb05c2decf8564defade7194c336478ec5ae4be1ee79202269ff09830dada
       data_model: LP64
       language: C
-  location:
-    file_name: 39-bh-ex-add.c
-    file_hash: 9d2cb05c2decf8564defade7194c336478ec5ae4be1ee79202269ff09830dada
-    line: 7
-    column: 3
-    function: main
-  loop_invariant:
-    string: 0 <= m && m <= 60 && 0 <= n && n <= 60
-    type: assertion
-    format: C
+  content:
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 39-bh-ex-add.c
+        line: 7
+        column: 3
+        function: main
+      value: 0 <= m && m <= 60 && 0 <= n && n <= 60
+      format: c_expression
diff --git a/tests/regression/56-witness/40-bh-ex1-poly.c b/tests/regression/56-witness/40-bh-ex1-poly.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 40-bh-ex1-poly.yml --set sem.int.signed_overflow assume_none
+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set ana.activated[+] unassume --set witness.yaml.unassume 40-bh-ex1-poly.yml --set sem.int.signed_overflow assume_none
 // TODO: why need to assume no overflow?
 #include <goblint.h>
 int main() {
diff --git a/tests/regression/56-witness/40-bh-ex1-poly.yml b/tests/regression/56-witness/40-bh-ex1-poly.yml
@@ -1,6 +1,6 @@
-- entry_type: location_invariant
+- entry_type: invariant_set
   metadata:
-    format_version: "0.1"
+    format_version: "2.0"
     uuid: 6ee08942-60e6-4291-a9fc-ff6f2744ef4b
     creation_time: 2022-10-12T11:19:46Z
     producer:
@@ -13,13 +13,13 @@
         40-bh-ex1-poly.c: 34f781dcae089ecb6b7b2811027395fcb501b8477b7e5016f7b38081724bea28
       data_model: LP64
       language: C
-  location:
-    file_name: 40-bh-ex1-poly.c
-    file_hash: 34f781dcae089ecb6b7b2811027395fcb501b8477b7e5016f7b38081724bea28
-    line: 7
-    column: 5
-    function: main
-  location_invariant:
-    string: 0 <= i && i <= 3
-    type: assertion
-    format: C
+  content:
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 40-bh-ex1-poly.c
+        line: 7
+        column: 5
+        function: main
+      value: 0 <= i && i <= 3
+      format: c_expression
diff --git a/tests/regression/56-witness/41-as-hybrid.c b/tests/regression/56-witness/41-as-hybrid.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 41-as-hybrid.yml
+// PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 41-as-hybrid.yml
 #include <goblint.h>
 int main() {
   int i = 0;
diff --git a/tests/regression/56-witness/41-as-hybrid.yml b/tests/regression/56-witness/41-as-hybrid.yml

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-// PARAM: --enable ana.int.interval --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 26-mine-tutorial-ex4.6.yml`
	`1`	`+// PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 26-mine-tutorial-ex4.6.yml`
`2`	`2`	`#include <goblint.h>`
`3`	`3`	`int main() {`
`4`	`4`	`int x = 40;`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 28-mine-tutorial-ex4.8.yml`
	`1`	`+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.activated[+] unassume --set witness.yaml.unassume 28-mine-tutorial-ex4.8.yml`
`2`	`2`	`#include <goblint.h>`
`3`	`3`	`extern _Bool __VERIFIER_nondet_bool();`
`4`	`4`	`int main() {`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 29-mine-tutorial-ex4.10.yml`
	`1`	`+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set ana.activated[+] unassume --set witness.yaml.unassume 29-mine-tutorial-ex4.10.yml`
`2`	`2`	`// Using Apron polyhedra to have no narrowing.`
`3`	`3`	`#include <goblint.h>`
`4`	`4`	`int main() {`