[kernel] Move Logic_interp.To_zone to Logic_deps

src/kernel_services/analysis/logic_deps.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2022                                               *)
+(*    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
+open Cil_types
+open Cil_datatype
+
+exception NYI of string
+let not_yet_implemented = ref ""
+
+(** [compute_term_deps] is provided by Eva; computes the memory zone on which a
+    term depends. *)
+let compute_term_deps = ref (fun _stmt _expr -> None)
+
+(* Reimport here the type definitions of Db.Properties.Interp. See
+    documentation there. *)
+type ctx = Db.Properties.Interp.To_zone.t_ctx =
+  {state_opt:bool option;
+   ki_opt:(stmt * bool) option;
+   kf:Kernel_function.t}
+
+type pragmas = Db.Properties.Interp.To_zone.t_pragmas =
+  {ctrl: Stmt.Set.t ; stmt: Stmt.Set.t}
+
+type t = Db.Properties.Interp.To_zone.t
+= {before:bool ; ki:stmt ; zone:Locations.Zone.t}
+type zone_info = Db.Properties.Interp.To_zone.t_zone_info
+
+type decl = Db.Properties.Interp.To_zone.t_decl =
+  {var: Varinfo.Set.t ; lbl: Logic_label.Set.t}
+
+let mk_ctx_func_contrat kf ~state_opt =
+  { state_opt = state_opt;
+    ki_opt = None;
+    kf = kf }
+
+let mk_ctx_stmt_contrat kf ki ~state_opt =
+  { state_opt=state_opt;
+    ki_opt= Some(ki, false);
+    kf = kf }
+
+let mk_ctx_stmt_annot kf ki =
+  { state_opt = Some true;
+    ki_opt = Some(ki, true);
+    kf = kf }
+
+type result = {
+  pragmas: pragmas;
+  locals: Varinfo.Set.t;
+  labels: Logic_label.Set.t;
+  zones: (Locations.Zone.t * Locations.Zone.t) Stmt.Map.t option;
+}
+
+let empty_pragmas =
+  { ctrl = Stmt.Set.empty;
+    stmt = Stmt.Set.empty }
+
+let empty_results = {
+  pragmas = empty_pragmas;
+  locals = Varinfo.Set.empty;
+  labels = Logic_label.Set.empty;
+  zones = Some Stmt.Map.empty;
+}
+
+let add_top_zone not_yet_implemented_msg =
+  function
+  | None -> (* top zone *) None
+  | Some _ ->
+    not_yet_implemented := not_yet_implemented_msg;
+    None
+
+let add_zone ~before ki zone =
+  function
+  | None -> (* top zone *) None
+  | Some other_zones ->
+    let zone_true, zone_false =
+      try Stmt.Map.find ki other_zones
+      with Not_found -> Locations.Zone.bottom, Locations.Zone.bottom
+    in
+    let new_zone =
+      if before
+      then Locations.Zone.join zone_true zone, zone_false
+      else zone_true, Locations.Zone.join zone_false zone
+    in
+    Some (Stmt.Map.add ki new_zone other_zones)
+
+let get_result result =
+  let zones =
+    match result.zones with
+    | None -> None
+    | Some other_zones ->
+      let zones =
+        Stmt.Map.to_seq other_zones |>
+        Seq.flat_map (fun (ki, (zone_true, zone_false)) ->
+            List.to_seq [
+              { before=false; ki; zone=zone_false } ;
+              { before=true; ki; zone=zone_true }
+            ]) |>
+        Seq.filter (fun x ->
+            not (Locations.Zone.equal Locations.Zone.bottom x.zone)) |>
+        List.of_seq
+      in
+      Some zones
+  in
+  zones, {var = result.locals; lbl = result.labels}
+
+let get_annot_result result =
+  get_result result, result.pragmas
+
+(** Logic_var utility: *)
+let extract_locals logicvars =
+  Logic_var.Set.fold
+    (fun lv cvars -> match lv.lv_origin with
+       | None -> cvars
+       | Some cvar ->
+         if cvar.Cil_types.vglob then cvars
+         else Varinfo.Set.add cvar cvars)
+    logicvars
+    Varinfo.Set.empty
+
+(** Term utility:
+    Extract C local variables occurring into a [term]. *)
+let extract_locals_from_term term =
+  extract_locals (extract_free_logicvars_from_term term)
+
+(** Predicate utility:
+    Extract C local variables occurring into a [term]. *)
+let extract_locals_from_pred pred =
+  extract_locals (extract_free_logicvars_from_predicate pred)
+
+type abs_label = | AbsLabel_here
+                 | AbsLabel_pre
+                 | AbsLabel_post
+                 | AbsLabel_init
+                 | AbsLabel_loop_entry
+                 | AbsLabel_loop_current
+                 | AbsLabel_stmt of stmt
+
+let is_same_label absl l =
+  match absl, l with
+  | AbsLabel_stmt s1, StmtLabel s2 -> Cil_datatype.Stmt.equal s1 !s2
+  | AbsLabel_here, BuiltinLabel Here -> true
+  | AbsLabel_pre, BuiltinLabel Pre -> true
+  | AbsLabel_post, BuiltinLabel Post -> true
+  | AbsLabel_init, BuiltinLabel Init -> true
+  | AbsLabel_loop_entry, BuiltinLabel LoopEntry -> true
+  | AbsLabel_loop_current, BuiltinLabel LoopCurrent -> true
+  | _, (StmtLabel _ | FormalLabel _ | BuiltinLabel _) -> false
+
+
+let populate_zone ctx visit cil_node current_zones =
+  let { state_opt=before_opt; ki_opt; kf } = ctx in
+  (* interpretation from the
+     - pre-state if  [before_opt=Some true]
+     - post-state if [before_opt=Some false]
+     - pre-state with possible reference to the post-state if
+        [before_opt=None] of a property relative to
+     - the contract of function [kf] when [ki_opt=None]
+        otherwise [ki_opt=Some(ki, code_annot)],
+     - the contract of the statement [ki] when [code_annot=false]
+     - the annotation of the statement [ki] when [code_annot=true] *)
+  let vis = object(self)
+    inherit Visitor.frama_c_inplace
+    val mutable current_label = AbsLabel_here
+    val mutable zones = current_zones
+    method get_zones = zones
+
+    method private get_ctrl_point () =
+      let get_fct_entry_point () =
+        (* TODO: to replace by true, None *)
+        true,
+        (try Some (Kernel_function.find_first_stmt kf)
+         with Kernel_function.No_Statement ->
+           (* raised when [kf] has no code. *)
+           None)
+      in
+      let get_ctrl_point dft =
+        let before = Option.value ~default:dft before_opt in
+        match ki_opt with
+        | None -> (* function contract *)
+
+          if before then get_fct_entry_point ()
+          else before, None
+        (* statement contract *)
+        | Some (ki,_) ->  (* statement contract and code annotation *)
+          before, Some ki
+      in
+      let result = match current_label with
+        | AbsLabel_stmt stmt -> true, Some stmt
+        | AbsLabel_pre -> get_fct_entry_point ()
+        | AbsLabel_here -> get_ctrl_point true
+        | AbsLabel_post -> get_ctrl_point false
+        | AbsLabel_init -> raise (NYI "[logic_interp] Init label")
+        | AbsLabel_loop_current ->
+          raise (NYI "[logic_interp] LoopCurrent label")
+        | AbsLabel_loop_entry ->
+          raise (NYI "[logic_interp] LoopEntry label")
+      in (* TODO: the method should be able to return result directly *)
+      match result with
+      | current_before, Some current_stmt -> current_before, current_stmt
+      | _ -> raise (NYI
+                      "[logic_interp] clause related to a function contract")
+
+    method private change_label: 'a.abs_label -> 'a -> 'a visitAction =
+      fun label x ->
+      let old_label = current_label in
+      current_label <- label;
+      ChangeDoChildrenPost
+        (x,fun x -> current_label <- old_label; x)
+
+    method private change_label_to_here: 'a.'a -> 'a visitAction =
+      fun x ->
+      self#change_label AbsLabel_here x
+
+    method private change_label_to_old: 'a.'a -> 'a visitAction =
+      fun x ->
+      match ki_opt,before_opt with
+      (* function contract *)
+      | None,Some true ->
+        failwith "The use of the label Old is forbidden inside clauses \
+                  related to the pre-state of function contracts."
+      | None,None
+      | None,Some false ->
+        (* refers to the pre-state of the contract. *)
+        self#change_label AbsLabel_pre x
+      (* statement contract *)
+      | Some (_ki,false),Some true  ->
+        failwith "The use of the label Old is forbidden inside clauses \
+                  related to the pre-state of statement contracts."
+      | Some (ki,false),None
+      | Some (ki,false),Some false  ->
+        (* refers to the pre-state of the contract. *)
+        self#change_label (AbsLabel_stmt ki) x
+      (* code annotation *)
+      | Some (_ki,true),None
+      | Some (_ki,true),Some _ ->
+        (* refers to the pre-state of the function contract. *)
+        self#change_label AbsLabel_pre x
+
+    method private change_label_to_post: 'a.'a -> 'a visitAction =
+      fun x ->
+      (* allowed when [before_opt=None] for function/statement contracts *)
+      match ki_opt,before_opt with
+      (* function contract *)
+      | None,Some _ ->
+        failwith "Function contract where the use of the label Post is \
+                  forbidden."
+      | None,None ->
+        (* refers to the post-state of the contract. *)
+        self#change_label AbsLabel_post x
+      (* statement contract *)
+      | Some (_ki,false),Some _  ->
+        failwith "Statement contract where the use of the label Post is \
+                  forbidden."
+      | Some (_ki,false),None ->
+        (* refers to the pre-state of the contract. *)
+        self#change_label AbsLabel_post x
+      (* code annotation *)
+      | Some (_ki,true), _ ->
+        failwith "The use of the label Post is forbidden inside code \
+                  annotations."
+
+    method private change_label_to_pre: 'a.'a -> 'a visitAction =
+      fun x ->
+      match ki_opt with
+      (* function contract *)
+      | None ->
+        failwith "The use of the label Pre is forbidden inside function \
+                  contracts."
+      (* statement contract *)
+      (* code annotation *)
+      | Some _ ->
+        (* refers to the pre-state of the function contract. *)
+        self#change_label AbsLabel_pre x
+
+    method private change_label_aux: 'a. _ -> 'a -> 'a visitAction =
+      fun lbl x -> self#change_label lbl x
+
+    method private change_label_to_stmt: 'a.stmt -> 'a -> 'a visitAction =
+      fun stmt x ->
+      match ki_opt with
+      (* function contract *)
+      | None ->
+        failwith "the use of C labels is forbidden inside clauses related \
+                  to function contracts."
+      (* statement contract *)
+      (* code annotation *)
+      | Some _ ->
+        (* refers to the state at the C label of the statement [stmt]. *)
+        self#change_label (AbsLabel_stmt stmt) x
+
+
+    method! vpredicate_node p =
+      let fail () =
+        raise (NYI (Format.asprintf
+                      "[logic_interp] %a" Printer.pp_predicate_node p))
+      in
+      match p with
+      | Pat (_, BuiltinLabel Old) -> self#change_label_to_old p
+      | Pat (_, BuiltinLabel Here) -> self#change_label_to_here p
+      | Pat (_, BuiltinLabel Pre) -> self#change_label_to_pre p
+      | Pat (_, BuiltinLabel Post) -> self#change_label_to_post p
+      | Pat (_, BuiltinLabel Init) ->
+        self#change_label_aux AbsLabel_init p
+      | Pat (_, BuiltinLabel LoopCurrent) ->
+        self#change_label_aux AbsLabel_loop_current p
+      | Pat (_, BuiltinLabel LoopEntry) ->
+        self#change_label_aux AbsLabel_loop_entry p
+      | Pat (_, FormalLabel s) ->
+        failwith ("unknown logic label" ^ s)
+      | Pat (_, StmtLabel st) -> self#change_label_to_stmt !st p
+      | Pfalse | Ptrue | Prel _ | Pand _ | Por _ | Pxor _ | Pimplies _
+      | Piff _ | Pnot _ | Pif _ | Plet _ | Pforall _ | Pexists _
+      | Papp (_, [], _) (* No label, thus cannot access memory *)
+      | Pseparated _ (* need only to preserve the values of each pointer *)
+        -> DoChildren
+
+      | Pinitialized (lbl, t) | Pdangling (lbl, t) ->
+        (* Dependencies of [\initialized(p)] or [\dangling(p)] are the
+            dependencies of [*p]. *)
+        if is_same_label current_label lbl then (
+          let typ = Logic_typing.type_of_pointed t.term_type in
+          let tlv = Cil.mkTermMem ~addr:t ~off:TNoOffset in
+          let tlv' = Logic_const.term (TLval tlv) typ in
+          self#do_term_lval tlv';
+          DoChildren
+        )
+        else fail ()
+
+      | Pvalid_read (_lbl, _) | Pvalid (_lbl, _) ->
+        (* Does not take dynamic allocation into account, but then
+            Value does not either. [lbl] can be ignored because they are
+            taken into account by the functions [from_...] below *)
+        DoChildren
+
+      | Pobject_pointer _ | Pvalid_function _ ->
+        DoChildren
+
+      | Papp _ | Pallocable _ | Pfreeable _ | Pfresh _
+        -> fail ()
+
+    method private do_term_lval t =
+      let current_before, current_stmt = self#get_ctrl_point () in
+      match !compute_term_deps current_stmt t with
+      | Some zone ->
+        let filter = function Base.CLogic_Var _ -> false | _ -> true in
+        let zone = Locations.Zone.filter_base filter zone in
+        zones <- add_zone ~before:current_before current_stmt zone zones
+      | None ->
+        raise (NYI "[logic_interp] dependencies of a term lval")
+
+    method! vterm t =
+      match t.term_node with
+      | TAddrOf _ | TLval (TMem _,_)
+      | TLval(TVar {lv_origin = Some _},_) | TStartOf _  ->
+        self#do_term_lval t;
+        SkipChildren
+      | Tat (_, BuiltinLabel Old) -> self#change_label_to_old t
+      | Tat (_, BuiltinLabel Here) -> self#change_label_to_here t
+      | Tat (_, BuiltinLabel Pre) -> self#change_label_to_pre t
+      | Tat (_, BuiltinLabel Post) -> self#change_label_to_post t
+      | Tat (_, BuiltinLabel Init) ->
+        self#change_label_aux AbsLabel_init t
+      | Tat (_, BuiltinLabel LoopCurrent) ->
+        self#change_label_aux AbsLabel_loop_current t
+      | Tat (_, BuiltinLabel LoopEntry) ->
+        self#change_label_aux AbsLabel_loop_entry t
+      | Tat (_, StmtLabel st) -> self#change_label_to_stmt !st t
+      | Tat (_, FormalLabel s) ->
+        failwith ("unknown logic label" ^ s)
+      | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _ | TAlignOfE _ ->
+        (* These are static constructors, there are no dependencies here *)
+        SkipChildren
+      | _ -> DoChildren
+  end
+  in
+  try
+    ignore (visit (vis :> Visitor.frama_c_inplace) cil_node);
+    vis#get_zones
+  with NYI msg ->
+    add_top_zone msg (vis#get_zones)
+
+let update_pragmas f results =
+  { results with pragmas = f results.pragmas }
+
+let add_ctrl_pragma stmt =
+  update_pragmas (fun x -> { x with ctrl = Stmt.Set.add stmt x.ctrl })
+
+let add_stmt_pragma stmt =
+  update_pragmas (fun x -> { x with stmt = Stmt.Set.add stmt x.stmt })
+
+let add_results_from_term ctx results t =
+  let zones = populate_zone ctx Visitor.visitFramacTerm t results.zones in
+  {
+    results with
+    zones;
+    locals = Varinfo.Set.union (extract_locals_from_term t) results.locals;
+    labels = Logic_label.Set.union (extract_labels_from_term t) results.labels
+  }
+
+let add_results_from_pred ctx results p =
+  let zones = populate_zone ctx Visitor.visitFramacPredicate p results.zones in
+  {
+    results with
+    zones;
+    locals = Varinfo.Set.union (extract_locals_from_pred p) results.locals;
+    labels = Logic_label.Set.union (extract_labels_from_pred p) results.labels
+  }
+
+(** Entry point to get the list of [ki] * [Locations.Zone.t]
+    needed to evaluate the list of [terms]
+    relative to the [ctx] of interpretation. *)
+let from_terms terms ctx =
+  List.fold_left (add_results_from_term ctx) empty_results terms |>
+  get_result
+
+(** Entry point to get the list of [ki] * [Locations.Zone.t]
+    needed to evaluate the [term]
+    relative to the [ctx] of interpretation. *)
+let from_term term ctx =
+  add_results_from_term ctx empty_results term |>
+  get_result
+
+(** Entry point to get the list of [ki] * [Locations.Zone.t]
+    needed to evaluate the list of [preds]
+    relative to the [ctx] of interpretation. *)
+let from_preds preds ctx =
+  List.fold_left (add_results_from_pred ctx) empty_results preds |>
+  get_result
+
+(** Entry point to get the list of [ki] * [Locations.Zone.t]
+    needed to evaluate the [pred]
+    relative to the [ctx] of interpretation. *)
+let from_pred pred ctx =
+  add_results_from_pred ctx empty_results pred |>
+  get_result
+
+(** Used by annotations entry points. *)
+let get_zone_from_annot a (ki,kf) loop_body_opt results =
+  let get_zone_from_term k term results =
+    let ctx = { state_opt = Some true; ki_opt = Some (k, true); kf } in
+    add_results_from_term ctx results term
+  and get_zone_from_pred k pred results =
+    let ctx = { state_opt = Some true; ki_opt = Some (k, true); kf } in
+    add_results_from_pred ctx results pred
+  in
+  match a.annot_content with
+  | APragma (Slice_pragma (SPexpr term) | Impact_pragma (IPexpr term)) ->
+    results |>
+    (* to preserve the interpretation of the pragma *)
+    get_zone_from_term ki term |>
+    (* to select the reachability of the pragma *)
+    add_ctrl_pragma ki
+  | APragma (Slice_pragma SPctrl) ->
+    (* to select the reachability of the pragma *)
+    add_ctrl_pragma ki results
+  | APragma (Slice_pragma SPstmt | Impact_pragma IPstmt) ->
+    (* to preserve the effect of the statement *)
+    add_stmt_pragma ki results
+  | AAssert (_behav,pred) ->
+    (* to preserve the interpretation of the assertion *)
+    get_zone_from_pred ki pred.tp_statement results
+  | AInvariant (_behav,true,pred) -> (* loop invariant *)
+    (* WARNING this is obsolete *)
+    (* [JS 2010/09/02] TODO: so what is the right way to do? *)
+    (* to preserve the interpretation of the loop invariant *)
+    get_zone_from_pred (Option.get loop_body_opt) pred.tp_statement results
+  | AInvariant (_behav,false,pred) -> (* code invariant *)
+    (* to preserve the interpretation of the code invariant *)
+    get_zone_from_pred ki pred.tp_statement results
+  | AVariant (term,_) ->
+    (* to preserve the interpretation of the variant *)
+    get_zone_from_term (Option.get loop_body_opt) term results
+  | APragma (Loop_pragma (Unroll_specs terms))
+  | APragma (Loop_pragma (Widen_hints terms))
+  | APragma (Loop_pragma (Widen_variables terms)) ->
+    (* to select the declaration of the variables *)
+    List.fold_left
+      (fun results term -> {
+           results with
+           locals = Varinfo.Set.union (extract_locals_from_term term) results.locals;
+           labels = Logic_label.Set.union (extract_labels_from_term term) results.labels
+         })
+      results terms
+  | AAllocation (_,FreeAllocAny) -> results
+  | AAllocation (_,FreeAlloc(f,a)) ->
+    let get_zone results x =
+      get_zone_from_term (Option.get loop_body_opt) x.it_content results
+    in
+    let results = List.fold_left get_zone results f in
+    let results = List.fold_left get_zone results a in
+    results
+  | AAssigns (_, WritesAny) -> results
+  | AAssigns (_, Writes l) -> (* loop assigns *)
+    let get_zone results x =
+      get_zone_from_term (Option.get loop_body_opt) x.it_content results
+    in
+    List.fold_left
+      (fun results (zone,deps) ->
+         let results = get_zone results zone in
+         match deps with
+           FromAny -> results
+         | From l -> List.fold_left get_zone results l)
+      results l
+  | AStmtSpec _ -> (* TODO *)
+    raise (NYI "[logic_interp] statement contract")
+  | AExtended _ -> raise (NYI "[logic_interp] extension")
+
+(* Used by annotations entry points. *)
+let get_from_stmt_annots code_annot_filter ((ki, _kf) as stmt) results =
+  Option.fold
+    ~none:results
+    ~some:(fun caf ->
+        let loop_body_opt = match ki.skind with
+          | Loop(_, { bstmts = body :: _ }, _, _, _) -> Some body
+          | _ -> None
+        in
+        Annotations.fold_code_annot
+          (fun _ a results ->
+             if caf a
+             then get_zone_from_annot a stmt loop_body_opt results
+             else results)
+          ki results)
+    code_annot_filter
+
+(** Used by annotations entry points. *)
+let from_ki_annot annot ((ki, _kf) as stmt) =
+  let real_ki = match ki.skind with
+      Loop(_,{bstmts = loop_entry::_},_,_,_) -> Some loop_entry
+    | _ -> None
+  in
+  get_zone_from_annot annot stmt real_ki
+
+(** Entry point to get the list of [ki] * [Locations.Zone.t]
+    needed to evaluate the code annotations related to this [stmt]. *)
+let from_stmt_annot annot stmt =
+  from_ki_annot annot stmt empty_results |>
+  get_annot_result
+
+(** Entry point to get the list of [ki] * [Locations.Zone.t]
+    needed to evaluate the code annotations related to this [stmt]. *)
+let from_stmt_annots code_annot_filter stmt =
+  get_from_stmt_annots code_annot_filter stmt empty_results |>
+  get_annot_result
+
+(** Entry point to get the list of [ki] * [Locations.Zone.t]
+    needed to evaluate the code annotations related to this [kf]. *)
+let from_func_annots iter_on_kf_stmt code_annot_filter kf =
+  let results = ref empty_results in
+  let from_stmt_annots ki =
+    results := get_from_stmt_annots code_annot_filter (ki, kf) !results
+  in
+  iter_on_kf_stmt from_stmt_annots kf;
+  get_annot_result !results
+
+(** To quickly build a annotation filter *)
+let code_annot_filter annot ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop_var ~others =
+  match annot.annot_content with
+  | APragma (Slice_pragma _) -> slicing_pragma
+  | AAssert _ ->
+    (match Alarms.find annot with
+     | None -> user_assert
+     | Some _a -> threat)
+  | AVariant _ -> loop_var
+  | AInvariant(_behav,true,_pred) -> loop_inv
+  | AInvariant(_,false,_) -> others
+  | AAllocation _ -> others
+  | AAssigns _ -> others
+  | APragma (Loop_pragma _)| APragma (Impact_pragma _) -> others
+  | AStmtSpec _  | AExtended _ (* TODO *) -> false
+
+
+exception Prune
+
+let to_result_from_pred p =
+  let visitor = object (_self)
+    inherit Visitor.frama_c_inplace
+
+    method! vterm_lhost t =
+      match t with
+      | TResult _ -> raise Prune
+      | _ -> DoChildren
+
+  end
+  in
+  (try
+     ignore(Visitor.visitFramacPredicate visitor p);
+     false
+   with Prune ->
+     true)
+
+
+let () =
+  Db.Properties.Interp.To_zone.code_annot_filter := code_annot_filter;
+  Db.Properties.Interp.To_zone.mk_ctx_func_contrat := mk_ctx_func_contrat;
+  Db.Properties.Interp.To_zone.mk_ctx_stmt_contrat := mk_ctx_stmt_contrat;
+  Db.Properties.Interp.To_zone.mk_ctx_stmt_annot := mk_ctx_stmt_annot;
+
+  Db.Properties.Interp.To_zone.from_term := from_term;
+  Db.Properties.Interp.To_zone.from_terms := from_terms;
+  Db.Properties.Interp.To_zone.from_pred := from_pred;
+  Db.Properties.Interp.To_zone.from_preds := from_preds;
+  Db.Properties.Interp.To_zone.from_stmt_annot := from_stmt_annot;
+  Db.Properties.Interp.To_zone.from_stmt_annots := from_stmt_annots;
+  Db.Properties.Interp.To_zone.from_func_annots := from_func_annots;
+
+  Db.Properties.Interp.to_result_from_pred := to_result_from_pred;

src/kernel_services/analysis/logic_deps.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2022                                               *)
+(*    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
+
+val compute_term_deps: (stmt -> term -> Locations.Zone.t option) ref
+
+type ctx = Db.Properties.Interp.To_zone.t_ctx
+
+val mk_ctx_func_contrat: kernel_function -> state_opt:bool option -> ctx
+(** To build an interpretation context relative to function
+    contracts. *)
+
+val mk_ctx_stmt_contrat: kernel_function -> stmt -> state_opt:bool option -> ctx
+(** To build an interpretation context relative to statement
+    contracts. *)
+
+val mk_ctx_stmt_annot: kernel_function -> stmt -> ctx
+(** To build an interpretation context relative to statement
+    annotations. *)
+
+type t = Db.Properties.Interp.To_zone.t
+type zone_info = Db.Properties.Interp.To_zone.t_zone_info
+(** list of zones at some program points.
+ *   None means that the computation has failed. *)
+
+type decl = Db.Properties.Interp.To_zone.t_decl
+type pragmas = Db.Properties.Interp.To_zone.t_pragmas
+
+val from_term: term -> ctx -> zone_info * decl
+(** Entry point to get zones needed to evaluate the [term] relative to
+    the [ctx] of interpretation. *)
+
+val from_terms: term list -> ctx -> zone_info * decl
+(** Entry point to get zones needed to evaluate the list of [terms]
+    relative to the [ctx] of interpretation. *)
+
+val from_pred: predicate -> ctx -> zone_info * decl
+(** Entry point to get zones needed to evaluate the [predicate]
+    relative to the [ctx] of interpretation. *)
+
+val from_preds: predicate list -> ctx -> zone_info * decl
+(** Entry point to get zones needed to evaluate the list of
+    [predicates] relative to the [ctx] of interpretation. *)
+
+val from_stmt_annot:
+  code_annotation -> stmt * kernel_function ->
+  (zone_info * decl) * pragmas
+(** 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 -> (zone_info * decl) * pragmas
+(** 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 -> (zone_info * decl) * pragmas
+(** 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
+(** To quickly build an annotation filter *)
+
+(** Does the interpretation of the predicate rely on the interpretation
+    of the term result? *)
+val to_result_from_pred: predicate -> bool
+
+(** The follow declarations are kept for compatibility and should not be used *)
+exception NYI of string
+val not_yet_implemented: string ref

src/kernel_services/analysis/logic_interp.mli

@@ -20,12 +20,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* This module exists for compatibility only and will be removed in future
+   versions *)
+
 open Cil_types
 
 module To_zone : sig
   exception NYI of string
   val not_yet_implemented : string ref
-  val compute_term_deps: (stmt -> term -> Locations.Zone.t option) ref
 end
 
 exception [@alert deprecated "Use directly Logic_parse_string.Error istead."]

src/plugins/eva/legacy/logic_inout.ml

@@ -43,7 +43,7 @@ let compute_term_deps stmt t =
   let state = Results.(before stmt |> get_cvalue_model) in
   term_deps state t
 
-let () = Logic_interp.To_zone.compute_term_deps := compute_term_deps
+let () = Logic_deps.compute_term_deps := compute_term_deps
 
 let valid_behaviors kf state =
   let funspec = Annotations.funspec kf in