diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 469c3aed3c67d646755540143018f65cd1bdd9bf..3f7b06b545ff683e9835a9654c8312cc36222e5f 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -166,64 +166,7 @@ module Value = struct
type state = Cvalue.Model.t
type t = Cvalue.V.t
- (* This function is responsible for clearing completely Value's state
- when the user-supplied initial state or main arguments are changed.
- It is set deep inside Value for technical reasons *)
- let initial_state_changed = mk_fun "Value.initial_state_changed"
-
- (* Arguments of the root function of the value analysis *)
- module ListArgs = Datatype.List(Cvalue.V)
- module FunArgs =
- State_builder.Option_ref
- (ListArgs)
- (struct
- let name = "Db.Value.fun_args"
- let dependencies =
- [ Ast.self; Kernel.LibEntry.self; Kernel.MainFunction.self]
- end)
- let () = Ast.add_monotonic_state FunArgs.self
-
-
- exception Incorrect_number_of_arguments
-
- let fun_get_args () = FunArgs.get_option ()
-
- let fun_set_args l =
- if not (Option.equal ListArgs.equal (Some l) (FunArgs.get_option ())) then
- (!initial_state_changed (); FunArgs.set l)
-
- let fun_use_default_args () =
- if FunArgs.get_option () <> None then
- (!initial_state_changed (); FunArgs.clear ())
-
- (* Initial memory state of the value analysis *)
- module VGlobals =
- State_builder.Option_ref
- (Cvalue.Model)
- (struct
- let name = "Db.Value.Vglobals"
- let dependencies = [Ast.self]
- end)
-
- let globals_set_initial_state state =
- if not (Option.equal Cvalue.Model.equal
- (Some state)
- (VGlobals.get_option ()))
- then begin
- !initial_state_changed ();
- VGlobals.set state
- end
-
-
- let globals_use_default_initial_state () =
- if VGlobals.get_option () <> None then
- (!initial_state_changed (); VGlobals.clear ())
-
- let globals_state () = VGlobals.get_option ()
-
- let globals_use_supplied_state () = not (VGlobals.get_option () = None)
-
- let dependencies = [ FunArgs.self; VGlobals.self ]
+ let dependencies = [ ]
let proxy = State_builder.Proxy.(create "eva_db" Forward dependencies)
let self = State_builder.Proxy.get proxy
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 9344f5d1c2421c7bb61aad31f5bb8a84ddcae841..037888db0e7338f80b980eee05ce439b9b8efa9c 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -123,58 +123,6 @@ module Value : sig
specified for the entry point using {!Db.Value.fun_set_args}, and
an incorrect number of them is given.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
-
-
- (** {4 Arguments of the main function} *)
-
- (** The functions below are related to the arguments that are passed to the
- function that is analysed by the value analysis. Specific arguments
- are set by [fun_set_args]. Arguments reset to default values when
- [fun_use_default_args] is called, when the ast is changed, or
- if the options [-libentry] or [-main] are changed. *)
-
- (** Specify the arguments to use. *)
- val fun_set_args : t list -> unit
-
- val fun_use_default_args : unit -> unit
-
- (** For this function, the result [None] means that
- default values are used for the arguments. *)
- val fun_get_args : unit -> t list option
-
- exception Incorrect_number_of_arguments
- (** Raised by [Db.Compute] when the arguments set by [fun_set_args]
- are not coherent with the prototype of the function (if there are
- too few or too many of them) *)
-
-
- (** {4 Initial state of the analysis} *)
-
- (** The functions below are related to the value of the global variables
- when the value analysis is started. If [globals_set_initial_state] has not
- been called, the given state is used. A default state (which depends on
- the option [-libentry]) is used when [globals_use_default_initial_state]
- is called, or when the ast changes. *)
-
- (** Specify the initial state to use. *)
- val globals_set_initial_state : state -> unit
-
- val globals_use_default_initial_state : unit -> unit
-
- (** 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
- analysis has been supplied by the user (through
- [globals_set_initial_state]), or [false] if it is automatically
- computed by the value analysis *)
- val globals_use_supplied_state : unit -> bool
-
- (**/**)
- (** {3 Internal use only} *)
-
- val initial_state_changed: (unit -> unit) ref
end
[@@alert db_deprecated
"Db.Value is deprecated and will be removed in a future version \
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index f0e9343182ce137b504a561328d583f472725e88..c8c32af8d90dba5a9c34499454eb96b0caba795f 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -42,9 +42,6 @@ module Analysis: sig
(** Computes the Eva analysis, if not already computed, using the entry point
of the current project. You may set it with {!Globals.set_entry_point}.
@raise Globals.No_such_entry_point if the entry point is incorrect
- @raise Db.Value.Incorrect_number_of_arguments if some arguments are
- specified for the entry point using {!Db.Value.fun_set_args}, and
- an incorrect number of them is given.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val is_computed : unit -> bool
@@ -803,6 +800,26 @@ module Eva_results: sig
(** Internal temporary API: please do not use it, as it should be removed in a
future version. *)
+ (** {2 Initial cvalue state} *)
+
+ (** Specifies the initial cvalue state to use. *)
+ val set_initial_state: Cvalue.Model.t -> unit
+
+ (** Ignores previous calls to [set_initial_state] above, and uses the default
+ initial state instead. *)
+ val use_default_initial_state: unit -> unit
+
+ (** Specifies the values of the main function arguments. Beware that the
+ analysis fails if the number of given values is different from the number
+ of arguments of the entry point of the analysis. *)
+ val set_main_args: Cvalue.V.t list -> unit
+
+ (** Ignores previous calls to [set_main_args] above, and uses the default
+ main argument values instead. *)
+ val use_default_main_args: unit -> unit
+
+ (** {2 Results} *)
+
type results
val get_results: unit -> results
diff --git a/src/plugins/eva/engine/analysis.mli b/src/plugins/eva/engine/analysis.mli
index fe482f514af1c500e3757d6505f5dc40adc3c5f7..fe1c8b9b55620b6a4fd3e3c6b762b6da4ecacf13 100644
--- a/src/plugins/eva/engine/analysis.mli
+++ b/src/plugins/eva/engine/analysis.mli
@@ -82,9 +82,6 @@ val compute : unit -> unit
(** Computes the Eva analysis, if not already computed, using the entry point
of the current project. You may set it with {!Globals.set_entry_point}.
@raise Globals.No_such_entry_point if the entry point is incorrect
- @raise Db.Value.Incorrect_number_of_arguments if some arguments are
- specified for the entry point using {!Db.Value.fun_set_args}, and
- an incorrect number of them is given.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val is_computed : unit -> bool
diff --git a/src/plugins/eva/engine/initialization.ml b/src/plugins/eva/engine/initialization.ml
index 572cbf09e68f68d596b6f7faf98bd48d29ba6b32..7c8a63d15d27f4c32b2fa410cddd9d688cab5c23 100644
--- a/src/plugins/eva/engine/initialization.ml
+++ b/src/plugins/eva/engine/initialization.ml
@@ -273,12 +273,15 @@ module Make
bind them in [state] *)
let add_supplied_main_formals kf actuals state =
match get_cvalue with
- | None -> Self.abort "Function Db.Value.fun_set_args cannot be \
+ | None -> Self.abort "API function [set_main_args] cannot be \
used without the Cvalue domain"
| Some get_cvalue ->
let formals = Kernel_function.get_formals kf in
if (List.length formals) <> List.length actuals then
- raise Db.Value.Incorrect_number_of_arguments;
+ Self.abort
+ "Incorrect number of arguments for the main function %a \
+ provided via the API function [set_main_args]"
+ Kernel_function.pretty kf;
let cvalue_state = get_cvalue state in
let add_actual state actual formal =
let actual = Eval_op.offsetmap_of_v ~typ:formal.vtype actual in
@@ -291,7 +294,7 @@ module Make
set_domain (cvalue_state, Locals_scoping.bottom ()) state
let add_main_formals kf state =
- match Db.Value.fun_get_args () with
+ match Eva_results.get_main_args () with
| None -> compute_main_formals kf state
| Some actuals -> add_supplied_main_formals kf actuals state
@@ -384,7 +387,7 @@ module Make
let initial_state_with_formals ~lib_entry kf =
let init_state =
- match Db.Value.globals_state () with
+ match Eva_results.get_initial_state () with
| Some state ->
Self.feedback "Initial state supplied by user";
supplied_state state
diff --git a/src/plugins/eva/parameters.ml b/src/plugins/eva/parameters.ml
index dca2f98df5726fbd57b4aacb43f2e598e21ace42..6bd34e41303c915de0220d07de608ce1c0222721 100644
--- a/src/plugins/eva/parameters.ml
+++ b/src/plugins/eva/parameters.ml
@@ -1131,23 +1131,20 @@ let () = StopAtNthAlarm.set_range ~min:0 ~max:max_int
(* -------------------------------------------------------------------------- *)
let () = Parameter_customize.is_invisible ()
-module InitialStateChanged =
+module CorrectnessChanged =
Int (struct
let option_name = "-eva-new-initial-state"
let default = 0
let arg_name = "n"
let help = ""
end)
-(* Changing the user-supplied initial state (or the arguments of main) through
- the API of Db.Value does reset the state of Value, but *not* the property
- statuses that Value has positioned. Currently, statuses can only depend
- on a command-line parameter. We use the dummy one above to force a reset
- when needed. *)
-let () =
- add_correctness_dep InitialStateChanged.parameter;
- Db.Value.initial_state_changed :=
- (fun () -> InitialStateChanged.set (InitialStateChanged.get () + 1))
+let () = add_correctness_dep CorrectnessChanged.parameter
+(* Changing the user-supplied initial state (or the arguments of main) through
+ the API does reset the state of Eva, but *not* the property statuses set by
+ Eva. Currently, statuses can only depend on command-line parameters.
+ We use the dummy one above to force a reset when needed. *)
+let change_correctness = CorrectnessChanged.incr
(* -------------------------------------------------------------------------- *)
(* --- Eva options --- *)
diff --git a/src/plugins/eva/parameters.mli b/src/plugins/eva/parameters.mli
index 61daa88642517dc801a2a65b73d7b82e80ce6210..d477b8af08ab8777ec7c2e534df5b8a522707a1e 100644
--- a/src/plugins/eva/parameters.mli
+++ b/src/plugins/eva/parameters.mli
@@ -148,10 +148,17 @@ module Precision: Parameter_sig.Int
-eva-precision. *)
val configure_precision: unit -> unit
-
+(** List of parameters having an impact on the correctness of the analysis. *)
val parameters_correctness: Typed_parameter.t list
+
+(** List of parameters having an impact only on the analysis precision. *)
val parameters_tuning: Typed_parameter.t list
+(** This function should be called whenever the correctness of the analysis
+ is externally changed through the Eva API, to ensure that the property
+ statuses emitted by Eva are properly reset. *)
+val change_correctness: unit -> unit
+
(** Registers available cvalue builtins for the -eva-builtin option. *)
val register_builtin: string -> unit
diff --git a/src/plugins/eva/utils/eva_results.ml b/src/plugins/eva/utils/eva_results.ml
index c3fb17411b706d2443c641eba774e10adc141a01..a36640fe33adda23fdf861e02d1bd4d36b8b948e 100644
--- a/src/plugins/eva/utils/eva_results.ml
+++ b/src/plugins/eva/utils/eva_results.ml
@@ -42,6 +42,53 @@ let is_non_terminating_instr stmt =
| [], _ -> true
| _, _ -> false
+(* {2 Global state.} *)
+
+(* Option_ref that calls [Parameters.change_correctness] when its state
+ is modified. *)
+module Correctness_option_ref (Data: Datatype.S) (Info: State_builder.Info)
+= struct
+ include State_builder.Option_ref (Data) (Info)
+
+ let set x =
+ if not (Option.equal Data.equal (Some x) (get_option ())) then
+ (Parameters.change_correctness (); set x)
+
+ let clear () =
+ if get_option () <> None then
+ (Parameters.change_correctness (); clear ())
+end
+
+(* Values of the arguments of the main function of the analysis. *)
+module ListArgs = Datatype.List (Cvalue.V)
+module MainArgs =
+ Correctness_option_ref
+ (ListArgs)
+ (struct
+ let name = "Eva.Eva_results.MainArgs"
+ let dependencies =
+ [ Ast.self; Kernel.LibEntry.self; Kernel.MainFunction.self]
+ end)
+let () = Ast.add_monotonic_state MainArgs.self
+let () = State_builder.Proxy.extend [MainArgs.self] Self.proxy
+
+let get_main_args = MainArgs.get_option
+let set_main_args = MainArgs.set
+let use_default_main_args = MainArgs.clear
+
+(* Initial cvalue state of the analysis. *)
+module VGlobals =
+ Correctness_option_ref
+ (Cvalue.Model)
+ (struct
+ let name = "Eva.Eva_results.VGlobals"
+ let dependencies = [Ast.self]
+ end)
+let () = State_builder.Proxy.extend [VGlobals.self] Self.proxy
+
+let get_initial_state = VGlobals.get_option
+let set_initial_state = VGlobals.set
+let use_default_initial_state = VGlobals.clear
(* {2 Saving and restoring state} *)
@@ -94,7 +141,7 @@ let get_results () =
Globals.Functions.iter copy_kf;
let kf_callers = Function_calls.get_results () in
let initial_state = Cvalue_results.get_global_state () in
- let initial_args = Db.Value.fun_get_args () in
+ let initial_args = get_main_args () in
let aux_statuses f_status ip =
let aux_any_status e status =
if Emitter.Usable_emitter.equal vue e.Property_status.emitter then
@@ -136,8 +183,8 @@ let set_results results =
Cvalue_results.register_global_state true results.initial_state;
(* Initial args *)
begin match results.initial_args with
- | None -> Db.Value.fun_use_default_args ()
- | Some l -> Db.Value.fun_set_args l
+ | None -> use_default_main_args ()
+ | Some l -> set_main_args l
end;
(* Pre- and post-states *)
let register_states register (tbl: stmt_by_callstack Stmt.Hashtbl.t) =
diff --git a/src/plugins/eva/utils/eva_results.mli b/src/plugins/eva/utils/eva_results.mli
index ee688e7b7d7dc4e997c3fa22aaf592d847bcf79c..38ace066ca04458f1610d340cf11c2dd4ed754f7 100644
--- a/src/plugins/eva/utils/eva_results.mli
+++ b/src/plugins/eva/utils/eva_results.mli
@@ -27,13 +27,38 @@ val is_non_terminating_instr: stmt -> bool
not always fail/loop (for function calls). Must be called *only* on
statements that are instructions. *)
-(** {2 Results} *)
+(** Returns the initial state provided by [set_initial_state] below, if any. *)
+val get_initial_state: unit -> Cvalue.Model.t option
+
+(** Returns the values of the main arguments provided by [set_main_args] below,
+ if any. *)
+val get_main_args: unit -> Cvalue.V.t list option
[@@@ api_start]
(** Internal temporary API: please do not use it, as it should be removed in a
future version. *)
+(** {2 Initial cvalue state} *)
+
+(** Specifies the initial cvalue state to use. *)
+val set_initial_state: Cvalue.Model.t -> unit
+
+(** Ignores previous calls to [set_initial_state] above, and uses the default
+ initial state instead. *)
+val use_default_initial_state: unit -> unit
+
+(** Specifies the values of the main function arguments. Beware that the
+ analysis fails if the number of given values is different from the number
+ of arguments of the entry point of the analysis. *)
+val set_main_args: Cvalue.V.t list -> unit
+
+(** Ignores previous calls to [set_main_args] above, and uses the default
+ main argument values instead. *)
+val use_default_main_args: unit -> unit
+
+(** {2 Results} *)
+
type results
val get_results: unit -> results