Fix var_eq not limiting to queried lval invariants

goblint · Nov 3, 2023 · 9e26114 · 9e26114
1 parent a3e2f45
commit 9e26114
Showing 1 changed file with 9 additions and 1 deletion.
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
@@ -566,7 +566,15 @@ struct
       r
     | Queries.Invariant context when GobConfig.get_bool "witness.invariant.exact" -> (* only exact equalities here *)
       let scope = Node.find_fundec ctx.node in
-      D.invariant ~scope ctx.local
+      if Lval.Set.is_top context.lvals then
+        D.invariant ~scope ctx.local
+      else (
+        Lval.Set.fold (fun lval acc ->
+            match D.find_class (Lval lval) ctx.local with
+            | None -> acc
+            | Some c -> Invariant.(acc && D.invariant ~scope (D.singleton c))
+          ) context.lvals (Invariant.top ())
+      )
     | _ -> Queries.Result.top x
 
   let event ctx e octx =