46/{95,96}: Use only location_invariant

goblint · Jan 3, 2025 · a716017 · a716017
1 parent ef51516
commit a716017
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 182 deletions.
diff --git a/tests/regression/46-apron2/95-witness-mm-escape.t b/tests/regression/46-apron2/95-witness-mm-escape.t
@@ -19,11 +19,11 @@
   [Success][Witness] invariant confirmed: g != 0 (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: *b != 0 (95-witness-mm-escape.c:19:1)
   [Info][Witness] witness validation summary:
-    confirmed: 30
+    confirmed: 15
     unconfirmed: 0
     refuted: 0
     error: 0
     unchecked: 0
     unsupported: 0
     disabled: 0
-    total validation entries: 30
+    total validation entries: 15
diff --git a/tests/regression/46-apron2/95-witness-mm-escape.yml b/tests/regression/46-apron2/95-witness-mm-escape.yml
@@ -448,174 +448,3 @@
     string: '*b != 0'
     type: assertion
     format: C
-- entry_type: invariant_set
-  metadata:
-    format_version: "0.1"
-    uuid: 5f4a70a3-8b30-4b5a-a260-56bb341a6283
-    creation_time: 2024-07-16T16:36:39Z
-    producer:
-      name: Goblint
-      version: heads/check_overflow_convert-0-gc35fd8620-dirty
-      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--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'' ''--enable'' ''ana.relation.invariant.one-var''
-        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
-    task:
-      input_files:
-      - 95-witness-mm-escape.c
-      input_file_hashes:
-        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
-      data_model: LP64
-      language: C
-  content:
-  - invariant:
-      type: location_invariant
-      location:
-        file_name: 95-witness-mm-escape.c
-        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
-        line: 19
-        column: 1
-        function: main
-      value: 0 <= g
-      format: c_expression
-  - invariant:
-      type: location_invariant
-      location:
-        file_name: 95-witness-mm-escape.c
-        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
-        line: 19
-        column: 1
-        function: main
-      value: 0 <= *b
-      format: c_expression
-  - invariant:
-      type: location_invariant
-      location:
-        file_name: 95-witness-mm-escape.c
-        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
-        line: 19
-        column: 1
-        function: main
-      value: g <= 127
-      format: c_expression
-  - invariant:
-      type: location_invariant
-      location:
-        file_name: 95-witness-mm-escape.c
-        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
-        line: 19
-        column: 1
-        function: main
-      value: '*b <= 127'
-      format: c_expression
-  - invariant:
-      type: location_invariant
-      location:
-        file_name: 95-witness-mm-escape.c
-        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
-        line: 19
-        column: 1
-        function: main
-      value: -8LL + (long long )g >= 0LL
-      format: c_expression
-  - invariant:
-      type: location_invariant
-      location:
-        file_name: 95-witness-mm-escape.c
-        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
-        line: 19
-        column: 1
-        function: main
-      value: 2147483648LL + (long long )a >= 0LL
-      format: c_expression
-  - invariant:
-      type: location_invariant
-      location:
-        file_name: 95-witness-mm-escape.c
-        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
-        line: 19
-        column: 1
-        function: main
-      value: (2147483638LL + (long long )a) + (long long )g >= 0LL
-      format: c_expression
-  - invariant:
-      type: location_invariant
-      location:
-        file_name: 95-witness-mm-escape.c
-        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
-        line: 19
-        column: 1
-        function: main
-      value: (2147483637LL - (long long )a) + (long long )g >= 0LL
-      format: c_expression
-  - invariant:
-      type: location_invariant
-      location:
-        file_name: 95-witness-mm-escape.c
-        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
-        line: 19
-        column: 1
-        function: main
-      value: 10LL - (long long )g >= 0LL
-      format: c_expression
-  - invariant:
-      type: location_invariant
-      location:
-        file_name: 95-witness-mm-escape.c
-        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
-        line: 19
-        column: 1
-        function: main
-      value: 2147483647LL - (long long )a >= 0LL
-      format: c_expression
-  - invariant:
-      type: location_invariant
-      location:
-        file_name: 95-witness-mm-escape.c
-        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
-        line: 19
-        column: 1
-        function: main
-      value: (2147483658LL + (long long )a) - (long long )g >= 0LL
-      format: c_expression
-  - invariant:
-      type: location_invariant
-      location:
-        file_name: 95-witness-mm-escape.c
-        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
-        line: 19
-        column: 1
-        function: main
-      value: (2147483657LL - (long long )a) - (long long )g >= 0LL
-      format: c_expression
-  - invariant:
-      type: location_invariant
-      location:
-        file_name: 95-witness-mm-escape.c
-        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
-        line: 19
-        column: 1
-        function: main
-      value: b == & g
-      format: c_expression
-  - invariant:
-      type: location_invariant
-      location:
-        file_name: 95-witness-mm-escape.c
-        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
-        line: 19
-        column: 1
-        function: main
-      value: g != 0
-      format: c_expression
-  - invariant:
-      type: location_invariant
-      location:
-        file_name: 95-witness-mm-escape.c
-        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
-        line: 19
-        column: 1
-        function: main
-      value: '*b != 0'
-      format: c_expression
diff --git a/tests/regression/46-apron2/96-witness-mm-escape2.t b/tests/regression/46-apron2/96-witness-mm-escape2.t
@@ -1,21 +1,20 @@
-  $ goblint --disable ana.dead-code.lines --disable warn.race --enable warn.deterministic --disable warn.behavior --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
+  $ 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
   [Info][Witness] witness generation summary:
-    location invariants: 8
+    location invariants: 4
     loop invariants: 0
-    flow-insensitive invariants: 1
-    total generation entries: 6
+    flow-insensitive invariants: 0
+    total generation entries: 4
 
-  $ goblint --disable ana.dead-code.lines --disable warn.race --enable warn.deterministic --disable warn.behavior --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
-  [Warning][Witness] cannot validate entry of type flow_insensitive_invariant
+  $ 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
   [Info][Witness] witness validation summary:
-    confirmed: 8
+    confirmed: 4
     unconfirmed: 0
     refuted: 0
     error: 0
     unchecked: 0
-    unsupported: 1
+    unsupported: 0
     disabled: 0
-    total validation entries: 9
+    total validation entries: 4
   [Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (96-witness-mm-escape2.c:8:5)
   [Success][Witness] invariant confirmed: -128 <= g (96-witness-mm-escape2.c:22:1)
   [Success][Witness] invariant confirmed: g != 0 (96-witness-mm-escape2.c:22:1)