[Eva] Removes logic inout functions from Db.Value.

src/kernel_services/plugin_entry_points/db.ml

@@ -591,19 +591,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
 

src/kernel_services/plugin_entry_points/db.mli

@@ -374,39 +374,6 @@ 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
-
   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

src/plugins/eva/register.ml

@@ -47,26 +47,14 @@ let access_value_of_location kinstr loc =
   let state = Db.Value.get_state kinstr in
   Db.Value.find state loc
 
-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;
 
 
@@ -415,8 +403,6 @@ let register (module Eval: Eval) (module Export: Export) =
 
 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