diff --git a/src/kernel_services/abstract_interp/cilE.ml b/src/kernel_services/abstract_interp/cilE.ml
deleted file mode 100644
index f650d8e3a6d6b6d390328e69bbca35ecf2b2d062..0000000000000000000000000000000000000000
--- a/src/kernel_services/abstract_interp/cilE.ml
+++ /dev/null
@@ -1,46 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* ************************************************************************* *)
-(* [JS 2011/03/11] All the below stuff manage warnings of the value analysis
- plug-in. Refactoring required. *)
-(* ************************************************************************* *)
-
-type alarm_behavior = unit -> unit
-
-let a_ignore = Extlib.nop
-
-type warn_mode = {defined_logic: alarm_behavior;
- unspecified: alarm_behavior;
- others: alarm_behavior;}
-
-let warn_none_mode =
- { defined_logic = a_ignore; unspecified = a_ignore; others = a_ignore; }
-
-
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/abstract_interp/cilE.mli b/src/kernel_services/abstract_interp/cilE.mli
deleted file mode 100644
index cb0e2d41d37de35c0dde6494b32cb8c4fe500b5c..0000000000000000000000000000000000000000
--- a/src/kernel_services/abstract_interp/cilE.mli
+++ /dev/null
@@ -1,54 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(** Value analysis alarms *)
-
-(* ************************************************************************* *)
-(* [JS 2011/03/11] All the below stuff manage warnings of the value analysis
- plug-in. Refactoring required. *)
-(* ************************************************************************* *)
-
-type alarm_behavior = unit -> unit
-
-val a_ignore: alarm_behavior
-
-type warn_mode =
- { defined_logic: alarm_behavior
- (** operations that raise an error only in the C, not in the logic *);
- unspecified: alarm_behavior (** defined but unspecified behaviors *);
- others: alarm_behavior (** all the remaining undefined behaviors *);
- }
-(** An argument of type [warn_mode] can be supplied to some of the access
- functions in {!Db.Value} (the interface to the value analysis).
- Each field of {!warn_mode} indicates the action to perform
- for each category of alarm. These fields are not completely fixed
- yet. However, you can use the value {!warn_none_mode} below
- when you have to provide an argument of type [warn_mode]. *)
-
-val warn_none_mode : warn_mode
-(** Do not emit any message. *)
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 4266f7dd1276e87ab4ebab7fa32e55b24b5ac3c3..69383faea0bdae2dd7329a0d55062024fac86df0 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -157,114 +157,6 @@ module Derefs = struct
let pretty = Locations.Zone.pretty
end
-
-(* ************************************************************************* *)
-(** {2 Values} *)
-(* ************************************************************************* *)
-
-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 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_use_supplied_state () = not (VGlobals.get_option () = None)
-
- let dependencies = [ FunArgs.self; VGlobals.self ]
- let proxy = State_builder.Proxy.(create "eva_db" Forward dependencies)
- let self = State_builder.Proxy.get proxy
- let only_self = [ self ]
-
- module Conditions_table =
- Cil_state_builder.Stmt_hashtbl
- (Datatype.Int)
- (struct
- let name = "Db.Value.Conditions_table"
- let size = 101
- let dependencies = only_self
- end)
-
- let merge_conditions h =
- Cil_datatype.Stmt.Hashtbl.iter
- (fun stmt v ->
- try
- let old = Conditions_table.find stmt in
- Conditions_table.replace stmt (old lor v)
- with Not_found ->
- Conditions_table.add stmt v)
- h
-
- let mask_then = 1
- let mask_else = 2
-
- let condition_truth_value s =
- try
- let i = Conditions_table.find s in
- ((i land mask_then) <> 0, (i land mask_else) <> 0)
- with Not_found -> false, false
-
- let compute = mk_fun "Value.compute"
-
-end
-
(* ************************************************************************* *)
(** {2 Others plugins} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 7867a74f246a0f5f098b09b0ea08d9e312866339..ff51d3e0f5b15023c5b7e1fd665756a7f5c85313 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -96,100 +96,6 @@ module Toplevel: sig
end
-(* ************************************************************************* *)
-(** {2 Values} *)
-(* ************************************************************************* *)
-
-(** Deprecated module: use the Eva.mli API instead. *)
-module Value : sig
-
- type state = Cvalue.Model.t
- (** Internal state of the value analysis. *)
-
- type t = Cvalue.V.t
- (** Internal representation of a value. *)
-
- val proxy: State_builder.Proxy.t
-
- val self : State.t
- (** Internal state of the value analysis from projects viewpoint.
- @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
-
- val compute : (unit -> unit) ref
- (** Compute the value analysis 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 condition_truth_value: stmt -> bool * bool
- (** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)]
- (resp. snd) is true if and only if the condition of the 'if' has been
- evaluated to true (resp. false) at least once during the analysis. *)
-
- (** {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 used by the analysis *)
- val globals_state : unit -> state
-
-
- (** @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 merge_conditions: int Cil_datatype.Stmt.Hashtbl.t -> unit
- val mask_then: int
- val mask_else: int
-
- val initial_state_only_globals : (unit -> state) ref
-
- val initial_state_changed: (unit -> unit) ref
-end
-[@@alert db_deprecated
- "Db.Value is deprecated and will be removed in a future version \
- of Frama-C. Please use the Eva.mli public API instead."]
-
(* ************************************************************************* *)
(** {2 Plugins} *)
(* ************************************************************************* *)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index f0e9343182ce137b504a561328d583f472725e88..33d434deb9819cfe16e8506fe206fc62e690cf59 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
@@ -116,7 +113,6 @@ module Analysis: sig
end
module Callstack: sig
- [@@@ alert "-db_deprecated"]
(** A call is identified by the function called and the call statement *)
type call = Cil_types.kernel_function * Cil_types.stmt
@@ -803,6 +799,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/alarmset.ml b/src/plugins/eva/alarmset.ml
index d902c0d852f9830c0c9a1d85c67b90aa88a1a839..88c99208679080682094f369c6db18bd0e5283e9 100644
--- a/src/plugins/eva/alarmset.ml
+++ b/src/plugins/eva/alarmset.ml
@@ -205,8 +205,6 @@ let for_all test ~default = function
Alarms
------------------------------------------------------------------------ *)
-open CilE
-
let emitter = Eva_utils.emitter
(* Printer that shows additional information about temporaries *)
@@ -432,32 +430,6 @@ let emit kinstr = function
"All alarms may arise: \
abstract state too imprecise to continue the analysis."
-let warn_alarm warn_mode = function
- | Alarms.Uninitialized _
- | Alarms.Dangling _
- -> warn_mode.unspecified ()
- | Alarms.Pointer_comparison _
- | Alarms.Differing_blocks _
- -> warn_mode.defined_logic ()
- | Alarms.Division_by_zero _
- | Alarms.Overflow _
- | Alarms.Float_to_int _
- | Alarms.Invalid_shift _
- | Alarms.Memory_access _
- | Alarms.Index_out_of_bound _
- | Alarms.Invalid_pointer _
- | Alarms.Is_nan_or_infinite _
- | Alarms.Is_nan _
- | Alarms.Not_separated _
- | Alarms.Overlap _
- | Alarms.Function_pointer _
- | Alarms.Invalid_bool _
- -> warn_mode.others ()
-
-let notify warn_mode alarms =
- iter (fun alarm _status -> warn_alarm warn_mode alarm) alarms
-
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/eva/alarmset.mli b/src/plugins/eva/alarmset.mli
index 7363b281e6f21eb7fdb18e5f34273796a9c102f8..850f8e6d7b3d3772b62089c77f996cdd2254472b 100644
--- a/src/plugins/eva/alarmset.mli
+++ b/src/plugins/eva/alarmset.mli
@@ -104,10 +104,6 @@ val fold : (alarm -> status -> 'a -> 'a) -> 'a -> t -> 'a
instruction. *)
val emit: Cil_types.kinstr -> t -> unit
-(** Calls the functions registered in the [warn_mode] according to the
- set of alarms. *)
-val notify: CilE.warn_mode -> t -> unit
-
val pretty : Format.formatter -> t -> unit
val pretty_status : Format.formatter -> status -> unit
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index 9a3d06be43283a6417be2fcede82b8b3c1b54090..7023a1e20869441630a0ce257e11798603971a3f 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -40,7 +40,7 @@
(name eva)
(optional)
(public_name frama-c-eva.core)
- (flags -open Frama_c_kernel :standard -w -9 -alert -db_deprecated)
+ (flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-server.core)
(instrumentation (backend landmarks))
(instrumentation (backend bisect_ppx))
@@ -60,7 +60,7 @@
(name eva_gui)
(optional)
(public_name frama-c-eva.gui)
- (flags -open Frama_c_kernel -open Frama_c_gui -open Eva__Private :standard -w -9 -alert -db_deprecated)
+ (flags -open Frama_c_kernel -open Frama_c_gui -open Eva__Private :standard -w -9)
(libraries eva frama-c.kernel frama-c.gui)
(instrumentation (backend landmarks))))
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index 6bbfef27ba4dc1a948398cb182431dd2c0fda689..aee5de68bf0f43530d7fad97ae8be115ad7c227a 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 =
@@ -238,7 +229,6 @@ let compute =
let name = "Eva.Analysis.compute" in
fst (State_builder.apply_once name [ Self.state ] compute)
-let () = Db.Value.compute := compute
let () = Parameters.ForceValues.set_output_dependencies [Self.state]
let main () =
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/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..7c8a63d15d27f4c32b2fa410cddd9d688cab5c23 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:
@@ -274,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
@@ -292,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
@@ -357,19 +359,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 +387,16 @@ module Make
let initial_state_with_formals ~lib_entry kf =
let init_state =
- if Db.Value.globals_use_supplied_state ()
- then begin
+ match Eva_results.get_initial_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/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index 28a09aefb91ba4effb0aa2d49f0ee2a97f5c8e6f..899fb60129901f150699afc38977f924bef104f0 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -43,6 +43,33 @@ let blocks_share_locals b1 b2 =
| v1 :: _, v2 :: _ -> v1.vid = v2.vid
| _, _ -> false
+
+module Conditions_table =
+ Cil_state_builder.Stmt_hashtbl
+ (Datatype.Pair (Datatype.Bool) (Datatype.Bool))
+ (struct
+ let name = "Eva.Iterator.Conditions_table"
+ let size = 101
+ let dependencies = [ Self.state ]
+ end)
+
+let condition_truth_value s =
+ try Conditions_table.find s
+ with Not_found -> false, false
+
+let record_fireable edge =
+ match edge.edge_transition with
+ | Guard (_exp, kind, stmt) ->
+ let b_then, b_else = condition_truth_value stmt in
+ let new_status =
+ match kind with
+ | Then -> true, b_else
+ | Else -> b_then, true
+ in
+ Conditions_table.replace stmt new_status
+ | _ -> ()
+
+
module Make_Dataflow
(Abstract : Abstractions.S_with_evaluation)
(States : Powerset.S with type state = Abstract.Dom.t)
@@ -104,10 +131,6 @@ module Make_Dataflow
type tank = Partitioning.tank
type widening = Partitioning.widening
- type edge_info = {
- mutable fireable : bool (* Does any states survive the transition ? *)
- }
-
(* --- Interpreted automata --- *)
@@ -171,7 +194,7 @@ module Make_Dataflow
VertexTable.create control_point_count
let w_table : widening VertexTable.t =
VertexTable.create 7
- let e_table : (tank * edge_info) EdgeTable.t =
+ let e_table : tank EdgeTable.t =
EdgeTable.create transition_count
(* Default (Initial) stores on vertex and edges *)
@@ -179,18 +202,18 @@ module Make_Dataflow
Partitioning.empty_store ~stmt:v.vertex_start_of
let default_vertex_widening (v : vertex) () : widening =
Partitioning.empty_widening ~stmt:v.vertex_start_of
- let default_edge_tank () : tank * edge_info =
- Partitioning.empty_tank (), { fireable = false }
+ let default_edge_tank () : tank =
+ Partitioning.empty_tank ()
(* Get the stores associated to a control point or edge *)
let get_vertex_store (v : vertex) : store =
VertexTable.find_or_add v_table v ~default:(default_vertex_store v)
let get_vertex_widening (v : vertex) : widening =
VertexTable.find_or_add w_table v ~default:(default_vertex_widening v)
- let get_edge_data (e : vertex edge) : tank * edge_info =
+ let get_edge_data (e : vertex edge) : tank =
EdgeTable.find_or_add e_table e ~default:default_edge_tank
let get_succ_tanks (v : vertex) : tank list =
- List.map (fun (_,e,_) -> fst (get_edge_data e)) (G.succ_e graph v)
+ List.map (fun (_,e,_) -> get_edge_data e) (G.succ_e graph v)
module StmtTable = struct
include Cil_datatype.Stmt.Hashtbl
@@ -422,7 +445,7 @@ module Make_Dataflow
let process_edge (v1,e,v2 : G.edge) : flow =
let {edge_transition=transition; edge_kinstr=kinstr} = e in
- let tank,edge_info = get_edge_data e in
+ let tank = get_edge_data e in
let flow = Partitioning.drain tank in
Db.yield ();
check_signals ();
@@ -431,7 +454,7 @@ module Make_Dataflow
let flow = Partitioning.transfer (transfer_transition transition) flow in
let flow = process_partitioning_transitions v1 v2 transition flow in
if not (Partitioning.is_empty_flow flow) then
- edge_info.fireable <- true;
+ record_fireable e;
flow
let gather_cvalues states = match get_cvalue with
@@ -526,7 +549,7 @@ module Make_Dataflow
let reset_component (vertex_list : vertex list) : unit =
let reset_edge (_,e,_) =
- let t,_ = get_edge_data e in
+ let t = get_edge_data e in
Partitioning.reset_tank t
in
let reset_vertex v =
@@ -611,29 +634,6 @@ module Make_Dataflow
(* --- Results conversion --- *)
- let merge_conditions () =
- let table = StmtTable.create 5 in
- let fill (_,e,_) =
- match e.edge_transition with
- | Guard (_exp,kind,stmt) ->
- let mask = match kind with
- | Then -> Db.Value.mask_then
- | Else -> Db.Value.mask_else
- in
- let edge_info = snd (get_edge_data e) in
- let old_status =
- try StmtTable.find table stmt
- with Not_found -> 0
- and status =
- if edge_info.fireable then mask else 0
- in
- let new_status = old_status lor status in
- StmtTable.replace table stmt new_status;
- | _ -> ()
- in
- G.iter_edges_e fill graph;
- Db.Value.merge_conditions table
-
let is_instr s = match s.skind with Instr _ -> true | _ -> false
let states_after_stmt states_before states_after =
@@ -693,7 +693,6 @@ module Make_Dataflow
and register_post = Domain.Store.register_state_after_stmt callstack in
StmtTable.iter register_pre (Lazy.force merged_pre_states);
StmtTable.iter register_post (Lazy.force merged_post_states);
- merge_conditions ();
end;
let states =
Cvalue_callbacks.{ before_stmts = merged_pre_cvalues;
diff --git a/src/plugins/eva/engine/iterator.mli b/src/plugins/eva/engine/iterator.mli
index 0d1f9944063057b116f95a53af45b2766169cd64..4c8d02c16bbfa8a8c7d51cdf93fc0e2a719b0c57 100644
--- a/src/plugins/eva/engine/iterator.mli
+++ b/src/plugins/eva/engine/iterator.mli
@@ -25,6 +25,11 @@ open Cil_types
(** Mark the analysis as aborted. It will be stopped at the next safe point *)
val signal_abort: unit -> unit
+(** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)]
+ (resp. snd) is true if and only if the condition of the 'if' has been
+ evaluated to true (resp. false) at least once during the analysis. *)
+val condition_truth_value: stmt -> bool * bool
+
module Computer
(* Abstractions with the evaluator. *)
(Abstract: Abstractions.S_with_evaluation)
diff --git a/src/plugins/eva/legacy/TOREMOVE b/src/plugins/eva/legacy/TOREMOVE
index a45847d25ad5d534973f2563e1c31130ecacab8f..7fc89bce7fe16e277a92ae32d0c20bcce97b3df6 100644
--- a/src/plugins/eva/legacy/TOREMOVE
+++ b/src/plugins/eva/legacy/TOREMOVE
@@ -1,11 +1,6 @@
-**Function_args**: only there to fill Db.Value.add_formals_to_state, itself used
- by Inout/Cumulative_analysis. [compute_actual] is now in [Transfer_stmt],
- [actualize_formals] is in [Cvalue_transfer]
-
**Eval_op**: multiple dependencies in Eval_terms and builtins. Must be rewritten
into the corresponding functionality in Cvalue_forward. This requires having
contexts for logic terms, though.
-
To be moved elsewhere, probably in domains/cvalue or in engine:
eval_annots, eval_terms
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/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/self.ml b/src/plugins/eva/self.ml
index 072213e1a68c550fc1389bb697e0d79b71937b1c..e802fe89a788a0f252b63391adc6d03ae6dea5a0 100644
--- a/src/plugins/eva/self.ml
+++ b/src/plugins/eva/self.ml
@@ -38,14 +38,9 @@ let kernel_dependencies =
Alarms.self;
Annotations.code_annot_state; ]
-let dependencies = Db.Value.self :: kernel_dependencies
-
-let proxy = State_builder.Proxy.(create "eva" Forward dependencies)
+let proxy = State_builder.Proxy.(create "eva" Forward kernel_dependencies)
let state = State_builder.Proxy.get proxy
-let () = State_builder.Proxy.extend [state] Db.Value.proxy
-
-
(* Current state of the analysis *)
type computation_state = NotComputed | Computing | Computed | Aborted
diff --git a/src/plugins/eva/types/callstack.mli b/src/plugins/eva/types/callstack.mli
index 76701e429dcc298daca823dc8673760ef03d4417..f63751e19d9ecf65bea5d2f19db6ee7474200be2 100644
--- a/src/plugins/eva/types/callstack.mli
+++ b/src/plugins/eva/types/callstack.mli
@@ -21,7 +21,6 @@
(**************************************************************************)
[@@@ api_start]
-[@@@ alert "-db_deprecated"]
(** A call is identified by the function called and the call statement *)
type call = Cil_types.kernel_function * Cil_types.stmt
diff --git a/src/plugins/eva/utils/eva_results.ml b/src/plugins/eva/utils/eva_results.ml
index 606158151f651cc2197e55f78b3b4b26ecfc1ca4..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} *)
@@ -57,7 +104,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,8 +140,8 @@ 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_args = Db.Value.fun_get_args () in
+ let initial_state = Cvalue_results.get_global_state () 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
@@ -133,11 +180,11 @@ 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 ()
- | 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) =
@@ -254,7 +301,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
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
diff --git a/src/plugins/eva/utils/results.ml b/src/plugins/eva/utils/results.ml
index bc78a896d00c381e9616a2a675b4f7a6b3152029..297a2b22d2edf20faaac55e7e7c4e5a6443e824d 100644
--- a/src/plugins/eva/utils/results.ml
+++ b/src/plugins/eva/utils/results.ml
@@ -774,7 +774,7 @@ let is_reachable_kinstr kinstr =
let module M = Make () in
M.is_reachable (before_kinstr kinstr)
-let condition_truth_value = Db.Value.condition_truth_value
+let condition_truth_value = Iterator.condition_truth_value
(* Callers / callsites *)