Count witness.invariant.flow_insensitive-as location invariants in su…

…mmary
goblint · Nov 29, 2024 · ffe255b · ffe255b
1 parent 3369955
commit ffe255b
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 3 deletions.
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
@@ -385,6 +385,7 @@ struct
                   fold_flow_insensitive_as_location ~inv (fun ~location ~inv acc ->
                       let invariant = Entry.invariant (CilType.Exp.show inv) in
                       let entry = Entry.location_invariant ~task ~location ~invariant in
+                      incr cnt_location_invariant;
                       entry :: acc
                     ) acc
                 | `Lifted _, _
@@ -605,6 +606,7 @@ struct
                       fold_flow_insensitive_as_location ~inv (fun ~location ~inv acc ->
                           let invariant = CilType.Exp.show inv in
                           let invariant = Entry.location_invariant' ~location ~invariant in
+                          incr cnt_location_invariant;
                           invariant :: acc
                         ) acc
                     | `Bot | `Top -> (* global bot might only be possible for alloc variables, if at all, so emit nothing *)

diff --git a/tests/regression/13-privatized/04-priv_multi.t b/tests/regression/13-privatized/04-priv_multi.t
@@ -215,7 +215,7 @@ Flow-insensitive invariants as location invariants.
   [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (04-priv_multi.c:45:10-45:11)
   [Warning][Deadcode][CWE-571] condition 'B > 0' is always true (04-priv_multi.c:47:9-47:14)
   [Info][Witness] witness generation summary:
-    location invariants: 0
+    location invariants: 9
     loop invariants: 0
     flow-insensitive invariants: 0
     total generation entries: 10

diff --git a/tests/regression/13-privatized/74-mutex.t b/tests/regression/13-privatized/74-mutex.t
@@ -108,7 +108,7 @@ Flow-insensitive invariants as location invariants.
     total lines: 15
   [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (74-mutex.c:19:10-19:11)
   [Info][Witness] witness generation summary:
-    location invariants: 0
+    location invariants: 2
     loop invariants: 0
     flow-insensitive invariants: 0
     total generation entries: 3
@@ -177,7 +177,7 @@ Same with ghost_instrumentation and invariant_set entries.
     total lines: 15
   [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (74-mutex.c:19:10-19:11)
   [Info][Witness] witness generation summary:
-    location invariants: 0
+    location invariants: 2
     loop invariants: 0
     flow-insensitive invariants: 0
     total generation entries: 2