From 33ff506f987a88f8ea5401c1c0db7db22854a30b Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 10 Oct 2022 17:42:48 +0200
Subject: [PATCH] [kernel] Remove Db.Properties. Completely.
---
src/kernel_services/plugin_entry_points/db.ml | 97 ---------
.../plugin_entry_points/db.mli | 196 ------------------
src/plugins/eva/legacy/eval_terms.ml | 28 ---
3 files changed, 321 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 20331018415..bdf3b968626 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -683,103 +683,6 @@ module From = struct
mk_fun "From.find_deps_term_no_transitivity_state"
end
-(* ************************************************************************* *)
-(** {2 Properties} *)
-(* ************************************************************************* *)
-
-module Properties = struct
-
- let mk_resultfun s =
- ref (fun ~result:_ -> failwith (Printf.sprintf "Function '%s' not registered yet" s))
-
- module Interp = struct
-
- exception No_conversion = Logic_to_c.No_conversion
-
- (** Interpretation and conversions of of formulas *)
- let code_annot = ref Logic_parse_string.code_annot
- let term_lval = ref Logic_parse_string.term_lval
- let term = ref Logic_parse_string.term
- let predicate = ref Logic_parse_string.predicate
-
- let mandatory_result f ~result = f ?result
- let term_lval_to_lval = ref (mandatory_result Logic_to_c.term_lval_to_lval)
- let term_to_exp = ref (mandatory_result Logic_to_c.term_to_exp)
- let term_to_lval = ref (mandatory_result Logic_to_c.term_to_lval)
- let loc_to_lval = ref (mandatory_result Logic_to_c.loc_to_lval)
- (* loc_to_loc and loc_to_locs are defined in Value/Eval_logic, not
- in Logic_interp *)
- let loc_to_loc = mk_resultfun "Properties.Interp.loc_to_loc"
- let loc_to_loc_under_over = mk_resultfun "Properties.Interp.loc_to_loc_with_deps"
- let loc_to_offset = ref (mandatory_result Logic_to_c.loc_to_offset)
- let loc_to_exp = ref (mandatory_result Logic_to_c.loc_to_exp)
- let term_offset_to_offset =
- ref (mandatory_result Logic_to_c.term_offset_to_offset)
-
- module To_zone =
- struct
- type t_ctx =
- { state_opt: bool option;
- ki_opt: (stmt * bool) option;
- kf:Kernel_function.t }
-
- type t = Logic_deps.t =
- {before:bool ;
- ki:stmt ; zone:Locations.Zone.t}
- type t_zone_info = (t list) option
- type t_decl = Logic_deps.decl =
- {var: Varinfo.Set.t ;
- lbl: Logic_label.Set.t}
- type t_pragmas = Logic_deps.pragmas =
- {ctrl: Stmt.Set.t ;
- stmt: Stmt.Set.t}
-
- let mk_ctx_func_contrat = ref (fun kf ~state_opt ->
- { state_opt = state_opt;
- ki_opt = None;
- kf = kf })
-
- let mk_ctx_stmt_contrat = ref (fun kf ki ~state_opt ->
- { state_opt=state_opt;
- ki_opt= Some(ki, false);
- kf = kf })
-
- let mk_ctx_stmt_annot = ref (fun kf ki ->
- { state_opt = Some true;
- ki_opt = Some(ki, true);
- kf = kf })
-
- let adapt_ctx ctx =
- let site = match ctx.ki_opt with
- | None -> Logic_deps.FunctionContract
- | Some (stmt, false) -> StatementContract stmt
- | Some (stmt, true) -> StatementAnnotation stmt
- in
- { Logic_deps.site; before=ctx.state_opt; kf=ctx.kf }
-
- let code_annot_filter = ref Logic_deps.code_annot_filter
-
- let from_term =
- ref (fun term ctx -> Logic_deps.from_term term (adapt_ctx ctx))
- let from_terms =
- ref (fun terms ctx -> Logic_deps.from_terms terms (adapt_ctx ctx))
- let from_pred =
- ref (fun pred ctx -> Logic_deps.from_pred pred (adapt_ctx ctx))
- let from_preds =
- ref (fun preds ctx -> Logic_deps.from_preds preds (adapt_ctx ctx))
- let from_stmt_annot = ref Logic_deps.from_stmt_annot
- let from_stmt_annots = ref Logic_deps.from_stmt_annots
- let from_func_annots = ref Logic_deps.from_func_annots
-
- let from_zone : (identified_term -> t_ctx -> t_zone_info * t_decl) ref =
- mk_fun "Interp.To_zone.from_zone"
- end
-
- let to_result_from_pred = ref Logic_deps.to_result_from_pred;
- end
-
-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 f342bf670dc..16a3b015d7f 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -527,202 +527,6 @@ end
"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 Properties} *)
-(* ************************************************************************* *)
-
-(** Dealing with logical properties.
- @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
-module Properties : sig
-
- (** Interpretation of logic terms. *)
- module Interp : sig
-
- (** {3 Parsing logic terms and annotations} *)
-
- (** For the three functions below, [env] can be used to specify which
- logic labels are parsed. By default, only [Here] is accepted. All
- the C labels inside the function are also accepted, regardless of
- [env]. [loc] is used as the source for the beginning of the string.
- All three functions may raise {!Logic_interp.Error} or
- {!Parsing.Parse_error}. *)
-
- val term_lval :
- (kernel_function -> ?loc:location -> ?env:Logic_typing.Lenv.t -> string ->
- Cil_types.term_lval) ref
- val term :
- (kernel_function -> ?loc:location -> ?env:Logic_typing.Lenv.t -> string ->
- Cil_types.term) ref
- val predicate :
- (kernel_function -> ?loc:location -> ?env:Logic_typing.Lenv.t -> string ->
- Cil_types.predicate) ref
-
- val code_annot : (kernel_function -> stmt -> string -> code_annotation) ref
-
-
- (** {3 From logic terms to C terms} *)
-
- (** Exception raised by the functions below when their given argument
- cannot be interpreted in the C world.
- @since Aluminium-20160501
- *)
- exception No_conversion
-
- val term_lval_to_lval:
- (result: Cil_types.varinfo option -> term_lval -> Cil_types.lval) ref
- (** @raise No_conversion if the argument is not a left value. *)
-
- val term_to_lval:
- (result: Cil_types.varinfo option -> term -> Cil_types.lval) ref
- (** @raise No_conversion if the argument is not a left value. *)
-
- val term_to_exp:
- (result: Cil_types.varinfo option -> term -> Cil_types.exp) ref
- (** @raise No_conversion if the argument is not a valid expression. *)
-
- val loc_to_exp:
- (result: Cil_types.varinfo option -> term -> Cil_types.exp list) ref
- (** @return a list of C expressions.
- @raise No_conversion if the argument is not a valid set of
- expressions. *)
-
- val loc_to_lval:
- (result: Cil_types.varinfo option -> term -> Cil_types.lval list) ref
- (** @return a list of C locations.
- @raise No_conversion if the argument is not a valid set of
- left values. *)
-
- val term_offset_to_offset:
- (result: Cil_types.varinfo option -> term_offset -> offset) ref
- (** @raise No_conversion if the argument is not a valid offset. *)
-
- val loc_to_offset:
- (result: Cil_types.varinfo option -> term -> Cil_types.offset list) ref
- (** @return a list of C offset provided the term denotes locations who
- have all the same base address.
- @raise No_conversion if the given term does not match the precondition *)
-
-
- (** {3 From logic terms to Locations.location} *)
-
- val loc_to_loc:
- (result: Cil_types.varinfo option -> Cvalue.Model.t -> term ->
- Locations.location) ref
- (** @raise No_conversion if the translation fails. *)
-
- val loc_to_loc_under_over:
- (result: Cil_types.varinfo option -> Cvalue.Model.t -> term ->
- Locations.location * Locations.location * Locations.Zone.t) ref
- (** Same as {!loc_to_loc}, except that we return simultaneously an
- under-approximation of the term (first location), and an
- over-approximation (second location). The under-approximation
- is particularly useful when evaluating Tsets. The zone returned is an
- over-approximation of locations that have been read during evaluation.
- Warning: This API is not stabilized, and may change in
- the future.
- @raise No_conversion if the translation fails.
- *)
-
- (** {3 From logic terms to Zone.t} *)
-
- module To_zone : sig
- type t_ctx =
- {state_opt:bool option;
- ki_opt:(stmt * bool) option;
- kf:Kernel_function.t}
-
- val mk_ctx_func_contrat:
- (kernel_function -> state_opt:bool option -> t_ctx) ref
- (** To build an interpretation context relative to function
- contracts. *)
-
- val mk_ctx_stmt_contrat:
- (kernel_function -> stmt -> state_opt:bool option -> t_ctx) ref
- (** To build an interpretation context relative to statement
- contracts. *)
-
- val mk_ctx_stmt_annot:
- (kernel_function -> stmt -> t_ctx) ref
- (** To build an interpretation context relative to statement
- annotations. *)
-
- type t = Logic_deps.t =
- {before:bool ;
- ki:stmt ; zone:Locations.Zone.t}
- type t_zone_info = (t list) option
- (** list of zones at some program points.
- * None means that the computation has failed. *)
-
- type t_decl = Logic_deps.decl =
- {var: Varinfo.Set.t ; (* related to vars of the annot *)
- lbl: Logic_label.Set.t} (* related to labels of the annot *)
- type t_pragmas = Logic_deps.pragmas =
- {ctrl: Stmt.Set.t ; (* related to //@ slice pragma ctrl/expr *)
- stmt: Stmt.Set.t} (* related to statement assign and
- //@ slice pragma stmt *)
-
- val from_term: (term -> t_ctx -> t_zone_info * t_decl) ref
- (** Entry point to get zones needed to evaluate the [term] relative to
- the [ctx] of interpretation. *)
-
- val from_terms: (term list -> t_ctx -> t_zone_info * t_decl) ref
- (** Entry point to get zones needed to evaluate the list of [terms]
- relative to the [ctx] of interpretation. *)
-
- val from_pred: (predicate -> t_ctx -> t_zone_info * t_decl) ref
- (** Entry point to get zones needed to evaluate the [predicate]
- relative to the [ctx] of interpretation. *)
-
- val from_preds: (predicate list -> t_ctx -> t_zone_info * t_decl) ref
- (** Entry point to get zones needed to evaluate the list of
- [predicates] relative to the [ctx] of interpretation. *)
-
- val from_zone: (identified_term -> t_ctx -> t_zone_info * t_decl) ref
- (** Entry point to get zones needed to evaluate the [zone] relative to
- the [ctx] of interpretation. *)
-
- val from_stmt_annot:
- (code_annotation -> stmt * kernel_function
- -> (t_zone_info * t_decl) * t_pragmas) ref
- (** Entry point to get zones needed to evaluate an annotation on the
- given stmt. *)
-
- val from_stmt_annots:
- ((code_annotation -> bool) option ->
- stmt * kernel_function -> (t_zone_info * t_decl) * t_pragmas) ref
- (** Entry point to get zones needed to evaluate annotations of this
- [stmt]. *)
-
- val from_func_annots:
- (((stmt -> unit) -> kernel_function -> unit) ->
- (code_annotation -> bool) option ->
- kernel_function -> (t_zone_info * t_decl) * t_pragmas) ref
- (** Entry point to get zones
- needed to evaluate annotations of this [kf]. *)
-
- val code_annot_filter:
- (code_annotation ->
- threat:bool -> user_assert:bool -> slicing_pragma:bool ->
- loop_inv:bool -> loop_var:bool -> others:bool -> bool) ref
- (** To quickly build an annotation filter *)
-
- end
-
- (** Does the interpretation of the predicate rely on the interpretation
- of the term result?
- @since Carbon-20110201 *)
- val to_result_from_pred:
- (predicate -> bool) ref
-
-
- end
-
-end
-[@@alert db_deprecated
- "Db.Properties is deprecated and will be removed in a future version \
- of Frama-C. Please use the Logic_to_c, Logic_deps or Logic_parse_string
- instead."]
-
(* ************************************************************************* *)
(** {2 Plugins} *)
(* ************************************************************************* *)
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 98ba5bc8f5f..b256b6c2546 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -2774,31 +2774,3 @@ let eval_tlval_as_zone ~alarm_mode access env t =
over
let tlval_deps env t = (eval_term_as_lval ~alarm_mode:Ignore env t).ldeps
-
-
-[@@@alert "-db_deprecated"]
-let () =
- (* TODO: deprecate loc_to_loc, move loc_to_locs into Value *)
- Db.Properties.Interp.loc_to_loc :=
- (fun ~result state t ->
- let env = env_post_f ~pre:state ~post:state ~result () in
- try eval_tlval_as_location ~alarm_mode:Ignore env t
- with LogicEvalError _ -> raise Logic_to_c.No_conversion
- );
- (* TODO: specify better evaluation environment *)
- Db.Properties.Interp.loc_to_loc_under_over :=
- (fun ~result state t ->
- let env = env_post_f ~pre:state ~post:state ~result () in
- try
- let r= eval_term_as_lval ~alarm_mode:Ignore env t in
- let s = Eval_typ.sizeof_lval_typ r.etype in
- make_loc r.eunder s, make_loc r.eover s, deps_at lbl_here r.ldeps
- with LogicEvalError _ -> raise Logic_to_c.No_conversion
- );
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../../.."
-End:
-*)
--
GitLab