Filter out-of-invariant exclusion list elements in IntDomTuple invariant

goblint · Jun 19, 2024 · 2408ab6 · 2408ab6
1 parent 39f6c2d
commit 2408ab6
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 35 deletions.
diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
@@ -3803,6 +3803,8 @@ module IntDomTupleImpl = struct
         let min = minimal x in
         let max = maximal x in
         let ns = Option.map fst (to_excl_list x) |? [] in
+        let ns = Option.map_default (fun min -> List.filter (Z.leq min) ns) ns min in
+        let ns = Option.map_default (fun max -> List.filter (Z.geq max) ns) ns max in
         Invariant.(
           IntInvariant.of_interval_opt e ik (min, max) &&
           IntInvariant.of_excl_list e ik ns &&

diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t
@@ -67,7 +67,7 @@
     total lines: 6
   [Warning][Deadcode][CWE-571] condition 'a > 0' (possibly inserted by CIL) is always true (foo.c:3:10-3:20)
   [Info][Witness] witness generation summary:
-    total generation entries: 13
+    total generation entries: 10
 
   $ yamlWitnessStrip < witness.yml
   - entry_type: loop_invariant
@@ -103,17 +103,6 @@
       string: b == 0
       type: assertion
       format: C
-  - entry_type: location_invariant
-    location:
-      file_name: foo.c
-      file_hash: $FILE_HASH
-      line: 7
-      column: 3
-      function: main
-    location_invariant:
-      string: a != 0
-      type: assertion
-      format: C
   - entry_type: location_invariant
     location:
       file_name: foo.c
@@ -147,17 +136,6 @@
       string: b != 0
       type: assertion
       format: C
-  - entry_type: location_invariant
-    location:
-      file_name: foo.c
-      file_hash: $FILE_HASH
-      line: 5
-      column: 5
-      function: main
-    location_invariant:
-      string: a != 1
-      type: assertion
-      format: C
   - entry_type: location_invariant
     location:
       file_name: foo.c
@@ -191,17 +169,6 @@
       string: b != 0
       type: assertion
       format: C
-  - entry_type: location_invariant
-    location:
-      file_name: foo.c
-      file_hash: $FILE_HASH
-      line: 4
-      column: 5
-      function: main
-    location_invariant:
-      string: a != 0
-      type: assertion
-      format: C
   - entry_type: location_invariant
     location:
       file_name: foo.c

diff --git a/tests/regression/witness/int.t/run.t b/tests/regression/witness/int.t/run.t
@@ -29,7 +29,7 @@
       column: 5
       function: main
     location_invariant:
-      string: (51 <= i && i <= 99) && (i != 0 && (51 <= i && i <= 99))
+      string: (51 <= i && i <= 99) && (51 <= i && i <= 99)
       type: assertion
       format: C
   - entry_type: location_invariant