diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 960480c8c2213503cd308d9f11b65c155181286a..469c3aed3c67d646755540143018f65cd1bdd9bf 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -219,12 +219,7 @@ module Value = struct
if VGlobals.get_option () <> None then
(!initial_state_changed (); VGlobals.clear ())
- let initial_state_only_globals = mk_fun "Value.initial_state_only_globals"
-
- let globals_state () =
- match VGlobals.get_option () with
- | Some v -> v
- | None -> !initial_state_only_globals ()
+ let globals_state () = VGlobals.get_option ()
let globals_use_supplied_state () = not (VGlobals.get_option () = None)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index d664470b29dc0bf994ede598f40ea3c6c112e3c7..9344f5d1c2421c7bb61aad31f5bb8a84ddcae841 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -161,8 +161,8 @@ module Value : sig
val globals_use_default_initial_state : unit -> unit
- (** Initial state used by the analysis *)
- val globals_state : unit -> state
+ (** Initial state provided by [globals_set_initial_state], if any. *)
+ val globals_state : unit -> state option
(** @return [true] if the initial state for globals used by the value
@@ -174,9 +174,6 @@ module Value : sig
(**/**)
(** {3 Internal use only} *)
-
- val initial_state_only_globals : (unit -> state) ref
-
val initial_state_changed: (unit -> unit) ref
end
[@@alert db_deprecated
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index 6bbfef27ba4dc1a948398cb182431dd2c0fda689..06aa0bce44b1c7290400f61d59edf71f381e680d 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -88,7 +88,6 @@ module type Analyzer = sig
include S
val compute_from_entry_point : kernel_function -> lib_entry:bool -> unit
(* val compute_from_init_state: kernel_function -> Dom.t -> unit *)
- val initial_state: lib_entry:bool -> Dom.t or_bottom
end
@@ -181,14 +180,6 @@ let set_current_analyzer config (analyzer: (module Analyzer)) =
Analyzer_Hook.apply (module (val analyzer): S);
ref_analyzer := (config, analyzer)
-let cvalue_initial_state () =
- let module A = (val snd !ref_analyzer) in
- let module G = (Cvalue_domain.Getters (A.Dom)) in
- let _, lib_entry = Globals.entry_point () in
- G.get_cvalue_or_bottom (A.initial_state ~lib_entry)
-
-let () = Db.Value.initial_state_only_globals := cvalue_initial_state
-
(* Builds the Analyzer module corresponding to a given configuration,
and sets it as the current analyzer. *)
let make_analyzer config =
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index d46426ab057153674119cfb4d418b2a8db790894..59f8a8d9a4e6c3e74a00fbc6427d09371995da74 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -167,8 +167,6 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
include Cvalue_domain.Getters (Abstract.Dom)
- let initial_state = Init.initial_state
-
let get_cval =
match Abstract.Val.get Main_values.CVal.key with
| None -> fun _ -> assert false
diff --git a/src/plugins/eva/engine/compute_functions.mli b/src/plugins/eva/engine/compute_functions.mli
index 28f78965dbb2d54008aabe51674bbf084a49f3d8..b582766632a43768abdd5399173249071a265a5f 100644
--- a/src/plugins/eva/engine/compute_functions.mli
+++ b/src/plugins/eva/engine/compute_functions.mli
@@ -23,7 +23,6 @@
(** Value analysis of entire functions, using Eva engine. *)
open Cil_types
-open Eval
module Make (Abstract: Abstractions.S_with_evaluation)
: sig
@@ -33,6 +32,4 @@ module Make (Abstract: Abstractions.S_with_evaluation)
(** Compute a call to the main function from the given initial state. *)
val compute_from_init_state: kernel_function -> Abstract.Dom.t -> unit
-
- val initial_state: lib_entry:bool -> Abstract.Dom.t or_bottom
end
diff --git a/src/plugins/eva/engine/initialization.ml b/src/plugins/eva/engine/initialization.ml
index da1ac7627c24ad6b1b39e6b09f7803ba7d6ec3e7..572cbf09e68f68d596b6f7faf98bd48d29ba6b32 100644
--- a/src/plugins/eva/engine/initialization.ml
+++ b/src/plugins/eva/engine/initialization.ml
@@ -27,7 +27,6 @@ open Eval
module type S = sig
type state
- val initial_state : lib_entry:bool -> state or_bottom
val initial_state_with_formals :
lib_entry:bool -> kernel_function -> state or_bottom
val initialize_local_variable:
@@ -357,19 +356,13 @@ module Make
InitialState.memo (compute_global_state ~lib_entry)
(* The global cvalue state may be supplied by the user. *)
- let supplied_state () =
- let cvalue_state = Db.Value.globals_state () in
+ let supplied_state cvalue_state =
if Cvalue.Model.is_reachable cvalue_state
then
let cvalue_state = cvalue_state, Locals_scoping.bottom () in
`Value (Domain.set Cvalue_domain.State.key cvalue_state Domain.top)
else `Bottom
- let initial_state ~lib_entry =
- if Db.Value.globals_use_supplied_state ()
- then supplied_state ()
- else global_state ~lib_entry
-
let print_initial_cvalue_state state =
let cvalue_state = get_cvalue_or_bottom state in
(* Do not show variables from the frama-c libc specifications. *)
@@ -391,18 +384,16 @@ module Make
let initial_state_with_formals ~lib_entry kf =
let init_state =
- if Db.Value.globals_use_supplied_state ()
- then begin
+ match Db.Value.globals_state () with
+ | Some state ->
Self.feedback "Initial state supplied by user";
- supplied_state ()
- end
- else begin
+ supplied_state state
+ | None ->
let pp = Parameters.ValShowProgress.get () in
if pp then Self.feedback "Computing initial state";
let state = global_state ~lib_entry in
if pp then Self.feedback "Initial state computed";
state
- end
in
let b = Parameters.ResultsAll.get () in
Domain.Store.register_global_state b init_state;
diff --git a/src/plugins/eva/engine/initialization.mli b/src/plugins/eva/engine/initialization.mli
index 872206abe61796ac482a107efdd3d344668ca87b..e669a8df56c486c4751b7ac4bf798c12b02af7c2 100644
--- a/src/plugins/eva/engine/initialization.mli
+++ b/src/plugins/eva/engine/initialization.mli
@@ -28,11 +28,6 @@ open Lattice_bounds
module type S = sig
type state
- (** Compute the initial state for an analysis. The initial state is generated
- according to the options of Value governing the shape of this state.
- All global variables are bound in the resulting abstract state. *)
- val initial_state : lib_entry:bool -> state or_bottom
-
(** Compute the initial state for an analysis (as in {!initial_state}),
but also bind the formal parameters of the function given as argument. *)
val initial_state_with_formals :
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 72e58f5421a151d2c5301def1d89ad7c9cf0fb2a..0eceb70bf4872593ecfed55d2ff0353f4261d740 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -238,8 +238,10 @@ let add_pre = add_logic Logic_const.pre_label
let add_post = add_logic Logic_const.post_label
let add_old = add_logic Logic_const.old_label
(* Init is a bit special, it is constant and always added to the initial state*)
-let add_init state =
- add_logic Logic_const.init_label (Db.Value.globals_state ()) state
+let add_init states =
+ match Cvalue_results.get_global_state () with
+ | `Bottom -> states
+ | `Value state -> add_logic Logic_const.init_label state states
let add_logic_var env lv cvalue =
{ env with logic_vars = LogicVarEnv.add lv cvalue env.logic_vars }
diff --git a/src/plugins/eva/utils/eva_results.ml b/src/plugins/eva/utils/eva_results.ml
index 606158151f651cc2197e55f78b3b4b26ecfc1ca4..c3fb17411b706d2443c641eba774e10adc141a01 100644
--- a/src/plugins/eva/utils/eva_results.ml
+++ b/src/plugins/eva/utils/eva_results.ml
@@ -57,7 +57,7 @@ type results = {
after_states: stmt_by_callstack Stmt.Hashtbl.t;
kf_initial_states: stmt_by_callstack Kernel_function.Hashtbl.t;
kf_callers: Function_calls.t;
- initial_state: Cvalue.Model.t;
+ initial_state: Cvalue.Model.t Lattice_bounds.or_bottom;
initial_args: Cvalue.V.t list option;
alarms: Property_status.emitted_status AlarmsStmt.Hashtbl.t;
statuses: Property_status.emitted_status Property.Hashtbl.t
@@ -93,7 +93,7 @@ let get_results () =
in
Globals.Functions.iter copy_kf;
let kf_callers = Function_calls.get_results () in
- let initial_state = Db.Value.globals_state () in
+ let initial_state = Cvalue_results.get_global_state () in
let initial_args = Db.Value.fun_get_args () in
let aux_statuses f_status ip =
let aux_any_status e status =
@@ -133,7 +133,7 @@ let set_results results =
Project.clear ~selection ();
(* Those two functions may clear Self.state. Start by them *)
(* Initial state *)
- Db.Value.globals_set_initial_state results.initial_state;
+ Cvalue_results.register_global_state true results.initial_state;
(* Initial args *)
begin match results.initial_args with
| None -> Db.Value.fun_use_default_args ()
@@ -254,7 +254,9 @@ let merge r1 r2 =
let kf_callers = Function_calls.merge_results r1.kf_callers r2.kf_callers in
let alarms = AlarmsStmtH.merge merge_statuses r1.alarms r2.alarms in
let statuses = PropertyH.merge merge_statuses r1.statuses r2.statuses in
- let initial_state = Cvalue.Model.join r1.initial_state r2.initial_state in
+ let initial_state =
+ Lattice_bounds.Bottom.join Cvalue.Model.join r1.initial_state r2.initial_state
+ in
let initial_args =
match main, r1.initial_args, r2.initial_args with
| None, _, _ | _, None, _ | _, _, None -> None