diff --git a/src/kernel_services/abstract_interp/value_types.ml b/src/kernel_services/abstract_interp/value_types.ml
deleted file mode 100644
index d7d070d20e3053df8e3337c8921a6b9bd037c536..0000000000000000000000000000000000000000
--- a/src/kernel_services/abstract_interp/value_types.ml
+++ /dev/null
@@ -1,36 +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). *)
-(* *)
-(**************************************************************************)
-
-type 'a callback_result =
- | Normal of 'a
- | NormalStore of 'a * int
- | Reuse of int
-
-type call_froms = (Function_Froms.froms * Locations.Zone.t) option
-
-type logic_dependencies = Locations.Zone.t Cil_datatype.Logic_label.Map.t
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/abstract_interp/value_types.mli b/src/kernel_services/abstract_interp/value_types.mli
deleted file mode 100644
index 811e97b24fd8645dacd03b2224d5186e007f8c6a..0000000000000000000000000000000000000000
--- a/src/kernel_services/abstract_interp/value_types.mli
+++ /dev/null
@@ -1,44 +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). *)
-(* *)
-(**************************************************************************)
-
-(** Declarations that are useful for plugins written on top of the results
- of Value. *)
-
-type 'a callback_result =
- | Normal of 'a
- | NormalStore of 'a * int
- | Reuse of int
-
-type call_froms = (Function_Froms.froms * Locations.Zone.t) option
-(** If not None, the froms of the function, and its sure outputs;
- i.e. the dependencies of the result, and the dependencies
- of each zone written to. *)
-
-(** Dependencies for the evaluation of a term or a predicate: for each
- program point involved, sets of zones that must be read *)
-type logic_dependencies = Locations.Zone.t Cil_datatype.Logic_label.Map.t
-
-(*
-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 2cbd4c86ed67b863730b680daac78bcc60029fc0..c09f4e6b4fccfd0434b06eda9a42e17544ab4eaa 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -319,20 +319,6 @@ module Value = struct
((i land mask_then) <> 0, (i land mask_else) <> 0)
with Not_found -> false, false
- module RecursiveCallsFound =
- State_builder.Set_ref
- (Kernel_function.Set)
- (struct
- let name = "Db.Value.RecursiveCallsFound"
- let dependencies = only_self
- end)
-
- let ignored_recursive_call kf =
- RecursiveCallsFound.mem kf
-
- let recursive_call_occurred kf =
- RecursiveCallsFound.add kf
-
module Called_Functions_By_Callstack =
State_builder.Hashtbl(Kernel_function.Hashtbl)
(States_by_callstack)
@@ -369,54 +355,6 @@ module Value = struct
Cvalue.Model.pretty v)
*)
- module Record_Value_Callbacks =
- Hook.Build
- (struct
- type t = callstack * (state Stmt.Hashtbl.t) Lazy.t
- end)
-
- module Record_Value_Callbacks_New =
- Hook.Build
- (struct
- type t =
- callstack *
- ((state Stmt.Hashtbl.t) Lazy.t * (state Stmt.Hashtbl.t) Lazy.t)
- Value_types.callback_result
- end)
-
- module Record_Value_After_Callbacks =
- Hook.Build
- (struct
- type t = callstack * (state Stmt.Hashtbl.t) Lazy.t
- end)
-
- module Record_Value_Superposition_Callbacks =
- Hook.Build
- (struct
- type t = callstack * (state list Stmt.Hashtbl.t) Lazy.t
- end)
-
- module Call_Value_Callbacks =
- Hook.Build
- (struct type t = state * callstack end)
-
- module Call_Type_Value_Callbacks =
- Hook.Build(struct
- type t = [`Builtin | `Spec
- | `Body | `Reuse]
- * state * callstack end)
- ;;
-
-
- module Compute_Statement_Callbacks =
- Hook.Build
- (struct type t = stmt * callstack * state list end)
-
- (* -remove-redundant-alarms feature, applied at the end of an Eva analysis,
- fulfilled by the Scope plugin that also depends on Eva. We thus use a
- reference here to avoid a cyclic dependency. *)
- let rm_asserts = mk_fun "Value.rm_asserts"
-
let no_results = mk_fun "Value.no_results"
let update_callstack_table ~after stmt callstack v =
@@ -476,10 +414,6 @@ module Value = struct
try Some (Called_Functions_By_Callstack.find kf)
with Not_found -> None
- let valid_behaviors = mk_fun "Value.get_valid_behaviors"
-
- let add_formals_to_state = mk_fun "add_formals_to_state"
-
let get_fundec_from_stmt stmt =
let kf =
try
@@ -572,19 +506,6 @@ module Value = struct
| Kglobal -> Cvalue.Model.is_reachable (globals_state ())
| Kstmt stmt -> is_reachable_stmt stmt
- let is_called = mk_fun "Value.is_called"
- let callers = mk_fun "Value.callers"
-
- let access_location = mk_fun "Value.access_location"
-
- let find state loc = Cvalue.Model.find state loc
-
- let access = mk_fun "Value.access"
- let access_expr = mk_fun "Value.access_expr"
-
- let use_spec_instead_of_definition =
- mk_fun "Value.use_spec_instead_of_definition"
-
let eval_lval =
ref (fun ?with_alarms:_ _ -> mk_labeled_fun "Value.eval_lval")
let eval_expr =
@@ -597,29 +518,8 @@ module Value = struct
let find_lv_plus = mk_fun "Value.find_lv_plus"
- let pretty_state = Cvalue.Model.pretty
-
- let pretty = Cvalue.V.pretty
-
let compute = mk_fun "Value.compute"
- let memoize = mk_fun "Value.memoize"
- let expr_to_kernel_function = mk_fun "Value.expr_to_kernel_function"
- let expr_to_kernel_function_state =
- mk_fun "Value.expr_to_kernel_function_state"
-
- exception Not_a_call
-
- let call_to_kernel_function call_stmt = match call_stmt.skind with
- | Instr (Call (_, fexp, _, _)) ->
- let _, called_functions =
- !expr_to_kernel_function ?with_alarms:None ~deps:None
- (Kstmt call_stmt) fexp
- in called_functions
- | Instr(Local_init(_, ConsInit(f,_,_),_)) ->
- Kernel_function.Hptset.singleton (Globals.Functions.get f)
- | _ -> raise Not_a_call
-
let lval_to_loc_with_deps = mk_fun "Value.lval_to_loc_with_deps"
let lval_to_loc_with_deps_state = mk_fun "Value.lval_to_loc_with_deps_state"
@@ -634,54 +534,7 @@ module Value = struct
ref (fun ?with_alarms:_ _ -> mk_labeled_fun "Value.lval_to_precise_loc")
let lval_to_precise_loc_with_deps_state =
mk_fun "Value.lval_to_precise_loc_with_deps_state"
- let assigns_inputs_to_zone = mk_fun "Value.assigns_inputs_to_zone"
- let assigns_outputs_to_zone = mk_fun "Value.assigns_outputs_to_zone"
- let assigns_outputs_to_locations = mk_fun "Value.assigns_outputs_to_locations"
- let verify_assigns_froms = mk_fun "Value.verify_assigns_froms"
-
- module Logic = struct
- let eval_predicate =
- ref (fun ~pre:_ ~here:_ _ ->
- raise
- (Extlib.Unregistered_function
- "Function 'Value.Logic.eval_predicate' not registered yet"))
-
- end
-
- exception Void_Function
-
- let find_return_loc kf =
- try
- let ki = Kernel_function.find_return kf in
- let lval = match ki with
- | { skind = Return (Some ({enode = Lval ((_ , offset) as lval)}), _) }
- ->
- assert (offset = NoOffset) ;
- lval
- | { skind = Return (None, _) } -> raise Void_Function
- | _ -> assert false
- in
- !lval_to_loc (Kstmt ki) ?with_alarms:None lval
- with Kernel_function.No_Statement ->
- (* [JS 2011/05/17] should be better to have another name for this
- exception or another one since it is possible to have no return without
- returning void (the case when the kf corresponds to a declaration *)
- raise Void_Function
-
- let display = mk_fun "Value.display"
-
- let emitter = ref Emitter.dummy
-
-end
-
-module From = struct
- exception Not_lval
- let find_deps_no_transitivity = mk_fun "From.find_deps_no_transitivity"
- let find_deps_no_transitivity_state =
- mk_fun "From.find_deps_no_transitivity_state"
- let find_deps_term_no_transitivity_state =
- mk_fun "From.find_deps_term_no_transitivity_state"
end
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 4a82d0b724c34198a6b7dcb7821732989a710ebd..18c76a9838ef2d6eb38920f0f7da01e5a6689a46 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -109,9 +109,6 @@ module Value : sig
type t = Cvalue.V.t
(** Internal representation of a value. *)
- val emitter: Emitter.t ref
- (** Emitter used by Value to emit statuses *)
-
val proxy: State_builder.Proxy.t
val self : State.t
@@ -151,23 +148,11 @@ module Value : sig
of each reachable and evaluable statement. Filled only if
[Value_parameters.ResultsAfter] is set. *)
- val ignored_recursive_call: kernel_function -> bool
- (** This functions returns true if the value analysis found and ignored
- a recursive call to this function during the analysis. *)
-
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. *)
- (** {3 Parameterization} *)
-
- val use_spec_instead_of_definition: (kernel_function -> bool) ref
- (** To be called by derived analyses to determine if they must use
- the body of the function (if available), or only its spec. Used for
- value builtins, and option -val-use-spec. *)
-
-
(** {4 Arguments of the main function} *)
(** The functions below are related to the arguments that are passed to the
@@ -237,8 +222,6 @@ module Value : sig
val fold_state_callstack :
(state -> 'a -> 'a) -> 'a -> after:bool -> kinstr -> 'a
- val find : state -> Locations.location -> t
-
(** {3 Evaluations} *)
val eval_lval :
@@ -263,33 +246,6 @@ module Value : sig
(** returns the list of all decompositions of [expr] into the sum an lvalue
and an interval. *)
- (** {3 Values and kernel functions} *)
-
- val expr_to_kernel_function :
- (kinstr
- -> ?with_alarms:CilE.warn_mode
- -> deps:Locations.Zone.t option
- -> exp
- -> Locations.Zone.t * Kernel_function.Hptset.t) ref
-
- val expr_to_kernel_function_state :
- (state
- -> deps:Locations.Zone.t option
- -> exp
- -> Locations.Zone.t * Kernel_function.Hptset.t) ref
-
- exception Not_a_call
- val call_to_kernel_function : stmt -> Kernel_function.Hptset.t
- (** Return the functions that can be called from this call.
- @raise Not_a_call if the statement is not a call. *)
-
- val valid_behaviors: (kernel_function -> state -> funbehavior list) ref
-
- val add_formals_to_state: (state -> kernel_function -> exp list -> state) ref
- (** [add_formals_to_state state kf exps] evaluates [exps] in [state]
- and binds them to the formal arguments of [kf] in the resulting
- state *)
-
(** {3 Reachability} *)
val is_accessible : kinstr -> bool
@@ -298,26 +254,6 @@ module Value : sig
val is_reachable_stmt : stmt -> bool
- (** {3 About kernel functions} *)
-
- exception Void_Function
- val find_return_loc : kernel_function -> Locations.location
- (** Return the location of the returned lvalue of the given function.
- @raise Void_Function if the function does not return any value. *)
-
- val is_called: (kernel_function -> bool) ref
-
- val callers: (kernel_function -> (kernel_function*stmt list) list) ref
- (** @return the list of callers with their call sites. Each function is
- present only once in the list. *)
-
- (** {3 State before a kinstr} *)
-
- val access : (kinstr -> lval -> t) ref
- val access_expr : (kinstr -> exp -> t) ref
- val access_location : (kinstr -> Locations.location -> t) ref
-
-
(** {3 Locations of left values} *)
val lval_to_loc :
@@ -374,105 +310,12 @@ module Value : sig
Locations.Zone.t * Precise_locs.precise_location) ref
- (** Evaluation of the [\from] clause of an [assigns] clause.*)
- val assigns_inputs_to_zone :
- (state -> assigns -> Locations.Zone.t) ref
-
- (** Evaluation of the left part of [assigns] clause (without [\from]).*)
- val assigns_outputs_to_zone :
- (state -> result:varinfo option -> assigns -> Locations.Zone.t) ref
-
- (** Evaluation of the left part of [assigns] clause (without [\from]). Each
- assigns term results in one location. *)
- val assigns_outputs_to_locations :
- (state -> result:varinfo option -> assigns -> Locations.location list) ref
-
- (** For internal use only. Evaluate the [assigns] clause of the
- given function in the given prestate, compare it with the
- computed froms, return warning and set statuses. *)
- val verify_assigns_froms :
- (Kernel_function.t -> pre:state -> Function_Froms.t -> unit) ref
-
-
- (** {3 Evaluation of logic terms and predicates} *)
- module Logic : sig
- (** The APIs of this module are not stabilized yet, and are subject
- to change between Frama-C versions. *)
-
- val eval_predicate:
- (pre:state -> here:state -> predicate ->
- Property_status.emitted_status) ref
- (** Evaluate the given predicate in the given states for the Pre
- and Here ACSL labels.
- @since Neon-20140301 *)
- end
-
-
- (** {3 Callbacks} *)
-
- (** Actions to perform at end of each function analysis. Not compatible with
- option [-memexec-all] *)
-
- module Record_Value_Callbacks:
- Hook.Iter_hook
- with type param = callstack * (state Stmt.Hashtbl.t) Lazy.t
-
- module Record_Value_Superposition_Callbacks:
- Hook.Iter_hook
- with type param = callstack * (state list Stmt.Hashtbl.t) Lazy.t
-
- module Record_Value_After_Callbacks:
- Hook.Iter_hook
- with type param = callstack * (state Stmt.Hashtbl.t) Lazy.t
-
- (**/**)
- (* Temporary API, do not use *)
- module Record_Value_Callbacks_New: Hook.Iter_hook
- with type param =
- callstack *
- ((state Stmt.Hashtbl.t) Lazy.t (* before states *) *
- (state Stmt.Hashtbl.t) Lazy.t) (* after states *)
- Value_types.callback_result
- (**/**)
-
val no_results: (fundec -> bool) ref
(** Returns [true] if the user has requested that no results should
be recorded for this function. If possible, hooks registered
on [Record_Value_Callbacks] and [Record_Value_Callbacks_New]
should not force their lazy argument *)
- (** Actions to perform at each treatment of a "call"
- statement. [state] is the state before the call.
- @deprecated Use Call_Type_Value_Callbacks instead. *)
- module Call_Value_Callbacks:
- Hook.Iter_hook with type param = state * callstack
-
- (** Actions to perform at each treatment of a "call"
- statement. [state] is the state before the call.
- @since Aluminium-20160501 *)
- module Call_Type_Value_Callbacks:
- Hook.Iter_hook with type param =
- [`Builtin | `Spec | `Body | `Reuse]
- * state * callstack
-
-
- (** Actions to perform whenever a statement is handled. *)
- module Compute_Statement_Callbacks:
- Hook.Iter_hook with type param = stmt * callstack * state list
-
- (* -remove-redundant-alarms feature, applied at the end of an Eva analysis,
- fulfilled by the Scope plugin that also depends on Eva. We thus use a
- reference here to avoid a cyclic dependency. *)
- val rm_asserts: (unit -> unit) ref
-
-
- (** {3 Pretty printing} *)
-
- val pretty : Format.formatter -> t -> unit
- val pretty_state : Format.formatter -> state -> unit
-
-
- val display : (Format.formatter -> kernel_function -> unit) ref
(**/**)
(** {3 Internal use only} *)
@@ -481,8 +324,6 @@ module Value : sig
(** To be used during the value analysis itself (instead of
{!get_state}). [after] is false by default. *)
- val recursive_call_occurred: kernel_function -> unit
-
val merge_conditions: int Cil_datatype.Stmt.Hashtbl.t -> unit
val mask_then: int
val mask_else: int
@@ -492,12 +333,6 @@ module Value : sig
val update_callstack_table: after:bool -> stmt -> callstack -> state -> unit
(* Merge a new state in the table indexed by callstacks. *)
-
- val memoize : (kernel_function -> unit) ref
- (* val compute_call :
- (kernel_function -> call_kinstr:kinstr -> state -> (exp*t) list
- -> Cvalue.V_Offsetmap.t option (** returned value of [kernel_function] *) * state) ref
- *)
val merge_initial_state : callstack -> kernel_function -> state -> unit
(** Store an additional possible initial state for the given callstack as
well as its values for actuals. *)
@@ -508,30 +343,6 @@ end
"Db.Value is deprecated and will be removed in a future version \
of Frama-C. Please use the Eva.mli public API instead."]
-(** Functional dependencies between function inputs and function outputs.
- @see <../from/index.html> internal documentation. *)
-module From : sig
-
- (** exception raised by [find_deps_no_transitivity_*] if the given expression
- is not an lvalue.
- @since Aluminium-20160501
- *)
- exception Not_lval
-
- val find_deps_no_transitivity : (stmt -> exp -> Locations.Zone.t) ref
-
- val find_deps_no_transitivity_state :
- (Cvalue.Model.t -> exp -> Locations.Zone.t) ref
-
- (** @raise Not_lval if the given expression is not a C lvalue. *)
- val find_deps_term_no_transitivity_state :
- (Cvalue.Model.t -> term -> Value_types.logic_dependencies) ref
-
-end
-[@@alert db_deprecated
- "Db.From is deprecated and will be removed in a future version \
- of Frama-C. Please use the From module or the Eva API instead."]
-
(* ************************************************************************* *)
(** {2 Plugins} *)
(* ************************************************************************* *)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 3357d50d8349a3d3e2e90fe704eb5394b2b9109d..9d6baa29c8440b1deaab66ab6fdfbdbc366c91cb 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -685,6 +685,11 @@ module Cvalue_callbacks: sig
type state = Cvalue.Model.t
+ (** If not None, the froms of the function, and its sure outputs;
+ i.e. the dependencies of the result, and the dependencies
+ of each zone written to. *)
+ type call_froms = (Function_Froms.froms * Locations.Zone.t) option
+
type analysis_kind =
[ `Builtin (** A cvalue builtin is used to interpret the function. *)
| `Spec (** The specification is used to interpret the function. *)
@@ -708,7 +713,7 @@ module Cvalue_callbacks: sig
(** Results of a function call. *)
type call_results =
- [ `Builtin of state list * Value_types.call_froms
+ [ `Builtin of state list * call_froms
(** List of cvalue states at the end of the builtin. *)
| `Spec of state list
(** List of cvalue states at the end of the call. *)
diff --git a/src/plugins/eva/domains/cvalue/builtins_watchpoint.ml b/src/plugins/eva/domains/cvalue/builtins_watchpoint.ml
index 39c576d07b60206c8b24bbb7bc700503bc983aa2..695278f28d6f4ae42c1d87c4c3887acdce294c40 100644
--- a/src/plugins/eva/domains/cvalue/builtins_watchpoint.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_watchpoint.ml
@@ -96,7 +96,7 @@ let () =
Builtins.register_builtin "Frama_C_watch_cardinal" Cacheable
(add_watch make_watch_cardinal)
-let watch_hook (stmt, _callstack, states) =
+let watch_hook _callstack stmt states =
let treat ({name_lv = name; loc=loc; v=wa; remaining_count=current; stmts=set} as w) =
List.iter
(fun state ->
@@ -132,7 +132,7 @@ let watch_hook (stmt, _callstack, states) =
in
List.iter treat !watch_table
-let () = Db.Value.Compute_Statement_Callbacks.extend_once watch_hook
+let () = Cvalue_callbacks.register_statement_hook watch_hook
(*
Local Variables:
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 7822ad59369304d3781cdaa189f1c2abfb0fac4a..56b16b97f71b400fa7502c214f14319382e12f95 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -584,8 +584,6 @@ module State = struct
then Parameters.ForceValues.output display_results
end
-let () = Db.Value.display := (fun fmt kf -> State.display ~fmt kf)
-
let registered =
let name = "cvalue"
diff --git a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
index 222f8bbe68349524dabe96f1d9b91d1ed3e1e438..007674371f657ba8bdca117a649689e86287b3be 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
@@ -204,10 +204,7 @@ let actualize_formals state arguments =
List.fold_left treat_one_formal state arguments
let start_call _stmt call _recursion _valuation state =
- let with_formals = actualize_formals state call.arguments in
- let stack_with_call = Eva_utils.current_call_stack () in
- Db.Value.Call_Value_Callbacks.apply (with_formals, stack_with_call);
- `Value with_formals
+ `Value (actualize_formals state call.arguments)
let finalize_call stmt call _recursion ~pre:_ ~post:state =
(* Deallocate memory allocated via alloca().
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 9fda306efa9a0cafb74be4405962cf7d244a63ce..03dc9b5a62980335cac260fe0a35c8d5e8c0c418 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -353,16 +353,11 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* ----- Main call -------------------------------------------------------- *)
- let store_initial_state callstack kf init_state =
- Abstract.Dom.Store.register_initial_state callstack kf init_state;
- let cvalue_state = get_cvalue_or_top init_state in
- Db.Value.Call_Value_Callbacks.apply (cvalue_state, callstack)
-
let compute kf init_state =
let restore_signals = register_signal_handler () in
let compute () =
let callstack = Eva_utils.init_call_stack kf in
- store_initial_state callstack kf init_state;
+ Abstract.Dom.Store.register_initial_state callstack kf init_state;
let call = { kf; callstack; arguments = []; rest = []; return = None; } in
let final_result = compute_call Kglobal call None init_state in
let final_states = List.map snd (final_result.Transfer.states) in
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index e97c859d276e889eadf25f1374727816f36479fa..28a09aefb91ba4effb0aa2d49f0ee2a97f5c8e6f 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -35,7 +35,6 @@ let check_signals, signal_abort =
(fun () -> signal_emitted := true)
let dkey = Self.dkey_iterator
-let dkey_callbacks = Self.dkey_callbacks
let stat_iterations = Statistics.register_statement_stat "iterations"
let blocks_share_locals b1 b2 =
@@ -686,13 +685,6 @@ module Make_Dataflow
let merged_post_states = lazy
(states_after_stmt merged_pre_states merged_post_states)
in
- let unmerged_pre_cvalues = lazy
- (StmtTable.map (fun _stmt (v,_) ->
- let store = get_vertex_store v in
- let states = Partitioning.expanded store in
- List.map (fun (_k,x) -> get_cvalue_or_top x) states)
- automaton.stmt_table)
- in
let merged_pre_cvalues = lazy (lift_to_cvalues merged_pre_states)
and merged_post_cvalues = lazy (lift_to_cvalues merged_post_states) in
let callstack = Eva_utils.current_call_stack () in
@@ -703,22 +695,6 @@ module Make_Dataflow
StmtTable.iter register_post (Lazy.force merged_post_states);
merge_conditions ();
end;
- if not (Db.Value.Record_Value_Superposition_Callbacks.is_empty ())
- then begin
- if Parameters.ValShowProgress.get () then
- Self.debug ~dkey:dkey_callbacks
- "now calling Record_Value_Superposition callbacks";
- Db.Value.Record_Value_Superposition_Callbacks.apply
- (callstack, unmerged_pre_cvalues);
- end;
- if not (Db.Value.Record_Value_Callbacks.is_empty ())
- then begin
- if Parameters.ValShowProgress.get () then
- Self.debug ~dkey:dkey_callbacks
- "now calling Record_Value callbacks";
- Db.Value.Record_Value_Callbacks.apply
- (callstack, merged_pre_cvalues)
- end;
let states =
Cvalue_callbacks.{ before_stmts = merged_pre_cvalues;
after_stmts = merged_post_cvalues }
@@ -726,14 +702,6 @@ module Make_Dataflow
let cvalue_init = get_cvalue_or_top initial_state in
let results = `Body (states, Mem_exec.new_counter ()) in
Cvalue_callbacks.apply_call_results_hooks callstack kf cvalue_init results;
- if not (Db.Value.Record_Value_After_Callbacks.is_empty ())
- then begin
- if Parameters.ValShowProgress.get () then
- Self.debug ~dkey:dkey_callbacks
- "now calling Record_After_Value callbacks";
- Db.Value.Record_Value_After_Callbacks.apply
- (callstack, merged_post_cvalues);
- end;
end
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 75e3571534fd65d3b671950aa9250ccfcb87ed59..78ab84bc9725887ee9d3ce1810e128248af25ce5 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -733,7 +733,6 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let call_stack = Eva_utils.current_call_stack () in
let stack_with_call = Callstack.push kf stmt call_stack in
let cvalue_state = get_cvalue_or_top state in
- Db.Value.Call_Value_Callbacks.apply (cvalue_state, stack_with_call);
Cvalue_callbacks.apply_call_hooks stack_with_call kf cvalue_state `Builtin;
Cvalue_callbacks.apply_call_results_hooks stack_with_call kf cvalue_state
(`Builtin ([cvalue_state], None))
diff --git a/src/plugins/eva/legacy/function_args.ml b/src/plugins/eva/legacy/function_args.ml
deleted file mode 100644
index b1f4dd23053f3a49a56eccdd76ff835d4b8376e6..0000000000000000000000000000000000000000
--- a/src/plugins/eva/legacy/function_args.ml
+++ /dev/null
@@ -1,83 +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). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-open Lattice_bounds
-
-exception Actual_is_bottom
-exception WrongFunctionType (* at a call through a pointer *)
-
-let rec fold_left2_best_effort f acc l1 l2 =
- match l1,l2 with
- | _,[] -> acc
- | [],_ -> raise WrongFunctionType (* Too few arguments *)
- | (x1::r1),(x2::r2) -> fold_left2_best_effort f (f acc x1 x2) r1 r2
-
-let actualize_formals kf state actuals =
- let formals = Kernel_function.get_formals kf in
- let treat_one_formal acc actual_o formal =
- Cvalue.Model.add_base (Base.of_varinfo formal) actual_o acc
- in
- fold_left2_best_effort treat_one_formal state actuals formals
-
-let offsetmap_of_lv state lv =
- let open Locations in
- let state, loc_to_read, _typ = !Db.Value.lval_to_precise_loc_state state lv in
- let aux loc offsm_res =
- let size = Int_Base.project loc.size in
- let copy = Cvalue.Model.copy_offsetmap loc.loc size state in
- Bottom.join Cvalue.V_Offsetmap.join copy offsm_res
- in
- Precise_locs.fold aux loc_to_read `Bottom
-
-let compute_actual state e =
- match e with
- | { enode = Lval lv } when not (Eval_typ.is_bitfield (Cil.typeOfLval lv)) ->
- let o =
- try offsetmap_of_lv state lv
- with Abstract_interp.Error_Top ->
- Self.abort ~current:true
- "Function argument %a has unknown size. Aborting" Printer.pp_exp e;
- in begin
- match o with
- | `Value o -> o
- | `Bottom -> raise Actual_is_bottom
- end
- | _ ->
- let interpreted_expr = !Db.Value.eval_expr state e in
- if Cvalue.V.is_bottom interpreted_expr then raise Actual_is_bottom;
- let typ = Cil.typeOf e in
- Eval_op.offsetmap_of_v ~typ interpreted_expr
-
-let () =
- Db.Value.add_formals_to_state :=
- (fun state kf exps ->
- try
- let actuals = List.map (fun e -> compute_actual state e) exps in
- actualize_formals kf state actuals
- with Actual_is_bottom | WrongFunctionType -> Cvalue.Model.bottom)
-
-(*
-Local Variables:
-compile-command: "make -C ../../../.."
-End:
-*)
diff --git a/src/plugins/eva/legacy/function_args.mli b/src/plugins/eva/legacy/function_args.mli
deleted file mode 100644
index c2690f3b81659bccfa182f636ed5b8851db004ca..0000000000000000000000000000000000000000
--- a/src/plugins/eva/legacy/function_args.mli
+++ /dev/null
@@ -1,24 +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). *)
-(* *)
-(**************************************************************************)
-
-(** Nothing is exported; the function [compute_atual] is registered
- in {!Db.Value}. *)
diff --git a/src/plugins/eva/register.ml b/src/plugins/eva/register.ml
index 0994d6ee1ec9087820633e00d0d76eb0352e4ea2..7fd5081fe77c76679b400b083619f092d505611e 100644
--- a/src/plugins/eva/register.ml
+++ b/src/plugins/eva/register.ml
@@ -33,63 +33,9 @@ let main () =
let () = Db.Main.extend main
-
-(* "access" functions before evaluation, registered in Db.Value *)
-let access_value_of_lval kinstr lv =
- let state = Db.Value.get_state kinstr in
- snd (!Db.Value.eval_lval None state lv)
-
-let access_value_of_expr kinstr e =
- let state = Db.Value.get_state kinstr in
- !Db.Value.eval_expr state e
-
-let access_value_of_location kinstr loc =
- let state = Db.Value.get_state kinstr in
- Db.Value.find state loc
-
-let find_deps_term_no_transitivity_state state t =
- try
- let env = Eval_terms.env_only_here state in
- let r = Eval_terms.eval_term ~alarm_mode:Eval_terms.Ignore env t in
- r.Eval_terms.ldeps
- with Eval_terms.LogicEvalError _ -> raise Db.From.Not_lval
-
-let find_deps_no_transitivity stmt expr =
- Results.(before stmt |> expr_deps expr)
-
-let find_deps_no_transitivity_state state expr =
- Results.(in_cvalue_state state |> expr_deps expr)
-
-let eval_predicate ~pre ~here p =
- let open Eval_terms in
- let env = env_annot ~pre ~here () in
- match eval_predicate env p with
- | True -> Property_status.True
- | False -> Property_status.False_if_reachable
- | Unknown -> Property_status.Dont_know
-
-let () =
- Db.Value.is_called := Function_calls.is_called;
- Db.Value.callers := Function_calls.callsites;
- Db.Value.use_spec_instead_of_definition :=
- Function_calls.use_spec_instead_of_definition;
- Db.Value.assigns_outputs_to_zone :=
- (fun s ~result a -> Logic_inout.assigns_outputs_to_zone ~result s a);
- Db.Value.assigns_inputs_to_zone := Logic_inout.assigns_inputs_to_zone;
- Db.Value.access := access_value_of_lval;
- Db.Value.access_location := access_value_of_location;
- Db.Value.access_expr := access_value_of_expr;
- Db.Value.Logic.eval_predicate := eval_predicate;
- Db.Value.valid_behaviors := Logic_inout.valid_behaviors;
- Db.From.find_deps_term_no_transitivity_state :=
- find_deps_term_no_transitivity_state;
- Db.From.find_deps_no_transitivity := find_deps_no_transitivity;
- Db.From.find_deps_no_transitivity_state := find_deps_no_transitivity_state;
-
-
- (* -------------------------------------------------------------------------- *)
- (* Register Evaluation Functions *)
- (* -------------------------------------------------------------------------- *)
+(* -------------------------------------------------------------------------- *)
+(* Register Evaluation Functions *)
+(* -------------------------------------------------------------------------- *)
open Eval
@@ -371,28 +317,6 @@ module Export (Eval : Eval) = struct
let lval_to_offsetmap_state state lv =
lval_to_offsetmap_aux state lv
-
-
- let expr_to_kernel_function_state ?with_alarms state ~deps exp =
- let r, deps = resolv_func_vinfo ?with_alarms deps state exp in
- Option.value ~default:Locations.Zone.bottom deps, r
-
- let expr_to_kernel_function kinstr ?with_alarms ~deps exp =
- let state_to_joined_kernel_function state (z_acc, kf_acc) =
- let z, kf =
- expr_to_kernel_function_state ?with_alarms state ~deps exp
- in
- Locations.Zone.join z z_acc,
- Kernel_function.Hptset.union kf kf_acc
- in
- Db.Value.fold_state_callstack
- state_to_joined_kernel_function
- ((match deps with None -> Locations.Zone.bottom | Some z -> z),
- Kernel_function.Hptset.empty)
- ~after:false kinstr
-
- let expr_to_kernel_function_state =
- expr_to_kernel_function_state ?with_alarms:None
end
@@ -425,15 +349,11 @@ let register (module Eval: Eval) (module Export: Export) =
lval_to_precise_loc_with_deps_state;
Db.Value.lval_to_offsetmap := lval_to_offsetmap;
Db.Value.lval_to_offsetmap_state := lval_to_offsetmap_state;
- Db.Value.expr_to_kernel_function := expr_to_kernel_function;
- Db.Value.expr_to_kernel_function_state := expr_to_kernel_function_state;
()
let () = Db.Value.initial_state_only_globals := Analysis.cvalue_initial_state
-let () = Db.Value.verify_assigns_froms := Logic_inout.verify_assigns
-
let () =
let eval = (module Eval : Eval) in
let export = (module Export ((val eval : Eval)) : Export) in
diff --git a/src/plugins/eva/utils/cvalue_callbacks.ml b/src/plugins/eva/utils/cvalue_callbacks.ml
index d5bf54e2f5b77bc048ad80777e94aa85cc0e2c81..d4101a12b9c2de6f3a289deef62458ba3a3ef6c6 100644
--- a/src/plugins/eva/utils/cvalue_callbacks.ml
+++ b/src/plugins/eva/utils/cvalue_callbacks.ml
@@ -39,15 +39,15 @@ let register_call_hook f =
Call.extend (fun (callstack, kf, kind, state) -> f callstack kf kind state)
let apply_call_hooks callstack kf state kind =
- Call.apply (callstack, kf, state, kind);
- Db.Value.Call_Type_Value_Callbacks.apply (kind, state, callstack)
+ Call.apply (callstack, kf, state, kind)
+type call_froms = (Function_Froms.froms * Locations.Zone.t) option
type state_by_stmt = (state Cil_datatype.Stmt.Hashtbl.t) Lazy.t
type results = { before_stmts: state_by_stmt; after_stmts: state_by_stmt }
type call_results =
- [ `Builtin of state list * Value_types.call_froms
+ [ `Builtin of state list * call_froms
| `Spec of state list
| `Body of results * int
| `Reuse of int
@@ -65,21 +65,9 @@ let register_call_results_hook f =
(fun (callstack, kf, state, results) -> f callstack kf state results)
let apply_call_results_hooks callstack kf state call_results =
- if Parameters.ValShowProgress.get ()
- && not (Call_Results.is_empty ()
- && Db.Value.Record_Value_Callbacks_New.is_empty ())
+ if Parameters.ValShowProgress.get () && not (Call_Results.is_empty ())
then Self.debug ~dkey "now calling Call_Results callbacks";
- Call_Results.apply (callstack, kf, state, call_results);
- let results =
- match call_results with
- | `Builtin _ | `Spec _ -> None
- | `Reuse i -> Some (Value_types.Reuse i)
- | `Body ({before_stmts; after_stmts}, i) ->
- Some (Value_types.NormalStore ((before_stmts, after_stmts), i))
- in
- Option.iter
- (fun r -> Db.Value.Record_Value_Callbacks_New.apply (callstack, r))
- results
+ Call_Results.apply (callstack, kf, state, call_results)
module Statement =
@@ -89,5 +77,4 @@ let register_statement_hook f =
Statement.extend (fun (callstack, stmt, states) -> f callstack stmt states)
let apply_statement_hooks callstack stmt states =
- Statement.apply (callstack, stmt, states);
- Db.Value.Compute_Statement_Callbacks.apply (stmt, callstack, states)
+ Statement.apply (callstack, stmt, states)
diff --git a/src/plugins/eva/utils/cvalue_callbacks.mli b/src/plugins/eva/utils/cvalue_callbacks.mli
index 52d0d41330f31893650a9a232d2173376ea029bc..baa6dc0942ac19de3ec39a0ce11584b893626fe8 100644
--- a/src/plugins/eva/utils/cvalue_callbacks.mli
+++ b/src/plugins/eva/utils/cvalue_callbacks.mli
@@ -30,6 +30,11 @@
type state = Cvalue.Model.t
+(** If not None, the froms of the function, and its sure outputs;
+ i.e. the dependencies of the result, and the dependencies
+ of each zone written to. *)
+type call_froms = (Function_Froms.froms * Locations.Zone.t) option
+
type analysis_kind =
[ `Builtin (** A cvalue builtin is used to interpret the function. *)
| `Spec (** The specification is used to interpret the function. *)
@@ -53,7 +58,7 @@ type results = { before_stmts: state_by_stmt; after_stmts: state_by_stmt }
(** Results of a function call. *)
type call_results =
- [ `Builtin of state list * Value_types.call_froms
+ [ `Builtin of state list * call_froms
(** List of cvalue states at the end of the builtin. *)
| `Spec of state list
(** List of cvalue states at the end of the call. *)
diff --git a/src/plugins/eva/utils/eva_dynamic.ml b/src/plugins/eva/utils/eva_dynamic.ml
index ebfdc9384ad7969a7b94b12b290d03c92ccc47f0..c623675e2d22d95923eb4b3a9817f0c91cd2a8ec 100644
--- a/src/plugins/eva/utils/eva_dynamic.ml
+++ b/src/plugins/eva/utils/eva_dynamic.ml
@@ -62,5 +62,6 @@ module RteGen = struct
let mark_generated_rte () =
let list = all_statuses () in
let mark kf = List.iter (fun (_kind, set, _get) -> set kf true) list in
- Globals.Functions.iter (fun kf -> if !Db.Value.is_called kf then mark kf)
+ Globals.Functions.iter
+ (fun kf -> if Function_calls.is_called kf then mark kf)
end
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index 73dc03924ed0497f7e611994aeb9631803134333..1c3e435164f5ac9774c60b5390c7037c2061651d 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -79,8 +79,6 @@ let emitter =
~correctness:Parameters.parameters_correctness
~tuning:Parameters.parameters_tuning
-let () = Db.Value.emitter := emitter
-
let get_slevel kf =
try Parameters.SlevelFunction.find kf
with Not_found -> Parameters.SemanticUnrollingLevel.get ()
diff --git a/src/plugins/eva/utils/widen.ml b/src/plugins/eva/utils/widen.ml
index 00f6e6a4283eb02d0687521a5b4f732f7c8fcb52..2e4564b4ef0045ac2a79a43c30aacd65a2b2687f 100644
--- a/src/plugins/eva/utils/widen.ml
+++ b/src/plugins/eva/utils/widen.ml
@@ -561,7 +561,7 @@ let extract_per_function_hints fdec =
let per_function_hints = Per_Function_Hints.memo extract_per_function_hints
-let dynamic_widen_hints_hook (stmt, _callstack, states) =
+let dynamic_widen_hints_hook _callstack stmt states =
if Annotations.has_code_annot stmt then
let hs = parsed_dynamic_hints stmt in
if hs <> [] then
@@ -602,8 +602,7 @@ let dynamic_widen_hints_hook (stmt, _callstack, states) =
Dynamic_Hints.set hints;
end
-let () =
- Db.Value.Compute_Statement_Callbacks.extend_once dynamic_widen_hints_hook
+let () = Cvalue_callbacks.register_statement_hook dynamic_widen_hints_hook
let getWidenHints (kf:kernel_function) (stmt:stmt) =
let hints =
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index 513145d4b9f96e3016858c565b2c4176e932d7b0..f992fda8da2b72a2dc2d59a582b7fa832b201391 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -637,9 +637,6 @@ let rm_asserts () =
CA_Map.iter aux to_be_removed
end
-
-let () = Db.register Db.Value.rm_asserts rm_asserts [@alert "-db_deprecated"]
-
let rm_asserts =
Dynamic.register
~comment:"Remove redundant alarms. Used by the Eva plugin."