diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index e3978f9929..9d04b597fa 100644 --- 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 index af7c9b2098..1f6dff3fdc 100644 --- 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 index 1d750a211c..4b370db387 100644 --- 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