diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 80047f657589df147af4c3151a1229170642b540..9fd9ddd292908364c42cc4fe275f87e253e116c1 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -273,17 +273,16 @@ type 'state logic_environment = {
}
type variable_kind =
- | Global
- | Formal of kernel_function
- | Local of kernel_function
+ | Global (** Global variable *)
+ | Formal of kernel_function (** Formal parameter of a function. *)
+ | Local of kernel_function (** Local variable of a function. *)
+ | Return of kernel_function (** Special variable that stores the return value
+ of a call from the end of the function called
+ back to the call site. *)
(** 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
@@ -407,9 +406,13 @@ 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. TODO: move some parts of the
+ cvalue implementation of this function in the generic engine.
+ 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. *)
+ val initialize_variable_using_type: variable_kind -> varinfo -> t -> t
(** {3 Miscellaneous } *)
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 3ff88aca356602e63e132747791067cf2331ed5c..986f01689ab3125b5d530fa4cdc3827c8e31ea52 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -362,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.Return 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
@@ -396,9 +395,8 @@ module State = struct
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
+ | Abstract_domain.Global -> bind_global
+ | Abstract_domain.(Local _ | Formal _ | Return _) -> bind_local
in
List.fold_left bind state vars, clob
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 69dde95e126dbc2c67c4899a2e75a306122bcc5c..d7e947f267e1be837f8dbc8a1bb653280b3ef430 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -916,14 +916,15 @@ module Internal = struct
let empty () = Traces.empty
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 initialize_variable_using_type var_kind varinfo state =
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
+ (fun fmt var_kind ->
+ match var_kind with
+ | Abstract_domain.Local _ -> Format.pp_print_string fmt "Local"
+ | Abstract_domain.Formal _ -> Format.pp_print_string fmt "Formal"
+ | Abstract_domain.Global -> Format.pp_print_string fmt "Global"
+ | Abstract_domain.Return kf -> Format.fprintf fmt "Return(%s)" (Kernel_function.get_name kf))
+ var_kind
Varinfo.pretty varinfo
in
Traces.add_trans state (Msg msg)
@@ -1001,7 +1002,7 @@ module Internal = struct
if Kernel_function.equal kf (fst (Globals.entry_point ()))
then { state with main_formals = vars @ state.main_formals }
else state
- | Abstract_domain.Local kf ->
+ | Abstract_domain.(Local kf | Return kf) ->
Traces.add_trans state (EnterScope (kf, vars))
let leave_scope kf vars state =
diff --git a/src/plugins/value/engine/initialization.ml b/src/plugins/value/engine/initialization.ml
index 7d06a16962ed465d459ae767acfbc5df057b2bc3..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
@@ -266,8 +266,7 @@ module Make
else
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
+ 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] *)
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index def379b956f29ffdda46a6481d28c2b5da244a3b..c58cdc0e60ea54e21a34f1e4669223a39af9e1cb 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -337,7 +337,7 @@ module Make_Dataflow
let return_lval = Var vi_ret, NoOffset in
let kstmt = Kstmt stmt in
fun state ->
- let kind = Abstract_domain.Local kf in
+ let kind = Abstract_domain.Return 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'
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index 2d62190cc6146c85aae3d9ce11ccf393a88292ca..dff7f2b618dfa23d95079fb3d0a91897fccfd1ac 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -546,10 +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 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
+ let var_kind = Abstract_domain.Return 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