From 605fec48ba32e264bd9197970b6bf727b4ae59e0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 11 Jul 2023 18:26:48 +0200
Subject: [PATCH] [Eva] Removes logic inout functions from Db.Value.
---
src/kernel_services/plugin_entry_points/db.ml | 12 -------
.../plugin_entry_points/db.mli | 33 -------------------
src/plugins/eva/register.ml | 14 --------
3 files changed, 59 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 38f356a1c4e..39369632c9d 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/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
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 0bdab3e5919..d78a8959d43 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/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
diff --git a/src/plugins/eva/register.ml b/src/plugins/eva/register.ml
index ee8677596df..1b5c144c995 100644
--- a/src/plugins/eva/register.ml
+++ b/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
--
GitLab