Skip to content
Snippets Groups Projects
Commit 9e9cca2a authored by David Bühler's avatar David Bühler
Browse files

[Eva] Sets the current location in the engine, not in the cvalue domain.

parent 94f1dd54
No related branches found
No related tags found
No related merge requests found
...@@ -111,8 +111,6 @@ let reject_empty_struct b offset typ = ...@@ -111,8 +111,6 @@ let reject_empty_struct b offset typ =
(** [initialize_var_using_type varinfo state] uses the type of [varinfo] (** [initialize_var_using_type varinfo state] uses the type of [varinfo]
to create an initial value in [state]. *) to create an initial value in [state]. *)
let initialize_var_using_type varinfo 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 rec add_offsetmap depth b name_desc name typ offset_orig typ_orig state =
let typ = Cil.unrollType typ in let typ = Cil.unrollType typ in
let loc = lazy (loc_of_typoffset b typ_orig offset_orig) in let loc = lazy (loc_of_typoffset b typ_orig offset_orig) in
......
...@@ -267,7 +267,12 @@ module Make ...@@ -267,7 +267,12 @@ module Make
else else
let var_kind = Abstract_domain.Formal kf in let var_kind = Abstract_domain.Formal kf in
let state = Domain.enter_scope var_kind l state 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 (* Use the values supplied in [actuals] for the formals of [kf], and
bind them in [state] *) bind them in [state] *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment