From 3c4a12ee3fd95535111ce6f75169ca99d89c0c62 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 21 Feb 2020 09:01:42 +0100
Subject: [PATCH] [Eva] In abstract domains, removes [introduce_globals] and
changes [enter_scope].
---
src/plugins/value/domains/abstract_domain.mli | 30 +++++++-----
.../value/domains/apron/apron_domain.ml | 18 ++-----
.../value/domains/cvalue/cvalue_domain.ml | 49 ++++++++++---------
src/plugins/value/domains/domain_builder.ml | 4 +-
src/plugins/value/domains/domain_lift.ml | 2 -
src/plugins/value/domains/domain_product.ml | 6 +--
.../value/domains/equality/equality_domain.ml | 3 +-
.../value/domains/gauges/gauges_domain.ml | 3 +-
src/plugins/value/domains/inout_domain.ml | 3 +-
src/plugins/value/domains/octagons.ml | 3 +-
src/plugins/value/domains/offsm_domain.ml | 3 +-
src/plugins/value/domains/printer_domain.ml | 6 +--
src/plugins/value/domains/simple_memory.ml | 3 +-
src/plugins/value/domains/simpler_domains.mli | 6 +--
src/plugins/value/domains/symbolic_locs.ml | 3 +-
src/plugins/value/domains/traces_domain.ml | 22 +++++----
src/plugins/value/domains/unit_domain.ml | 1 -
src/plugins/value/engine/initialization.ml | 8 +--
src/plugins/value/engine/iterator.ml | 9 ++--
.../value/engine/transfer_specification.ml | 3 +-
src/plugins/value/engine/transfer_stmt.ml | 3 +-
21 files changed, 89 insertions(+), 99 deletions(-)
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 8a05da16558..2de5aebaf49 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -272,6 +272,11 @@ type 'state logic_environment = {
result: varinfo option;
}
+type variable_kind =
+ | Global
+ | Formal of kernel_function
+ | Local of kernel_function
+
(** Value for the initialization of variables. Can be either zero or top. *)
type init_value = Zero | Top
@@ -374,12 +379,20 @@ module type S = sig
(** {3 Miscellaneous } *)
(** Scoping: abstract transformers for entering and exiting blocks.
- [kf] is the englobing function, and the variables of the list [vars]
- should be added or removed from the abstract state here.
- Note that the formals of a function enter the scope through the transfer
- function {!Transfer.start_call}, but leave it through a
- call to {!leave_scope}. *)
- val enter_scope: kernel_function -> varinfo list -> t -> t
+ The variables should be added or removed from the abstract state here.
+ Note that the formals of a function called enter the scope through the
+ transfer function {!start_call}, but leave it through a call to
+ {!leave_scope}. *)
+
+ (** Introduces a list of variables in the state. At this point, the variables
+ are uninitialized. Globals and formals of the 'main' will be initialized
+ by {!initialize_variable} and {!initialize_variable_using_type}. Local
+ variables remain uninitialized until an assignment through {!assign}.
+ The formal parameters of a call enter the scope through {!start_call}. *)
+ val enter_scope: variable_kind -> varinfo list -> t -> t
+
+ (** Removes a list of local and formal variables from the state.
+ The first argument is the englobing function. *)
val leave_scope: kernel_function -> varinfo list -> t -> t
val enter_loop: stmt -> state -> state
@@ -391,11 +404,6 @@ module type S = sig
(** The initial state with which the analysis start. *)
val empty: unit -> t
- (** Introduces the list of global variables in the state. At this point,
- these variables are uninitialized: they will be initialized through the
- two functions below.*)
- val introduce_globals: varinfo list -> t -> t
-
(** [initialize_variable lval loc ~initialized init_value state] initializes
the value of the location [loc] of lvalue [lval] in [state] with:
– bits 0 if init_value = Zero;
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index 09ecaf05ded..72ce9a088e3 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -679,24 +679,12 @@ module Make (Man : Input) = struct
let empty () = top
- let introduce_globals vars state = enter_scope vars state
-
- let enter_scope _kf vars state = enter_scope vars state
+ let enter_scope _kind vars state = enter_scope vars state
let initialize_variable _lval _loc ~initialized:_ _init_value state = state
- let initialize_variable_using_type _kind varinfo state =
- try
- let var = translate_varinfo varinfo in
- let env = Abstract1.env state in
- if Environment.mem_var env var
- then state
- else
- let env = Environment.add env [|var|] [||] in
- let state = Abstract1.change_environment man state env false in
- constraint_to_typ env state [(var, varinfo)]
- with
- | Out_of_Scope _ -> state
+ (* TODO: use constraint_to_type? *)
+ let initialize_variable_using_type _kind _varinfo state = state
let relate _ _ _ = Base.SetLattice.top
let filter _ _ _ state = state
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 13142d74dcb..3ff88aca356 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -322,15 +322,6 @@ module State = struct
(* Initialization *)
(* ------------------------------------------------------------------------ *)
- let introduce_globals vars (state, clob) =
- let introduce state varinfo =
- let base = Base.of_varinfo varinfo in
- let loc = Locations.loc_of_base base in
- let value = Cvalue.V_Or_Uninitialized.uninitialized in
- Model.add_indeterminate_binding ~exact:true state loc value
- in
- List.fold_left introduce state vars, clob
-
let initialize_variable _lval loc ~initialized init_value (state, clob) =
let value = match init_value with
| Abstract_domain.Top -> Cvalue.V.top_int
@@ -383,21 +374,33 @@ module State = struct
(* Misc *)
(* ------------------------------------------------------------------------ *)
- let enter_scope _kf vars (state, clob) =
- let bind_local state vi =
- let b = Base.of_varinfo vi in
- let offsm =
- if Value_parameters.InitializedLocals.get () then
- let v = Cvalue.(V_Or_Uninitialized.initialized V.top_int) in
- match Cvalue.V_Offsetmap.size_from_validity (Base.validity b) with
- | `Bottom -> assert false
- | `Value size -> Cvalue.V_Offsetmap.create_isotropic ~size v
- else
- Bottom.non_bottom (Cvalue.Default_offsetmap.default_offsetmap b)
- in
- Model.add_base b offsm state
+ let bind_local state vi =
+ let b = Base.of_varinfo vi in
+ let offsm =
+ if Value_parameters.InitializedLocals.get () then
+ let v = Cvalue.(V_Or_Uninitialized.initialized V.top_int) in
+ match Cvalue.V_Offsetmap.size_from_validity (Base.validity b) with
+ | `Bottom -> assert false
+ | `Value size -> Cvalue.V_Offsetmap.create_isotropic ~size v
+ else
+ Bottom.non_bottom (Cvalue.Default_offsetmap.default_offsetmap b)
+ in
+ Model.add_base b offsm state
+
+ let bind_global state varinfo =
+ let base = Base.of_varinfo varinfo in
+ let loc = Locations.loc_of_base base in
+ let value = Cvalue.V_Or_Uninitialized.uninitialized in
+ Model.add_indeterminate_binding ~exact:true state loc value
+
+ let enter_scope kind vars (state, clob) =
+ let bind =
+ match kind with
+ | Abstract_domain.Local _kf -> bind_local
+ | Abstract_domain.Formal _kf -> bind_local
+ | Abstract_domain.Global -> bind_global
in
- List.fold_left bind_local state vars, clob
+ List.fold_left bind state vars, clob
let leave_scope kf vars (state, clob) =
let state = Model.remove_variables vars state in
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index ae604a6b2b0..ebeab1fb6a2 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -73,7 +73,7 @@ module Make_Minimal
let extract_expr _oracle _state _expr = top_answer
let extract_lval _oracle _state _lval _typ _location = top_answer
let backward_location _state _lval _typ location value = `Value (location, value)
- let reduce_further _sttae _expr _value = []
+ let reduce_further _state _expr _value = []
let update _valuation state = `Value state
@@ -100,7 +100,6 @@ module Make_Minimal
let initialize_variable_using_type _kind varinfo state =
let lval = Cil.var varinfo in
- let state = introduce_globals [varinfo] state in
Domain.initialize_variable lval ~initialized:true Abstract_domain.Top state
let logic_assign _assigns _location ~pre:_ _state = top
@@ -235,7 +234,6 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
let initialize_variable_using_type _kind varinfo state =
let lval = Cil.var varinfo in
- let state = introduce_globals [varinfo] state in
Domain.initialize_variable lval ~initialized:true Abstract_domain.Top state
let logic_assign _assigns _location ~pre:_ _state = top
diff --git a/src/plugins/value/domains/domain_lift.ml b/src/plugins/value/domains/domain_lift.ml
index 4aff7889345..8d264722a10 100644
--- a/src/plugins/value/domains/domain_lift.ml
+++ b/src/plugins/value/domains/domain_lift.ml
@@ -137,11 +137,9 @@ module Make
let leave_loop = Domain.leave_loop
let empty = Domain.empty
- let introduce_globals = Domain.introduce_globals
let initialize_variable lval loc ~initialized init_value state =
let loc = Convert.restrict_loc loc in
Domain.initialize_variable lval loc ~initialized init_value state
-
let initialize_variable_using_type = Domain.initialize_variable_using_type
let relate = Domain.relate
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index 5f9d14b4397..5dd265a91b8 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -256,8 +256,8 @@ module Make
Right.reduce_by_predicate right_env right pred positive >>-: fun right ->
left, right
- let enter_scope kf vars (left, right) =
- Left.enter_scope kf vars left, Right.enter_scope kf vars right
+ let enter_scope kind vars (left, right) =
+ Left.enter_scope kind vars left, Right.enter_scope kind vars right
let leave_scope kf vars (left, right) =
Left.leave_scope kf vars left, Right.leave_scope kf vars right
@@ -269,8 +269,6 @@ module Make
Left.leave_loop stmt left, Right.leave_loop stmt right
let empty () = Left.empty (), Right.empty ()
- let introduce_globals vars (left, right) =
- Left.introduce_globals vars left, Right.introduce_globals vars right
let initialize_variable lval loc ~initialized init_value (left, right) =
Left.initialize_variable lval loc ~initialized init_value left,
Right.initialize_variable lval loc ~initialized init_value right
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 9407df3145a..c6d87d30f88 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -511,7 +511,7 @@ module Make
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ state _ _ = `Value state
- let enter_scope _kf _vars state = state
+ let enter_scope _kind _vars state = state
let leave_scope _kf vars state = unscope state vars
let enter_loop _ state = state
@@ -519,7 +519,6 @@ module Make
let leave_loop _ state = state
let empty () = empty
- let introduce_globals _vars state = state
let initialize_variable _ _ ~initialized:_ _ state = state
let initialize_variable_using_type _ _ state = state
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 5c892c9e225..240fedb691b 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1141,7 +1141,7 @@ module D_Impl : Abstract_domain.S
let pretty = G.pretty
- let enter_scope _kf _vars state =
+ let enter_scope _kind _vars state =
state (* default is Top, nothing to do *)
let remove_variables vars (state:state) =
@@ -1292,7 +1292,6 @@ module D_Impl : Abstract_domain.S
let reuse _kf _bases ~current_input:_ ~previous_output = previous_output
(* Initial state *)
- let introduce_globals _ state = state
let initialize_variable_using_type _ _ state = state
let initialize_variable _ _ ~initialized:_ _ state = state
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index b34535306a3..000941e666b 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -223,7 +223,7 @@ module Internal
let name = "inout"
let log_category = Value_parameters.register_category "d-inout"
- let enter_scope _kf _vars state = state
+ let enter_scope _kind _vars state = state
let leave_scope _kf vars state = Transfer.remove_variables vars state
let to_z valuation lv =
@@ -257,7 +257,6 @@ module Internal
(* Initial state. Initializers are singletons, so we store nothing. *)
let empty () = LatticeInout.empty
- let introduce_globals _vars state = state
let initialize_variable _ _ ~initialized:_ _ state = state
let initialize_variable_using_type _ _ state = state
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index fae7d982ebc..4249c66e0ef 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -1244,7 +1244,7 @@ module Domain = struct
let evaluate_predicate _env _state _pred = Alarmset.Unknown
let reduce_by_predicate _env state _pred _positive = `Value state
- let enter_scope _kf _varinfos state = state
+ let enter_scope _kind _varinfos state = state
let leave_scope _kf varinfos state =
let state = List.fold_left State.remove state varinfos in
check "leave_scope" state
@@ -1253,7 +1253,6 @@ module Domain = struct
let incr_loop_counter _stmt state = state
let leave_loop _stmt state = state
- let introduce_globals _varinfos state = state
let initialize_variable _lval _location ~initialized:_ _value state = state
let initialize_variable_using_type _kind _varinfo state = state
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 2809ade3ffa..c02f00d3972 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -109,7 +109,7 @@ module Internal : Domain_builder.InputDomain
let empty _ = Memory.empty_map
- let enter_scope _kf _vars state = state (* default is Top, nothing to do *)
+ let enter_scope _kind _vars state = state (* default is Top, nothing to do *)
let leave_scope _kf vars state =
Memory.remove_variables vars state
@@ -212,7 +212,6 @@ module Internal : Domain_builder.InputDomain
state
(* Initial state *)
- let introduce_globals _ state = state
let initialize_variable_using_type _ _ state = state
let initialize_variable _ _ ~initialized:_ _ state = state
diff --git a/src/plugins/value/domains/printer_domain.ml b/src/plugins/value/domains/printer_domain.ml
index 6e77dfe64e7..84291ad8bce 100644
--- a/src/plugins/value/domains/printer_domain.ml
+++ b/src/plugins/value/domains/printer_domain.ml
@@ -110,17 +110,13 @@ module Simple : Simpler_domains.Simple_Cvalue = struct
feedback "empty";
()
- let introduce_globals vi_list state =
- feedback "introduce_globals %a" pp_vi_list vi_list;
- state
-
let initialize_variable lval ~initialized:_ init state =
feedback "initialize_variable %a with %a"
Printer.pp_lval lval
pp_init_val init;
state
- let enter_scope _kf vi_list state =
+ let enter_scope _kind vi_list state =
feedback "enter_scope %a" pp_vi_list vi_list;
state
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 97eed460437..fe8be4136e0 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -293,7 +293,7 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
end
| _ -> ()
- let enter_scope _kf _vars state = state
+ let enter_scope _kind _vars state = state
let leave_scope _kf vars state = remove_variables vars state
let enter_loop _ state = state
@@ -305,7 +305,6 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
let reduce_by_predicate _ state _ _ = `Value state
let empty () = top
- let introduce_globals _varinfos state = state
let initialize_variable _lval _location ~initialized:_ _value state = state
let initialize_variable_using_type _kind _varinfo state = state
diff --git a/src/plugins/value/domains/simpler_domains.mli b/src/plugins/value/domains/simpler_domains.mli
index 2b4d654bdde..c8aa69e2c58 100644
--- a/src/plugins/value/domains/simpler_domains.mli
+++ b/src/plugins/value/domains/simpler_domains.mli
@@ -70,11 +70,10 @@ module type Minimal = sig
(** Initialization of variables. *)
val empty: unit -> t
- val introduce_globals: varinfo list -> t -> t
val initialize_variable:
lval -> initialized:bool -> Abstract_domain.init_value -> t -> t
- val enter_scope: kernel_function -> varinfo list -> t -> t
+ val enter_scope: Abstract_domain.variable_kind -> varinfo list -> t -> t
val leave_scope: kernel_function -> varinfo list -> t -> t
(** Pretty printers. *)
@@ -138,11 +137,10 @@ module type Simple_Cvalue = sig
(** Initialization of variables. *)
val empty: unit -> t
- val introduce_globals: varinfo list -> t -> t
val initialize_variable:
lval -> initialized:bool -> Abstract_domain.init_value -> t -> t
- val enter_scope: kernel_function -> varinfo list -> t -> t
+ val enter_scope: Abstract_domain.variable_kind -> varinfo list -> t -> t
val leave_scope: kernel_function -> varinfo list -> t -> t
(** Pretty printer. *)
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index f325e2a7148..98a56ef209d 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -478,7 +478,7 @@ module Internal : Domain_builder.InputDomain
let empty _ = Memory.empty_map
- let enter_scope _kf _vars state = state
+ let enter_scope _kind _vars state = state
let leave_scope _kf vars state =
(* removed variables revert implicitly to Top *)
Memory.remove_variables vars state
@@ -627,7 +627,6 @@ module Internal : Domain_builder.InputDomain
keys state
(* Initial state. Initializers are singletons, so we store nothing. *)
- let introduce_globals _ state = state
let initialize_variable_using_type _ _ state = state
let initialize_variable _ _ ~initialized:_ _ state = state
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 771c2220a59..69dde95e126 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -914,16 +914,9 @@ module Internal = struct
let reuse _kf _bases ~current_input:_ ~previous_output:state = state
let empty () = Traces.empty
- let introduce_globals vars state =
- {state with globals = vars @ state.globals}
let initialize_variable lv _ ~initialized:_ _ state =
Traces.add_trans state (Msg(Format.asprintf "initialize variable: %a" Printer.pp_lval lv ))
let initialize_variable_using_type init_kind varinfo state =
- let state =
- match init_kind with
- | Abstract_domain.Main_Formal -> {state with main_formals = varinfo::state.main_formals}
- | _ -> state
- in
let msg = Format.asprintf "initialize@ variable@ using@ type@ %a@ %a"
(fun fmt init_kind ->
match init_kind with
@@ -1000,8 +993,19 @@ module Internal = struct
Traces.add_trans state (Msg "leave_loop")
- let enter_scope kf vars state = Traces.add_trans state (EnterScope (kf, vars))
- let leave_scope kf vars state = Traces.add_trans state (LeaveScope (kf, vars))
+ let enter_scope kind vars state =
+ match kind with
+ | Abstract_domain.Global ->
+ { state with globals = vars @ state.globals }
+ | Abstract_domain.Formal kf ->
+ if Kernel_function.equal kf (fst (Globals.entry_point ()))
+ then { state with main_formals = vars @ state.main_formals }
+ else state
+ | Abstract_domain.Local kf ->
+ Traces.add_trans state (EnterScope (kf, vars))
+
+ let leave_scope kf vars state =
+ Traces.add_trans state (LeaveScope (kf, vars))
let reduce_further _state _expr _value = [] (*Nothing intelligent to suggest*)
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index 8fd5df76754..cd989453aed 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -79,7 +79,6 @@ module Make
let leave_loop _ _ = ()
let empty () = ()
- let introduce_globals _ () = ()
let initialize_variable _ _ ~initialized:_ _ _ = ()
let initialize_variable_using_type _ _ _ = ()
diff --git a/src/plugins/value/engine/initialization.ml b/src/plugins/value/engine/initialization.ml
index fd124a687b6..7d06a16962e 100644
--- a/src/plugins/value/engine/initialization.ml
+++ b/src/plugins/value/engine/initialization.ml
@@ -264,8 +264,10 @@ module Make
Value_parameters.abort "Entry point %a has arguments"
Kernel_function.pretty kf
else
- let kind = Abstract_domain.Main_Formal in
- List.fold_right (Domain.initialize_variable_using_type kind) l state
+ let var_kind = Abstract_domain.Formal kf in
+ let state = Domain.enter_scope var_kind l state in
+ let init_kind = Abstract_domain.Main_Formal in
+ List.fold_right (Domain.initialize_variable_using_type init_kind) l state
(* Use the values supplied in [actuals] for the formals of [kf], and
bind them in [state] *)
@@ -305,7 +307,7 @@ module Make
let initialize_global_variable ~lib_entry vi init state =
Cil.CurrentLoc.set vi.vdecl;
- let state = Domain.introduce_globals [vi] state in
+ let state = Domain.enter_scope Abstract_domain.Global [vi] state in
if vi.vsource then
let initialize =
if lib_entry || (vi.vstorage = Extern)
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index cc122f92ae9..def379b956f 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -281,18 +281,20 @@ module Make_Dataflow
let transfer_instr (stmt : stmt) (instr : instr) : transfer_function =
match instr with
| Local_init (vi, AssignInit exp, _loc) ->
+ let kind = Abstract_domain.Local kf in
let transfer state =
- let state = Domain.enter_scope kf [vi] state in
+ let state = Domain.enter_scope kind [vi] state in
Init.initialize_local_variable stmt vi exp state
in
lift' transfer
| Local_init (vi, ConsInit (f, args, k), loc) ->
+ let kind = Abstract_domain.Local kf in
let as_func dest callee args _loc state =
(* This variable enters the scope too early, as it should
be introduced after the call to [f] but before the assignment
to [v]. This is currently not possible, at least without
splitting Transfer.call in two. *)
- let state = Domain.enter_scope kf [vi] state in
+ let state = Domain.enter_scope kind [vi] state in
transfer_call stmt dest callee args state
in
Cil.treat_constructor_as_func as_func vi f args k loc
@@ -335,7 +337,8 @@ module Make_Dataflow
let return_lval = Var vi_ret, NoOffset in
let kstmt = Kstmt stmt in
fun state ->
- let state = Domain.enter_scope kf [vi_ret] state in
+ let kind = Abstract_domain.Local kf in
+ let state = Domain.enter_scope kind [vi_ret] state in
let state' = Transfer.assign state kstmt return_lval return_exp in
Bottom.to_list state'
in
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index b3be9e6f908..2d62190cc61 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -546,7 +546,8 @@ module Make
| Some retres_vi ->
(* Notify the user about missing assigns \result. *)
if warn then warn_on_missing_result_assigns kinstr call.kf spec;
- let state = Domain.enter_scope call.kf [retres_vi] state in
+ let kind = Abstract_domain.Local call.kf in
+ let state = Domain.enter_scope kind [retres_vi] state in
let init_kind = Abstract_domain.Spec_Return call.kf in
Domain.initialize_variable_using_type init_kind retres_vi state
in
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index d4ccb75c422..3e770b1c5ba 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -846,7 +846,8 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Makes the local variables [variables] enter the scope in [state].
Also initializes volatile variable to top. *)
let enter_scope kf variables state =
- let state = Domain.enter_scope kf variables state in
+ let kind = Abstract_domain.Local kf in
+ let state = Domain.enter_scope kind variables state in
let is_volatile varinfo =
Cil.typeHasQualifier "volatile" varinfo.vtype
in
--
GitLab