From c9b639aa17025bd428f5eb78b3b94987cc67b5fb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 28 Apr 2023 17:02:50 +0200
Subject: [PATCH] [Eva] Octagons: always infers modified zone in [assign]
transfer function.
---
src/plugins/eva/domains/octagons.ml | 2 ++
1 file changed, 2 insertions(+)
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index bd50d179591..89e5a9b843d 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -1752,6 +1752,8 @@ module Domain = struct
let variable = Variable.make_lval lvalue in
(* Remove lvals refering to the variable *)
let lvalue_zone = (eval_deps variable).data in
+ let modified = Locations.Zone.join state.modified lvalue_zone in
+ let state = { state with modified } in
let vars = Deps.intersects_zone state.deps lvalue_zone in
let vars = List.filter (Fun.negate (Variable.equal variable)) vars in
let state = List.fold_left State.remove state vars in
--
GitLab