diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 2aef27b1268274b5d66fe630c3013e54e69f824a..ff9852652b41d923f1cc0b266f08c38057601301 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)
@@ -433,8 +419,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 get_fundec_from_stmt stmt =
let kf =
try
@@ -530,16 +514,6 @@ module Value = struct
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 =
@@ -552,29 +526,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"
@@ -590,31 +543,6 @@ module Value = struct
let lval_to_precise_loc_with_deps_state =
mk_fun "Value.lval_to_precise_loc_with_deps_state"
-
- 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
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 579158e1033139b3e5f078c029ebe5f33deb32ca..b87bf1fbf98c8298424d17e417e924eb77047074 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,28 +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
-
(** {3 Reachability} *)
val is_accessible : kinstr -> bool
@@ -295,23 +256,12 @@ module Value : sig
(** {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} *)
@@ -380,15 +330,6 @@ module Value : sig
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} *)
@@ -396,8 +337,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
@@ -407,12 +346,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. *)
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/register.ml b/src/plugins/eva/register.ml
index 1b5c144c995bd2adbe2b3fb8d78120029c1139d4..4bc58fcd1ff401fff40b6e3f4bbd442b1ef5dbd0 100644
--- a/src/plugins/eva/register.ml
+++ b/src/plugins/eva/register.ml
@@ -34,28 +34,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 () =
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.access := access_value_of_lval;
- Db.Value.access_location := access_value_of_location;
- Db.Value.access_expr := access_value_of_expr;
- Db.Value.valid_behaviors := Logic_inout.valid_behaviors;
(* -------------------------------------------------------------------------- *)
@@ -342,28 +323,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
@@ -396,8 +355,6 @@ 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;
()
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 ()