From 668834f24ed96ce0ac0d0ddec53af49a63b9ebe6 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 9 Feb 2024 09:31:33 +0100
Subject: [PATCH] Use new Current_loc API in scope/from/loop_analysis
---
src/plugins/from/from_compute.ml | 14 +++++---------
src/plugins/loop_analysis/loop_analysis.ml | 3 ++-
src/plugins/scope/datascope.ml | 3 ++-
3 files changed, 9 insertions(+), 11 deletions(-)
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 32bde5c8b84..fddf07d1882 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -200,15 +200,11 @@ struct
is redundant with the work done by Value -- hence the use of [\nothing].*)
let bind_locals m b =
let aux_local acc vi =
- Current_loc.set vi.vdecl;
(* Consider that local are initialized to a constant value *)
- From_memory.bind_var vi Eva.Deps.bottom acc
+ Current_loc.with_loc vi.vdecl
+ (From_memory.bind_var vi Eva.Deps.bottom) acc
in
- let loc = Current_loc.get () in
-
- let r = List.fold_left aux_local m b.blocals in
- Current_loc.set loc;
- r
+ List.fold_left aux_local m b.blocals
let unbind_locals m b =
let aux_local acc vi =
@@ -631,7 +627,8 @@ struct
compute_using_prototype_for_state state kf assigns
let compute_and_return kf =
- let call_site_loc = Current_loc.get () in
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = Current_loc.get () in
From_parameters.feedback
"Computing for function %a%s"
Kernel_function.pretty kf
@@ -651,7 +648,6 @@ struct
From_parameters.feedback
"Done for function %a" Kernel_function.pretty kf;
Async.yield ();
- Current_loc.set call_site_loc;
result
let compute kf =
diff --git a/src/plugins/loop_analysis/loop_analysis.ml b/src/plugins/loop_analysis/loop_analysis.ml
index b6d09702f51..90481b13789 100644
--- a/src/plugins/loop_analysis/loop_analysis.ml
+++ b/src/plugins/loop_analysis/loop_analysis.ml
@@ -361,7 +361,8 @@ module Store(* (B:sig *)
end
let mu (f:(t -> t)) (value,conds,stmt) =
- Current_loc.set (Cil_datatype.Stmt.loc stmt);
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = Cil_datatype.Stmt.loc stmt in
let (result,final_conds,_) = f (init stmt) in
(* Induction variables is a map from each Varinfo to its increment. *)
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index 4c0f8787756..6cc50602a3d 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -126,10 +126,11 @@ let register_modified_zones lmap stmt =
* @raise Kernel_function.No_Definition if [kf] has no definition
*)
let compute kf =
+ let open Current_loc.Operators in
R.debug ~level:1 "computing for function %a" Kernel_function.pretty kf;
let f = Kernel_function.get_definition kf in
let do_stmt lmap s =
- Current_loc.set (Cil_datatype.Stmt.loc s);
+ let<> UpdatedCurrentLoc = Cil_datatype.Stmt.loc s in
if Eva.Results.is_reachable s
then register_modified_zones lmap s
else lmap
--
GitLab