diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 8a05da1655898d95dbf049af9504cd5472e5206f..06dfe5a14d785e2beacf3e3c0cb524f5bca8ba6f 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -272,18 +272,23 @@ type 'state logic_environment = {
result: varinfo option;
}
+type variable_kind =
+ | Global (** Global variable. *)
+ | Formal of kernel_function (** Formal parameter of a function. *)
+ | Local of kernel_function (** Local variable of a function. *)
+ | Result of kernel_function (** Special variable storing the return value
+ of a call. Assigned at the end of the called
+ function, and used at the call site. Also
+ used to model the ACSL \result construct. *)
+
(** Value for the initialization of variables. Can be either zero or top. *)
type init_value = Zero | Top
-(* Kind of variable being initialized by initialize_variable_using_type. *)
-type init_kind =
- Main_Formal | Library_Global | Spec_Return of kernel_function
-
(** MemExec is a global cache for the complete analysis of functions.
It avoids repeating the analysis of a function in equivalent entry states.
It uses an over-approximation of the locations possibly read and written
by a function, and compare the entry states for these locations. *)
-module type Recycle = sig
+module type Reuse = sig
type t (** Type of states. *)
(** [relate kf bases state] returns the set of bases [bases] in relation with
@@ -371,31 +376,28 @@ module type S = sig
val reduce_by_predicate:
state logic_environment -> state -> predicate -> bool -> state or_bottom
- (** {3 Miscellaneous } *)
+ (** {3 Scoping and initialization } *)
(** 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 called function enter the scope through the
+ transfer function {!start_call}, and 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
- val incr_loop_counter: stmt -> state -> state
- val leave_loop: stmt -> state -> state
-
- (** Initialization *)
-
(** 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;
@@ -405,11 +407,22 @@ module type S = sig
val initialize_variable:
lval -> location -> initialized:bool -> init_value -> t -> t
- (** Initializes a variable according to its type. TODO: move some parts
- of the cvalue implementation of this function in the generic engine. *)
- val initialize_variable_using_type: init_kind -> varinfo -> t -> t
+ (** Initializes a variable according to its type.
+ The variable can be:
+ - a global variable on lib-entry mode.
+ - a formal parameter of the 'main' function.
+ - the return variable of a function specification. *)
+ (* TODO: move some parts of the cvalue implementation of this function
+ in the generic engine. *)
+ val initialize_variable_using_type: variable_kind -> varinfo -> t -> t
+
+ (** {3 Miscellaneous } *)
+
+ val enter_loop: stmt -> state -> state
+ val incr_loop_counter: stmt -> state -> state
+ val leave_loop: stmt -> state -> state
- include Recycle with type t := t
+ include Reuse with type t := t
(** Category for the messages about the domain.
Must be created through {!Value_parameters.register_category}. *)
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index 09ecaf05ded71c5ed74445d1625d74915edc7081..228a52c2079280e1e86448bd7f2236ef208ce735 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 13142d74dcbfad8306ad66a7e6189f9e81200f9f..67eab080499f68a2f4336a21b9a833b5279aab22 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
@@ -371,10 +362,9 @@ module State = struct
let initialize_variable_using_type kind varinfo (state, clob) =
match kind with
- | Abstract_domain.Main_Formal
- | Abstract_domain.Library_Global ->
+ | Abstract_domain.(Global | Formal _ | Local _) ->
Cvalue_init.initialize_var_using_type varinfo state, clob
- | Abstract_domain.Spec_Return kf ->
+ | Abstract_domain.Result kf ->
let value = Library_functions.returned_value kf in
let loc = Locations.loc_of_varinfo varinfo in
Model.add_binding ~exact:true state loc value, clob
@@ -383,21 +373,32 @@ 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.Global -> bind_global
+ | Abstract_domain.(Local _ | Formal _ | Result _) -> bind_local
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 ae604a6b2b0a9d2b111991a4b586d80df49f1115..ebeab1fb6a2a86043e77fe44a01ff9b1a27ef3cd 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 4aff78893455842c47ad75e696d3b179aaa77c1f..8d264722a108824d17a64ac725f3cecfc6bd7713 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 5f9d14b4397089916514467667cdbe4bb1ef82b4..5dd265a91b888e10bb49749433674b65cef6de10 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 9407df3145acd07c7720396fd5201a2c27309a2f..c6d87d30f888e9c09609bb91ce39875369f9c145 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 5c892c9e22580ec5d8efe251d826e6637d599269..240fedb691b190bf53e2c2cc78a9c3e61d90a4df 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 b34535306a3b0b05c5dba5bc892f52592547dac7..000941e666bddcacbdc13211447291196891a97d 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 fae7d982ebcea2eda03670255d94a9a0a03350ce..4249c66e0ef5230a97916246a43486dacd51c412 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 2809ade3ffa86d3af14817a0de035bb7d6daeee0..c02f00d3972cb678cb6eb78cd18314198a57bb99 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 6e77dfe64e77dc709f991386cd8cbc65199cc2a1..330c4cde1a0ebb451c88ff227c3fe83242046f59 100644
--- a/src/plugins/value/domains/printer_domain.ml
+++ b/src/plugins/value/domains/printer_domain.ml
@@ -110,18 +110,14 @@ 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 =
- feedback "enter_scope %a" pp_vi_list vi_list;
+ let enter_scope _kind vi_list state =
+ feedback "enter_scope %a" pp_vi_list vi_list;
state
let leave_scope _kf vi_list state =
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 97eed460437020f80b6cd893aabb6e68c3d22776..fe8be4136e0fecb4457121a826543da320027a45 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 2b4d654bdde07ef30011bb6c4a568da82dfa7c54..c8aa69e2c585df1d92dea213155ab484bda1c647 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 f325e2a714866b4ff21fee35ef0222c04ffdc98a..98a56ef209dcf9cd50a8b76b57653c4054e316b0 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 771c2220a59d89cdc052d8fbf7efdb77c9377177..a2dffc08c938b4ed4b02626373dd70448e12d5e1 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -914,24 +914,19 @@ 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
+ let initialize_variable_using_type var_kind varinfo state =
+ let kind_str =
+ match var_kind with
+ | Abstract_domain.Global -> "global"
+ | Abstract_domain.Local _ -> "local"
+ | Abstract_domain.Formal _ -> "formal"
+ | Abstract_domain.Result _ -> "result"
in
- let msg = Format.asprintf "initialize@ variable@ using@ type@ %a@ %a"
- (fun fmt init_kind ->
- match init_kind with
- | Abstract_domain.Main_Formal -> Format.pp_print_string fmt "Main_Formal"
- | Abstract_domain.Library_Global -> Format.pp_print_string fmt "Library_Global"
- | Abstract_domain.Spec_Return kf -> Format.fprintf fmt "Spec_Return(%s)" (Kernel_function.get_name kf))
- init_kind
- Varinfo.pretty varinfo
+ let msg =
+ Format.asprintf "initialize@ %s variable@ using@ type@ %a"
+ kind_str Varinfo.pretty varinfo
in
Traces.add_trans state (Msg msg)
@@ -1000,8 +995,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 | Result 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 8fd5df76754bde4450ce50ccb1758000a2f44d84..cd989453aedf3ba7cf4e3246ece6543d49445b8b 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 fd124a687b6a27f5c823130697fcad9ca2042a7a..fb70a7e9ae9ad49c3a92d717cba3d342a3052d6c 100644
--- a/src/plugins/value/engine/initialization.ml
+++ b/src/plugins/value/engine/initialization.ml
@@ -234,7 +234,7 @@ module Make
initialize_var_padding vi ~local:false ~lib_entry:true state
in
(* Then initialize non-padding bits according to the type. *)
- let kind = Abstract_domain.Library_Global in
+ let kind = Abstract_domain.Global in
Domain.initialize_variable_using_type kind vi state
in
(* If needed, initializes const fields according to the initializer
@@ -264,8 +264,9 @@ 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
+ List.fold_right (Domain.initialize_variable_using_type var_kind) l state
(* Use the values supplied in [actuals] for the formals of [kf], and
bind them in [state] *)
@@ -305,7 +306,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 cc122f92ae9f36e93fb5d47b4a370cabe8620dc2..83a22d27168133743da52eacbf4e5aa693e62158 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.Result 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/mem_exec.ml b/src/plugins/value/engine/mem_exec.ml
index 83629ab5fc926f6d2d59ee2a77e93208b3df5d6a..4cd62fcbaaddebc8ee5bf8c7151d6dd134d26991 100644
--- a/src/plugins/value/engine/mem_exec.ml
+++ b/src/plugins/value/engine/mem_exec.ml
@@ -23,7 +23,7 @@
module type Domain = sig
include Datatype.S_with_collections
- include Abstract_domain.Recycle with type t := t
+ include Abstract_domain.Reuse with type t := t
end
diff --git a/src/plugins/value/engine/mem_exec.mli b/src/plugins/value/engine/mem_exec.mli
index 0b3fc959820db051608932a33d8a7d781b2850c9..9c288436038e2680f6aee33a1b04b14acd6c7d3c 100644
--- a/src/plugins/value/engine/mem_exec.mli
+++ b/src/plugins/value/engine/mem_exec.mli
@@ -25,7 +25,7 @@ open Eval
module type Domain = sig
include Datatype.S_with_collections
- include Abstract_domain.Recycle with type t := t
+ include Abstract_domain.Reuse with type t := t
end
(** Counter that must be used each time a new call is analyzed, in order
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index b3be9e6f908aa569bd360e6f002cde811ecc29a5..331a5946cf1fbd37dd1080195da3cfa0f8961bce 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -546,9 +546,9 @@ 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 init_kind = Abstract_domain.Spec_Return call.kf in
- Domain.initialize_variable_using_type init_kind retres_vi state
+ let var_kind = Abstract_domain.Result call.kf in
+ let state = Domain.enter_scope var_kind [retres_vi] state in
+ Domain.initialize_variable_using_type var_kind retres_vi state
in
let states =
compute_specification ~warn kinstr call.kf call.return spec state
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index d4ccb75c422925589acb2ffb2d016a802e16a24a..3e770b1c5ba1796ad72fe2ce66d12fce1825fa73 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
diff --git a/tests/value/traces/oracle/test1.res.oracle b/tests/value/traces/oracle/test1.res.oracle
index 371a47f96c36e39e09c8da22b72a8cc9d95178cd..679625f40788362b3bb3910df23bb974d38a6738 100644
--- a/tests/value/traces/oracle/test1.res.oracle
+++ b/tests/value/traces/oracle/test1.res.oracle
@@ -14,11 +14,11 @@
[eva:d-traces] Trace domains:
start: 0; globals = g, entropy_source; main_formals = c;
{[ 0 -> initialize variable: entropy_source -> 1
- 1 -> initialize variable using type Library_Global
+ 1 -> initialize global variable using type
entropy_source -> 2
2 -> initialize variable: g -> 3
3 -> Assign: g = 42 -> 4
- 4 -> initialize variable using type Main_Formal
+ 4 -> initialize formal variable using type
c -> 5
5 -> EnterScope: tmp -> 6
6 -> Assign: tmp = 0 -> 7
diff --git a/tests/value/traces/oracle/test2.res.oracle b/tests/value/traces/oracle/test2.res.oracle
index c936d8bb9b5ec7356b61cb874df09a8192438bd2..65c109933939b95fb5d020721e76de0b4dc550a6 100644
--- a/tests/value/traces/oracle/test2.res.oracle
+++ b/tests/value/traces/oracle/test2.res.oracle
@@ -21,7 +21,7 @@
tmp ∈ {4; 5}
[eva:d-traces] Trace domains:
start: 0; globals = ; main_formals = c;
- {[ 0 -> initialize variable using type Main_Formal
+ {[ 0 -> initialize formal variable using type
c -> 1
1 -> EnterScope: tmp -> 2
2 -> Assign: tmp = 0 -> 3
diff --git a/tests/value/traces/oracle/test3.res.oracle b/tests/value/traces/oracle/test3.res.oracle
index d99315838e92aad39c6e71fdddf12bbbf71b6085..94615aa1fd40d461d21b8914fbc9490ccf004a56 100644
--- a/tests/value/traces/oracle/test3.res.oracle
+++ b/tests/value/traces/oracle/test3.res.oracle
@@ -14,7 +14,7 @@
[eva:d-traces] Trace domains:
start: 0; globals = g; main_formals = c;
{[ 0 -> initialize variable: g -> 1
- 1 -> initialize variable using type Main_Formal
+ 1 -> initialize formal variable using type
c -> 2
2 -> EnterScope: __retres -> 3
3 -> EnterScope: tmp -> 4
diff --git a/tests/value/traces/oracle/test4.res.oracle b/tests/value/traces/oracle/test4.res.oracle
index 62f44d1b1031d4d20500bb91b2d631300bead971..131cdfb303e054a35f2fc4f8e90c97fdbcaedb83 100644
--- a/tests/value/traces/oracle/test4.res.oracle
+++ b/tests/value/traces/oracle/test4.res.oracle
@@ -24,7 +24,7 @@
tmp ∈ [46..2147483647]
[eva:d-traces] Trace domains:
start: 0; globals = ; main_formals = c;
- {[ 0 -> initialize variable using type Main_Formal
+ {[ 0 -> initialize formal variable using type
c -> 1
1 -> EnterScope: tmp -> 2
2 -> initialize variable: tmp -> 3
diff --git a/tests/value/traces/oracle/test5.res.oracle b/tests/value/traces/oracle/test5.res.oracle
index 1f021acddb6043e4a0f2f980bb3d3fb69561792d..815b9a52bd370ee6179be96c05a8b4a23601ab60 100644
--- a/tests/value/traces/oracle/test5.res.oracle
+++ b/tests/value/traces/oracle/test5.res.oracle
@@ -107,7 +107,7 @@
tmp ∈ [--..--]
[eva:d-traces] Trace domains:
start: 0; globals = ; main_formals = c;
- {[ 0 -> initialize variable using type Main_Formal
+ {[ 0 -> initialize formal variable using type
c -> 1
1 -> EnterScope: tmp -> 2
2 -> initialize variable: tmp -> 3