diff --git a/src/plugins/eva/domains/cvalue/cvalue_init.ml b/src/plugins/eva/domains/cvalue/cvalue_init.ml index d080059b3ae317762ef4a17a70a0efbe82121b62..3936eb4560c5989713c2523c02953ac78edc02b8 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 22bd7987f910cbcfe1329e133345cd7baa564025..304e8a1ff61bfef1d7522b5f1d37ed9926762d9a 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] *)