[Eva] In locals_scoping, implements the substitution of local and formal variables.

src/plugins/value/domains/cvalue/locals_scoping.ml

@@ -128,6 +128,32 @@ let make_escaping_fundec fundec clob vars state =
     make_escaping ~exact:true ~escaping ~on_escaping ~within:clob.clob state
 
 
+let substitute substitution clob state =
+  (* Clean [offsm], and bind it to [base] if it is modified. *)
+  let replace_offsm base offsm state =
+    let f v = snd (Cvalue.V_Or_Uninitialized.replace_base substitution v) in
+    let offsm' = Cvalue.V_Offsetmap.map_on_values f offsm in
+    if Cvalue.V_Offsetmap.equal offsm' offsm
+    then state
+    else Cvalue.Model.add_base base offsm' state
+  in
+  (* Clean the offsetmap bound to [base] in [state] *)
+  let replace_base base state =
+    try
+      match Cvalue.Model.find_base base state with
+      | `Top | `Bottom -> state
+      | `Value offsm -> replace_offsm base offsm state
+    with Not_found -> state
+  in
+  (* Iterate on all the bases that might contain a variable to substitute *)
+  try Base.SetLattice.fold replace_base clob.clob (replace_base Base.null state)
+  with Abstract_interp.Error_Top ->
+  (* [clob] is too imprecise. Iterate on the entire memory state instead,
+     which is much slower. *)
+  match state with
+  | Cvalue.Model.Top | Cvalue.Model.Bottom -> state
+  | Cvalue.Model.Map map -> Cvalue.Model.fold replace_offsm map state
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."

src/plugins/value/domains/cvalue/locals_scoping.mli

@@ -70,6 +70,8 @@ val make_escaping_fundec:
     [fdec] is used to detect whether we are deallocating the outer scope of a
     function, in which case a different warning is emitted. *)
 
+val substitute:
+  Base.substitution -> clobbered_set -> Cvalue.Model.t -> Cvalue.Model.t
 
 (*
 Local Variables: