From 9e9cca2a32b7d79e6a4e877ddecff80747ca6339 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 16 Apr 2024 14:35:33 +0200
Subject: [PATCH] [Eva] Sets the current location in the engine, not in the
cvalue domain.
---
src/plugins/eva/domains/cvalue/cvalue_init.ml | 2 --
src/plugins/eva/engine/initialization.ml | 7 ++++++-
2 files changed, 6 insertions(+), 3 deletions(-)
diff --git a/src/plugins/eva/domains/cvalue/cvalue_init.ml b/src/plugins/eva/domains/cvalue/cvalue_init.ml
index d080059b3ae..3936eb4560c 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_init.ml
@@ -111,8 +111,6 @@ let reject_empty_struct b offset typ =
(** [initialize_var_using_type varinfo state] uses the type of [varinfo]
to create an initial value in [state]. *)
let initialize_var_using_type varinfo state =
- let open Current_loc.Operators in
- let<> UpdatedCurrentLoc = varinfo.vdecl in
let rec add_offsetmap depth b name_desc name typ offset_orig typ_orig state =
let typ = Cil.unrollType typ in
let loc = lazy (loc_of_typoffset b typ_orig offset_orig) in
diff --git a/src/plugins/eva/engine/initialization.ml b/src/plugins/eva/engine/initialization.ml
index 22bd7987f91..304e8a1ff61 100644
--- a/src/plugins/eva/engine/initialization.ml
+++ b/src/plugins/eva/engine/initialization.ml
@@ -267,7 +267,12 @@ module Make
else
let var_kind = Abstract_domain.Formal kf in
let state = Domain.enter_scope var_kind l state in
- List.fold_right (Domain.initialize_variable_using_type var_kind) l state
+ let init vi state =
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = vi.vdecl in
+ Domain.initialize_variable_using_type var_kind vi state
+ in
+ List.fold_right init l state
(* Use the values supplied in [actuals] for the formals of [kf], and
bind them in [state] *)
--
GitLab