diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index b507afc33b78b757eed9dd5e30fdc08a7c12962b..6298b441abc8e3e4ca474f920061e1dd37532a6e 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -3726,8 +3726,9 @@ directly stored in the AST. These modules and functions are the following.
an ACSL annotation has to be converted into a property if you want to access
its property statuses.
\item Modules \texttt{Logic\_const}\codeidxdef{Logic\_const},
- \texttt{Logic\_utils}\codeidxdef{Logic\_utils} and
- \texttt{Db.Properties}\scodeidxdef{Db}{Properties} contain several
+ \texttt{Logic\_utils}\codeidxdef{Logic\_utils},
+ \texttt{Logic\_parse\_string}\codeidxdef{Logic\_parse\_string} and
+ \texttt{Logic\_to\_c}\codeidxdef{Logic\_to\_c}, contain several
operations over annotations.
\end{itemize}
diff --git a/src/kernel_services/analysis/logic_deps.ml b/src/kernel_services/analysis/logic_deps.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5f1598f76e7117cf8a83634ba2d44af5187cda47
--- /dev/null
+++ b/src/kernel_services/analysis/logic_deps.ml
@@ -0,0 +1,597 @@
+(**************************************************************************)
+(* *)
+(* 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)
+
+type ctx = {
+ site: ctx_site;
+ before: bool option;
+ kf: Kernel_function.t
+}
+
+and ctx_site =
+ | FunctionContract
+ | StatementContract of stmt
+ | StatementAnnotation of stmt
+
+type pragmas = {ctrl: Stmt.Set.t ; stmt: Stmt.Set.t}
+type t = {before:bool ; ki:stmt ; zone:Locations.Zone.t}
+type zone_info = (t list) option
+type decl = {var: Varinfo.Set.t ; lbl: Logic_label.Set.t}
+
+let mk_ctx_func_contract ?before kf =
+ { before; site=FunctionContract; kf }
+
+let mk_ctx_stmt_contract ?before kf stmt =
+ { before; site=StatementContract stmt; kf }
+
+let mk_ctx_stmt_annot kf stmt =
+ { before=Some true; site=StatementAnnotation stmt; 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 =
+ (* interpretation from the
+ - pre-state if [before=Some true]
+ - post-state if [before=Some false]
+ - pre-state with possible reference to the post-state if
+ [before=None] of a property relative to
+ - the contract of function [kf] when [side=FunctionContract]
+ - the contract of the statement [ki] when [site=StatementContract stmt]
+ - the annotation of the statement [ki] when [site=StatementAnnotation stmt] *)
+ 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 ctx.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 ctx.before in
+ match ctx.site with
+ | FunctionContract ->
+ if before then get_fct_entry_point ()
+ else before, None
+ (* statement contract *)
+ | StatementContract stmt | StatementAnnotation stmt -> (* statement contract and code annotation *)
+ before, Some stmt
+ 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 ctx.site, ctx.before with
+ (* function contract *)
+ | FunctionContract, Some true ->
+ failwith "The use of the label Old is forbidden inside clauses \
+ related to the pre-state of function contracts."
+ | FunctionContract, None
+ | FunctionContract, Some false ->
+ (* refers to the pre-state of the contract. *)
+ self#change_label AbsLabel_pre x
+ (* statement contract *)
+ | StatementContract _stmt, Some true ->
+ failwith "The use of the label Old is forbidden inside clauses \
+ related to the pre-state of statement contracts."
+ | StatementContract stmt, None
+ | StatementContract stmt, Some false ->
+ (* refers to the pre-state of the contract. *)
+ self#change_label (AbsLabel_stmt stmt) x
+ (* code annotation *)
+ | StatementAnnotation _stmt, _ ->
+ (* 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 ctx.site, ctx.before with
+ (* function contract *)
+ | FunctionContract, Some _ ->
+ failwith "Function contract where the use of the label Post is \
+ forbidden."
+ | FunctionContract, None ->
+ (* refers to the post-state of the contract. *)
+ self#change_label AbsLabel_post x
+ (* statement contract *)
+ | StatementContract _stmt, Some _ ->
+ failwith "Statement contract where the use of the label Post is \
+ forbidden."
+ | StatementContract _stmt,None ->
+ (* refers to the pre-state of the contract. *)
+ self#change_label AbsLabel_post x
+ (* code annotation *)
+ | StatementAnnotation _stmt, _ ->
+ 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 ctx.site with
+ (* function contract *)
+ | FunctionContract ->
+ failwith "The use of the label Pre is forbidden inside function \
+ contracts."
+ (* statement contract *)
+ (* code annotation *)
+ | StatementContract _ | StatementAnnotation _ ->
+ (* 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 ctx.site with
+ (* function contract *)
+ | FunctionContract ->
+ failwith "the use of C labels is forbidden inside clauses related \
+ to function contracts."
+ (* statement contract *)
+ (* code annotation *)
+ | StatementContract _ | StatementAnnotation _ ->
+ (* 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 = mk_ctx_stmt_annot kf k in
+ add_results_from_term ctx results term
+ and get_zone_from_pred k pred results =
+ let ctx = mk_ctx_stmt_annot kf k 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)
diff --git a/src/kernel_services/analysis/logic_deps.mli b/src/kernel_services/analysis/logic_deps.mli
new file mode 100644
index 0000000000000000000000000000000000000000..2a25e71b12cf111e880689779b9111fbf4299c00
--- /dev/null
+++ b/src/kernel_services/analysis/logic_deps.mli
@@ -0,0 +1,100 @@
+(**************************************************************************)
+(* *)
+(* 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
+
+val mk_ctx_func_contract: ?before:bool -> kernel_function -> ctx
+(** To build an interpretation context relative to function
+ contracts. *)
+
+val mk_ctx_stmt_contract: ?before:bool -> kernel_function -> stmt -> 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 = {before:bool ; ki:stmt ; zone:Locations.Zone.t}
+type zone_info = (t list) option
+(** list of zones at some program points.
+ * None means that the computation has failed. *)
+
+type decl = {var: Cil_datatype.Varinfo.Set.t ; (* related to vars of the annot *)
+ lbl: Cil_datatype.Logic_label.Set.t} (* related to labels of the annot *)
+type pragmas =
+ {ctrl: Cil_datatype.Stmt.Set.t ; (* related to //@ slice pragma ctrl/expr *)
+ stmt: Cil_datatype.Stmt.Set.t}
+
+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 following declarations are kept for compatibility and should not be
+ used *)
+exception NYI of string
+val not_yet_implemented: string ref
diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml
deleted file mode 100644
index e76accf2cc98f100b109ab0ff4523dc80bd797c2..0000000000000000000000000000000000000000
--- a/src/kernel_services/analysis/logic_interp.ml
+++ /dev/null
@@ -1,1110 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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 Error of Cil_types.location * string
-exception Unbound of string
-
-let find_var kf kinstr ?label var =
- let vi =
- try
- let vi = Globals.Vars.find_from_astinfo var (VLocal kf) in
- (match kinstr with
- | Kglobal -> vi (* don't refine search: the Kglobal here
- does not indicate the function contract, but merely
- the fact that we do not have any information about
- the targeted program point. Hence, no scope check
- can be performed or we might reject many legitimate
- terms and predicates.
- *)
- | Kstmt stmt ->
- let scope =
- match label with
- | None | Some "Here" | Some "Post" | Some "Old" -> stmt
- | Some "Pre" -> raise Not_found (* no local variable in scope. *)
- | Some "Init" -> raise Not_found (* no local variable in scope. *)
- | Some "LoopEntry" | Some "LoopCurrent" ->
- if not (Kernel_function.stmt_in_loop kf stmt) then
- Kernel.fatal
- "Use of LoopEntry or LoopCurrent outside of a loop";
- Kernel_function.find_enclosing_loop kf stmt
- | Some l ->
- (try let s = Kernel_function.find_label kf l in !s
- with Not_found ->
- Kernel.fatal
- "Use of label %s that does not exist in function %a"
- l Kernel_function.pretty kf)
- in
- if Kernel_function.var_is_in_scope scope vi then vi
- else raise Not_found)
- with Not_found ->
- try
- Globals.Vars.find_from_astinfo var (VFormal kf)
- with Not_found ->
- Globals.Vars.find_from_astinfo var VGlobal
- in
- cvar_to_lvar vi
-
-(** Create a logic typer, the interpretation being done for the given
- kernel_function and stmt (the stmt is used check that loop invariants
- are allowed). *)
-(* It is theoretically possible to use a first-class module instead, but the
- required signatures are not exported in Logic_typing. *)
-module DefaultLT (X:
- sig
- val kf: Kernel_function.t
- val kinstr: Cil_types.kinstr
- end) =
- Logic_typing.Make
- (struct
- let anonCompFieldName = Cabs2cil.anonCompFieldName
- let conditionalConversion = Cabs2cil.logicConditionalConversion
-
- let is_loop () =
- match X.kinstr with
- | Kglobal -> false
- | Kstmt s -> Kernel_function.stmt_in_loop X.kf s
-
- let find_macro _ = raise Not_found
-
- let find_var ?label var = find_var X.kf X.kinstr ?label var
-
- let find_enum_tag x =
- try
- Globals.Types.find_enum_tag x
- with Not_found ->
- (* The ACSL typer tries to parse a string, first as a variable,
- then as an enum. We report the "Unbound variable" message
- here, as it is nicer for the user. However, this short-circuits
- the later stages of resolution, for example global logic
- variables. *)
- raise (Unbound ("Unbound variable " ^ x))
-
- let find_comp_field info s =
- let field = Cil.getCompField info s in
- Field(field,NoOffset)
-
- let find_type = Globals.Types.find_type
-
- let find_label s = Kernel_function.find_label X.kf s
- include Logic_env
-
- let add_logic_function =
- add_logic_function_gen Logic_utils.is_same_logic_profile
-
- let remove_logic_info =
- remove_logic_info_gen Logic_utils.is_same_logic_profile
-
- let integral_cast ty t =
- raise
- (Failure
- (Format.asprintf
- "term %a has type %a, but %a is expected."
- Printer.pp_term t
- Printer.pp_logic_type Linteger
- Printer.pp_typ ty))
-
- let error loc msg =
- Pretty_utils.ksfprintf (fun e -> raise (Error (loc, e))) msg
-
- let on_error f rollback x =
- try f x with Error (loc,msg) as exn -> rollback (loc,msg); raise exn
-
- end)
-
-(** Set up the parser for the infamous 'C hack' needed to parse typedefs *)
-let sync_typedefs () =
- Logic_env.reset_typenames ();
- Globals.Types.iter_types
- (fun name _ ns ->
- if ns = Logic_typing.Typedef then Logic_env.add_typename name)
-
-let wrap f parsetree loc =
- match parsetree with
- | None -> raise (Error (loc, "Syntax error in annotation"))
- | Some annot -> try f annot with Unbound s -> raise (Error (loc, s))
-
-let code_annot kf stmt s =
- sync_typedefs ();
- let module LT = DefaultLT(struct
- let kf = kf
- let kinstr = Kstmt stmt
- end) in
- let loc = Stmt.loc stmt in
- let pa =
- Option.bind
- (Logic_lexer.annot (fst loc,s))
- (function (_, Logic_ptree.Acode_annot (_,a)) -> Some a | _ -> None)
- in
- let parse pa =
- LT.code_annot
- (Stmt.loc stmt)
- (Logic_utils.get_behavior_names (Annotations.funspec kf))
- (Ctype (Kernel_function.get_return_type kf)) pa
- in
- wrap parse pa loc
-
-let default_term_env () =
- Logic_typing.append_here_label (Logic_typing.Lenv.empty())
-
-let term kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
- sync_typedefs ();
- let module LT = DefaultLT(struct
- let kf = kf
- let kinstr = Kglobal
- end) in
- let pa_expr = Option.map snd (Logic_lexer.lexpr (fst loc, s)) in
- let parse pa_expr = LT.term env pa_expr in
- wrap parse pa_expr loc
-
-let term_lval kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
- match (term kf ~loc ~env s).term_node with
- | TLval lv -> lv
- | _ -> raise (Error (loc, "Syntax error (expecting an lvalue)"))
-
-let predicate kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
- sync_typedefs ();
- let module LT = DefaultLT(struct
- let kf = kf
- let kinstr = Kglobal
- end) in
- let pa_expr = Option.map snd (Logic_lexer.lexpr (fst loc, s)) in
- let parse pa_expr = LT.predicate env pa_expr in
- wrap parse pa_expr loc
-
-let error_lval () = raise Db.Properties.Interp.No_conversion
-
-let rec logic_type_to_typ = function
- | Ctype typ -> typ
- | Linteger -> TInt(ILongLong,[]) (*TODO: to have an unlimited integer type
- in the logic interpretation*)
- | Lreal -> TFloat(FDouble,[]) (* TODO: handle reals, not floats... *)
- | Ltype({lt_name = name},[]) when name = Utf8_logic.boolean ->
- TInt(ILongLong,[])
- | Ltype({lt_name = "set"},[t]) -> logic_type_to_typ t
- | Ltype _ | Lvar _ | Larrow _ -> error_lval ()
-
-
-(* Expect conversion to be possible on all sub-terms, otherwise raise an error. *)
-
-let logic_var_to_var { lv_origin = lv } =
- match lv with
- | None -> error_lval ()
- | Some lv -> lv
-
-let create_const_list loc kind low high =
- let rec aux acc i =
- if Integer.lt i low then acc
- else
- aux (new_exp ~loc (Const (CInt64 (i,kind,None)))::acc) (Integer.pred i)
- in aux [] high
-
-let range low high =
- let loc = fst low.eloc, snd high.eloc in
- match (Cil.constFold true low).enode, (Cil.constFold true high).enode with
- Const(CInt64(low,kind,_)), Const(CInt64(high,_,_)) ->
- create_const_list loc kind low high
- | _ -> error_lval()
-
-let singleton f loc =
- match f loc with
- [ l ] -> l
- | _ -> error_lval()
-
-let rec loc_lval_to_lval ~result (lh, lo) =
- Extlib.product
- (fun x y -> (x,y))
- (loc_lhost_to_lhost ~result lh)
- (loc_offset_to_offset ~result lo)
-
-and loc_lhost_to_lhost ~result = function
- | TVar lvar -> [Var (logic_var_to_var lvar)]
- | TMem lterm -> List.map (fun x -> Mem x) (loc_to_exp ~result lterm)
- | TResult _ ->
- ( match result with
- None -> error_lval()
- | Some v -> [Var v])
-
-and loc_offset_to_offset ~result = function
- | TNoOffset -> [NoOffset]
- | TModel _ -> error_lval ()
- | TField (fi, lo) ->
- List.map (fun x -> Field (fi,x)) (loc_offset_to_offset ~result lo)
- | TIndex (lexp, lo) ->
- Extlib.product
- (fun x y -> Index(x,y))
- (loc_to_exp ~result lexp)
- (loc_offset_to_offset ~result lo)
-
-and loc_to_exp ~result {term_node = lnode ; term_type = ltype; term_loc = loc} =
- match lnode with
- | TLval lv ->
- List.map (fun x -> new_exp ~loc (Lval x)) (loc_lval_to_lval ~result lv)
- | TAddrOf lv ->
- List.map (fun x -> new_exp ~loc (AddrOf x)) (loc_lval_to_lval ~result lv)
- | TStartOf lv ->
- List.map (fun x -> new_exp ~loc (StartOf x)) (loc_lval_to_lval ~result lv)
- | TSizeOfE lexp ->
- List.map (fun x -> new_exp ~loc (SizeOfE x)) (loc_to_exp ~result lexp)
- | TAlignOfE lexp ->
- List.map (fun x -> new_exp ~loc (AlignOfE x)) (loc_to_exp ~result lexp)
- | TUnOp (unop, lexp) ->
- List.map
- (fun x -> new_exp ~loc (UnOp (unop, x, logic_type_to_typ ltype)))
- (loc_to_exp ~result lexp)
- | TBinOp (binop, lexp1, lexp2) ->
- Extlib.product
- (fun x y -> new_exp ~loc (BinOp (binop, x,y, logic_type_to_typ ltype)))
- (loc_to_exp ~result lexp1)
- (loc_to_exp ~result lexp2)
- | TSizeOfStr string -> [new_exp ~loc (SizeOfStr string)]
- | TConst constant ->
- (* TODO: Very likely to fail on large integer and incorrect on reals not
- representable as floats *)
- [new_exp ~loc (Const (Logic_utils.lconstant_to_constant constant))]
- | TCastE (typ, lexp) ->
- List.map
- (fun x -> new_exp ~loc (CastE (typ, x))) (loc_to_exp ~result lexp)
- | TAlignOf typ -> [new_exp ~loc (AlignOf typ)]
- | TSizeOf typ -> [new_exp ~loc (SizeOf typ)]
- | Trange (Some low, Some high) ->
- let low = singleton (loc_to_exp ~result) low in
- let high = singleton (loc_to_exp ~result) high in
- range low high
- | Tunion l -> List.concat (List.map (loc_to_exp ~result) l)
- | Tempty_set -> []
- | Tinter _ | Tcomprehension _ -> error_lval()
- | Tat ({term_node = TAddrOf (TVar _, TNoOffset)} as taddroflval, _) ->
- loc_to_exp ~result taddroflval
- | TLogic_coerce(Linteger, t) when Logic_typing.is_integral_type t.term_type ->
- loc_to_exp ~result t
- | TLogic_coerce(Lreal, t) when Logic_typing.is_integral_type t.term_type ->
- List.map
- (fun x -> new_exp ~loc (CastE (logic_type_to_typ Lreal, x)))
- (loc_to_exp ~result t)
- | TLogic_coerce(Lreal, t) when Logic_typing.is_arithmetic_type t.term_type ->
- loc_to_exp ~result t
- | TLogic_coerce (set, t)
- when
- Logic_const.is_set_type set &&
- Logic_utils.is_same_type
- (Logic_typing.type_of_set_elem set) t.term_type ->
- loc_to_exp ~result t
- | Tnull -> [ Cil.mkCast ~newt:(TPtr(TVoid [], [])) (Cil.zero ~loc) ]
-
- (* additional constructs *)
- | Tapp _ | Tlambda _ | Trange _ | Tlet _
- | TDataCons _
- | Tif _
- | Tat _
- | Tbase_addr _
- | Toffset _
- | Tblock_length _
- | TUpdate _ | Ttypeof _ | Ttype _
- | TLogic_coerce _
- -> error_lval ()
-
-let rec loc_to_lval ~result t =
- match t.term_node with
- | TLval lv -> loc_lval_to_lval ~result lv
- | TAddrOf lv -> loc_lval_to_lval ~result lv
- | TStartOf lv -> loc_lval_to_lval ~result lv
- | Tunion l1 -> List.concat (List.map (loc_to_lval ~result) l1)
- | Tempty_set -> []
- (* coercions to arithmetic types cannot be lval. We only have to consider
- a coercion to set here.
- *)
- | TLogic_coerce(set, t) when
- Logic_typing.is_set_type set &&
- Logic_utils.is_same_type
- (Logic_typing.type_of_set_elem set) t.term_type ->
- loc_to_lval ~result t
- | Tinter _ -> error_lval() (* TODO *)
- | Tcomprehension _ -> error_lval()
- | TSizeOfE _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TSizeOfStr _
- | TConst _ | TCastE _ | TAlignOf _ | TSizeOf _ | Tapp _ | Tif _
- | Tat _ | Toffset _ | Tbase_addr _ | Tblock_length _ | Tnull | Trange _
- | TDataCons _ | TUpdate _ | Tlambda _
- | Ttypeof _ | Ttype _ | Tlet _ | TLogic_coerce _ ->
- error_lval ()
-
-let loc_to_offset ~result loc =
- let rec aux h =
- function
- TLval(h',o) | TStartOf (h',o) ->
- (match h with None -> Some h', loc_offset_to_offset ~result o
- | Some h when Logic_utils.is_same_lhost h h' ->
- Some h, loc_offset_to_offset ~result o
- | Some _ -> error_lval()
- )
- | Tat ({ term_node = TLval(TResult _,_)} as lv, BuiltinLabel Post) ->
- aux h lv.term_node
- | Tunion locs -> List.fold_left
- (fun (b,l) x ->
- let (b,l') = aux b x.term_node in b, l @ l') (h,[]) locs
- | Tempty_set -> h,[]
- | Trange _ | TAddrOf _ | Tat _
- | TSizeOfE _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TSizeOfStr _
- | TConst _ | TCastE _ | TAlignOf _ | TSizeOf _ | Tapp _ | Tif _
- | Toffset _ | Tbase_addr _ | Tblock_length _ | Tnull
- | TDataCons _ | TUpdate _ | Tlambda _
- | Ttypeof _ | Ttype _ | Tcomprehension _ | Tinter _ | Tlet _
- | TLogic_coerce _
- -> error_lval ()
- in snd (aux None loc.term_node)
-
-let term_lval_to_lval ~result = singleton (loc_lval_to_lval ~result)
-
-let term_to_lval ~result = singleton (loc_to_lval ~result)
-
-let term_to_exp ~result = singleton (loc_to_exp ~result)
-
-let term_offset_to_offset ~result = singleton (loc_offset_to_offset ~result)
-
-
-
-(** Utilities to identify [Locations.Zone.t] involved into
- [code_annotation]. *)
-module To_zone : sig
-
- type ctx = Db.Properties.Interp.To_zone.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 -> ctx
- (** [mk_ctx_func_contrat] to define an interpretation context related to
- [kernel_function] contracts.
- The control point of the interpretation is defined as follows:
- - pre-state if [state_opt=Some true]
- - post-state if [state_opt=Some false]
- - pre-state with possible reference to the post-state if
- [state_opt=None]. *)
-
- val mk_ctx_stmt_contrat:
- kernel_function -> stmt -> state_opt:bool option -> ctx
- (** [mk_ctx_stmt_contrat] to define an interpretation context related to
- [stmt] contracts.
- The control point of the interpretation is defined as follows:
- - pre-state if [state_opt=Some true]
- - post-state if [state_opt=Some false]
- - pre-state with possible reference to the post-state if
- [state_opt=None]. *)
-
- val mk_ctx_stmt_annot: kernel_function -> stmt -> ctx
- (** [mk_ctx_stmt_annot] to define an interpretation context related to an
- annotation attached before the [stmt]. *)
-
- type zone_info = Db.Properties.Interp.To_zone.t_zone_info
- type decl = Db.Properties.Interp.To_zone.t_decl
- type pragmas = Db.Properties.Interp.To_zone.t_pragmas
- val not_yet_implemented : string ref
- exception NYI of string
-
- val compute_term_deps: (stmt -> term -> Locations.Zone.t option) ref
- (** Provided by Eva, compute the memory zone on which a term depends. *)
-
- 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 code annotations of this
- [stmt]. *)
-
- val from_stmt_annots:
- (code_annotation -> bool) option ->
- (stmt * kernel_function) -> (zone_info * decl) * pragmas
- (** Entry point to get zones needed to evaluate code 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 code 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 a annotation filter *)
-end
-=
-struct
-
- exception NYI of string
- (* 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 }
-
-
- let empty_pragmas =
- { ctrl = Stmt.Set.empty;
- stmt = Stmt.Set.empty }
-
- let other_zones = Stmt.Hashtbl.create 7
- let locals = ref Varinfo.Set.empty
- let labels = ref Logic_label.Set.empty
- let pragmas = ref empty_pragmas
-
- let zone_result = ref (Some other_zones)
- let not_yet_implemented = ref ""
-
- let compute_term_deps = ref (fun _stmt _expr -> None)
-
- let add_top_zone not_yet_implemented_msg = match !zone_result with
- | None -> (* top zone *) ()
- | Some other_zones ->
- Stmt.Hashtbl.clear other_zones;
- not_yet_implemented := not_yet_implemented_msg;
- zone_result := None
-
- let add_result ~before ki zone = match !zone_result with
- | None -> (* top zone *) ()
- | Some other_zones ->
- let zone_true, zone_false =
- try Stmt.Hashtbl.find other_zones ki
- with Not_found -> Locations.Zone.bottom, Locations.Zone.bottom
- in
- Stmt.Hashtbl.replace other_zones
- ki
- (if before then Locations.Zone.join zone_true zone, zone_false
- else zone_true, Locations.Zone.join zone_false zone)
-
- let get_result_aux () =
- let result =
- let zones = match !zone_result with
- | None ->
- (* clear references for the next time when giving the result.
- Note that other_zones has been cleared in [add_top_zone]. *)
- zone_result := Some other_zones;
- None
- | Some other_zones ->
- let z =
- Stmt.Hashtbl.fold
- (fun ki (zone_true, zone_false) other_zones ->
- let add before zone others =
- if Locations.Zone.equal Locations.Zone.bottom zone then
- others
- else
- { before = before; ki = ki; zone = zone} :: others
- in
- add true zone_true (add false zone_false other_zones))
- other_zones
- []
- in
- (* clear table for the next time when giving the result *)
- Stmt.Hashtbl.clear other_zones;
- Some z
- in zones, {var = !locals; lbl = !labels}
- in
- let res_pragmas = !pragmas in
- (* clear references for the next time when giving the result *)
- (* TODO: this is hideous and error-prone as some functions are
- recursive. See VP comment about a more functional setting *)
- locals := Varinfo.Set.empty ;
- labels := Logic_label.Set.empty ;
- pragmas := empty_pragmas;
- result, res_pragmas
-
- let get_result () = fst (get_result_aux ())
-
- let get_annot_result () =
- get_result_aux ()
-
- (** 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
-
-
- class populate_zone before_opt ki_opt kf =
- (* 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] *)
- object(self)
- inherit Visitor.frama_c_inplace
- val mutable current_label = AbsLabel_here
-
- 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
- add_result ~before:current_before current_stmt zone
- | 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
-
- (** 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 =
- (* [VP 2011-01-28] TODO: factorize from_terms and from_term, and use
- a more functional setting. *)
- (try
- ignore(Visitor.visitFramacTerm
- (new populate_zone ctx.state_opt ctx.ki_opt ctx.kf) term)
- with NYI msg ->
- add_top_zone msg) ;
- locals := Varinfo.Set.union (extract_locals_from_term term) !locals;
- labels := Logic_label.Set.union (extract_labels_from_term term) !labels;
- get_result ()
-
- (** 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 =
- let f x =
- (try
- ignore(Visitor.visitFramacTerm
- (new populate_zone ctx.state_opt ctx.ki_opt ctx.kf) x)
- with NYI msg ->
- add_top_zone msg) ;
- locals := Varinfo.Set.union (extract_locals_from_term x) !locals;
- labels := Logic_label.Set.union (extract_labels_from_term x) !labels
- in
- List.iter f terms;
- 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 =
- (try
- ignore(Visitor.visitFramacPredicate
- (new populate_zone ctx.state_opt ctx.ki_opt ctx.kf) pred)
- with NYI msg ->
- add_top_zone msg) ;
- locals := Varinfo.Set.union (extract_locals_from_pred pred) !locals;
- labels := Logic_label.Set.union (extract_labels_from_pred pred) !labels;
- 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 =
- let f pred =
- (try
- ignore(Visitor.visitFramacPredicate
- (new populate_zone ctx.state_opt ctx.ki_opt ctx.kf) pred)
- with NYI msg ->
- add_top_zone msg) ;
- locals := Varinfo.Set.union (extract_locals_from_pred pred) !locals;
- labels := Logic_label.Set.union (extract_labels_from_pred pred) !labels
- in
- List.iter f preds;
- get_result ()
-
- (** Used by annotations entry points. *)
- let get_zone_from_annot a (ki,kf) loop_body_opt =
- let get_zone_from_term k x =
- (try
- ignore
- (Visitor.visitFramacTerm
- (new populate_zone (Some true) (Some (k, true)) kf) x)
- with NYI msg ->
- add_top_zone msg) ;
- (* to select the declaration of the variables *)
- locals := Varinfo.Set.union (extract_locals_from_term x) !locals;
- (* to select the labels of the annotation *)
- labels := Logic_label.Set.union (extract_labels_from_term x) !labels
- and get_zone_from_pred k x =
- (try
- ignore
- (Visitor.visitFramacPredicate
- (new populate_zone (Some true) (Some (k,true)) kf) x)
- with NYI msg ->
- add_top_zone msg) ;
- (* to select the declaration of the variables *)
- locals := Varinfo.Set.union (extract_locals_from_pred x) !locals;
- (* to select the labels of the annotation *)
- labels := Logic_label.Set.union (extract_labels_from_pred x) !labels
- in
- match a.annot_content with
- | APragma (Slice_pragma (SPexpr term) | Impact_pragma (IPexpr term)) ->
- (* to preserve the interpretation of the pragma *)
- get_zone_from_term ki term;
- (* to select the reachability of the pragma *)
- pragmas :=
- { !pragmas with ctrl = Stmt.Set.add ki !pragmas.ctrl }
- | APragma (Slice_pragma SPctrl) ->
- (* to select the reachability of the pragma *)
- pragmas :=
- { !pragmas with ctrl = Stmt.Set.add ki !pragmas.ctrl }
- | APragma (Slice_pragma SPstmt | Impact_pragma IPstmt) ->
- (* to preserve the effect of the statement *)
- pragmas :=
- { !pragmas with stmt = Stmt.Set.add ki !pragmas.stmt}
- | AAssert (_behav,pred) ->
- (* to preserve the interpretation of the assertion *)
- get_zone_from_pred ki pred.tp_statement;
- | 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;
- | AInvariant (_behav,false,pred) -> (* code invariant *)
- (* to preserve the interpretation of the code invariant *)
- get_zone_from_pred ki pred.tp_statement;
- | AVariant (term,_) ->
- (* to preserve the interpretation of the variant *)
- get_zone_from_term (Option.get loop_body_opt) term;
- | 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.iter
- (fun term ->
- locals := Varinfo.Set.union (extract_locals_from_term term) !locals;
- labels := Logic_label.Set.union (extract_labels_from_term term) !labels)
- terms
- | AAllocation (_,FreeAllocAny) -> ();
- | AAllocation (_,FreeAlloc(f,a)) ->
- let get_zone x =
- get_zone_from_term (Option.get loop_body_opt) x.it_content
- in
- List.iter get_zone f ;
- List.iter get_zone a
- | AAssigns (_, WritesAny) -> ()
- | AAssigns (_, Writes l) -> (* loop assigns *)
- let get_zone x =
- get_zone_from_term (Option.get loop_body_opt) x.it_content
- in
- List.iter
- (fun (zone,deps) ->
- get_zone zone;
- match deps with
- FromAny -> ()
- | From l -> List.iter get_zone l)
- 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) =
- Option.iter
- (fun caf ->
- let loop_body_opt = match ki.skind with
- | Loop(_, { bstmts = body :: _ }, _, _, _) -> Some body
- | _ -> None
- in
- Annotations.iter_code_annot
- (fun _ a ->
- if caf a then get_zone_from_annot a stmt loop_body_opt)
- ki)
- 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;
- 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 ;
- 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 from_stmt_annots ki =
- get_from_stmt_annots code_annot_filter (ki, kf)
- in iter_on_kf_stmt from_stmt_annots kf;
- get_annot_result ()
-
- (** 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
-end
-
-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.code_annot := code_annot;
- Db.Properties.Interp.term_lval := term_lval;
- Db.Properties.Interp.term := term;
- Db.Properties.Interp.predicate := predicate;
-
- Db.Properties.Interp.term_lval_to_lval := term_lval_to_lval;
- Db.Properties.Interp.term_to_exp := term_to_exp;
-
- Db.Properties.Interp.term_to_lval := term_to_lval;
- Db.Properties.Interp.term_offset_to_offset := term_offset_to_offset;
-
- Db.Properties.Interp.loc_to_lval := loc_to_lval;
- Db.Properties.Interp.loc_to_offset := loc_to_offset;
- Db.Properties.Interp.loc_to_exp := loc_to_exp;
-
- Db.Properties.Interp.To_zone.code_annot_filter := To_zone.code_annot_filter;
- Db.Properties.Interp.To_zone.mk_ctx_func_contrat :=
- To_zone.mk_ctx_func_contrat;
- Db.Properties.Interp.To_zone.mk_ctx_stmt_contrat :=
- To_zone.mk_ctx_stmt_contrat;
- Db.Properties.Interp.To_zone.mk_ctx_stmt_annot := To_zone.mk_ctx_stmt_annot;
-
- Db.Properties.Interp.To_zone.from_term := To_zone.from_term;
- Db.Properties.Interp.To_zone.from_terms := To_zone.from_terms;
- Db.Properties.Interp.To_zone.from_pred := To_zone.from_pred;
- Db.Properties.Interp.To_zone.from_preds := To_zone.from_preds;
- Db.Properties.Interp.To_zone.from_stmt_annot := To_zone.from_stmt_annot;
- Db.Properties.Interp.To_zone.from_stmt_annots := To_zone.from_stmt_annots;
- Db.Properties.Interp.To_zone.from_func_annots := To_zone.from_func_annots;
-
- Db.Properties.Interp.to_result_from_pred := to_result_from_pred;
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/ast_queries/logic_parse_string.ml b/src/kernel_services/ast_queries/logic_parse_string.ml
new file mode 100644
index 0000000000000000000000000000000000000000..9f5340c8e6d2276a9eac645bf5dd42ff4fed1289
--- /dev/null
+++ b/src/kernel_services/ast_queries/logic_parse_string.ml
@@ -0,0 +1,184 @@
+(**************************************************************************)
+(* *)
+(* 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 Error of Cil_types.location * string
+exception Unbound of string
+
+let find_var kf kinstr ?label var =
+ let vi =
+ try
+ let vi = Globals.Vars.find_from_astinfo var (VLocal kf) in
+ (match kinstr with
+ | Kglobal -> vi (* don't refine search: the Kglobal here
+ does not indicate the function contract, but merely
+ the fact that we do not have any information about
+ the targeted program point. Hence, no scope check
+ can be performed or we might reject many legitimate
+ terms and predicates.
+ *)
+ | Kstmt stmt ->
+ let scope =
+ match label with
+ | None | Some "Here" | Some "Post" | Some "Old" -> stmt
+ | Some "Pre" -> raise Not_found (* no local variable in scope. *)
+ | Some "Init" -> raise Not_found (* no local variable in scope. *)
+ | Some "LoopEntry" | Some "LoopCurrent" ->
+ if not (Kernel_function.stmt_in_loop kf stmt) then
+ Kernel.fatal
+ "Use of LoopEntry or LoopCurrent outside of a loop";
+ Kernel_function.find_enclosing_loop kf stmt
+ | Some l ->
+ (try let s = Kernel_function.find_label kf l in !s
+ with Not_found ->
+ Kernel.fatal
+ "Use of label %s that does not exist in function %a"
+ l Kernel_function.pretty kf)
+ in
+ if Kernel_function.var_is_in_scope scope vi then vi
+ else raise Not_found)
+ with Not_found ->
+ try
+ Globals.Vars.find_from_astinfo var (VFormal kf)
+ with Not_found ->
+ Globals.Vars.find_from_astinfo var VGlobal
+ in
+ cvar_to_lvar vi
+
+(** Create a logic typer, the interpretation being done for the given
+ kernel_function and stmt (the stmt is used check that loop invariants
+ are allowed). *)
+
+let default_typer kf kinstr =
+ let module LT = Logic_typing.Make
+ (struct
+ let anonCompFieldName = Cabs2cil.anonCompFieldName
+ let conditionalConversion = Cabs2cil.logicConditionalConversion
+
+ let is_loop () =
+ match kinstr with
+ | Kglobal -> false
+ | Kstmt s -> Kernel_function.stmt_in_loop kf s
+
+ let find_macro _ = raise Not_found
+
+ let find_var ?label var = find_var kf kinstr ?label var
+
+ let find_enum_tag x =
+ try
+ Globals.Types.find_enum_tag x
+ with Not_found ->
+ (* The ACSL typer tries to parse a string, first as a variable,
+ then as an enum. We report the "Unbound variable" message
+ here, as it is nicer for the user. However, this short-circuits
+ the later stages of resolution, for example global logic
+ variables. *)
+ raise (Unbound ("Unbound variable " ^ x))
+
+ let find_comp_field info s =
+ let field = Cil.getCompField info s in
+ Field(field,NoOffset)
+
+ let find_type = Globals.Types.find_type
+
+ let find_label s = Kernel_function.find_label kf s
+ include Logic_env
+
+ let add_logic_function =
+ add_logic_function_gen Logic_utils.is_same_logic_profile
+
+ let remove_logic_info =
+ remove_logic_info_gen Logic_utils.is_same_logic_profile
+
+ let integral_cast ty t =
+ raise
+ (Failure
+ (Format.asprintf
+ "term %a has type %a, but %a is expected."
+ Printer.pp_term t
+ Printer.pp_logic_type Linteger
+ Printer.pp_typ ty))
+
+ let error loc msg =
+ Pretty_utils.ksfprintf (fun e -> raise (Error (loc, e))) msg
+
+ let on_error f rollback x =
+ try f x with Error (loc,msg) as exn -> rollback (loc,msg); raise exn
+
+ end)
+ in
+ (module LT : Logic_typing.S)
+
+
+(** Set up the parser for the infamous 'C hack' needed to parse typedefs *)
+let sync_typedefs () =
+ Logic_env.reset_typenames ();
+ Globals.Types.iter_types
+ (fun name _ ns ->
+ if ns = Logic_typing.Typedef then Logic_env.add_typename name)
+
+let wrap f parsetree loc =
+ match parsetree with
+ | None -> raise (Error (loc, "Syntax error in annotation"))
+ | Some annot -> try f annot with Unbound s -> raise (Error (loc, s))
+
+let code_annot kf stmt s =
+ sync_typedefs ();
+ let module LT = (val default_typer kf (Kstmt stmt) : Logic_typing.S) in
+ let loc = Stmt.loc stmt in
+ let pa =
+ Option.bind
+ (Logic_lexer.annot (fst loc,s))
+ (function (_, Logic_ptree.Acode_annot (_,a)) -> Some a | _ -> None)
+ in
+ let parse pa =
+ LT.code_annot
+ (Stmt.loc stmt)
+ (Logic_utils.get_behavior_names (Annotations.funspec kf))
+ (Ctype (Kernel_function.get_return_type kf)) pa
+ in
+ wrap parse pa loc
+
+let default_term_env () =
+ Logic_typing.append_here_label (Logic_typing.Lenv.empty())
+
+let term kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
+ sync_typedefs ();
+ let module LT = (val default_typer kf Kglobal : Logic_typing.S) in
+ let pa_expr = Option.map snd (Logic_lexer.lexpr (fst loc, s)) in
+ let parse pa_expr = LT.term env pa_expr in
+ wrap parse pa_expr loc
+
+let term_lval kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
+ match (term kf ~loc ~env s).term_node with
+ | TLval lv -> lv
+ | _ -> raise (Error (loc, "Syntax error (expecting an lvalue)"))
+
+let predicate kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
+ sync_typedefs ();
+ let module LT = (val default_typer kf Kglobal : Logic_typing.S) in
+ let pa_expr = Option.map snd (Logic_lexer.lexpr (fst loc, s)) in
+ let parse pa_expr = LT.predicate env pa_expr in
+ wrap parse pa_expr loc
diff --git a/src/kernel_services/analysis/logic_interp.mli b/src/kernel_services/ast_queries/logic_parse_string.mli
similarity index 65%
rename from src/kernel_services/analysis/logic_interp.mli
rename to src/kernel_services/ast_queries/logic_parse_string.mli
index 09165c84558a238c1de29fc88b0b9af9118deae5..0083f8bfb0fa50381acb475126c752446d7d2201 100644
--- a/src/kernel_services/analysis/logic_interp.mli
+++ b/src/kernel_services/ast_queries/logic_parse_string.mli
@@ -20,24 +20,25 @@
(* *)
(**************************************************************************)
-(** All the interesting functions of this module are exported through
- {!Db.Interp}. *)
-
-(* TODO: remove the module Properties from Db and export directly the
- functions from here. *)
-
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 Error of Cil_types.location * string
+exception Unbound of string
-exception Error of location * string
+(** 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}. *)
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
+val code_annot : kernel_function -> stmt -> string -> code_annotation
+val term_lval :
+ kernel_function -> ?loc:location -> ?env:Logic_typing.Lenv.t -> string ->
+ Cil_types.term_lval
+val term :
+ kernel_function -> ?loc:location -> ?env:Logic_typing.Lenv.t -> string ->
+ Cil_types.term
+val predicate :
+ kernel_function -> ?loc:location -> ?env:Logic_typing.Lenv.t -> string ->
+ Cil_types.predicate
diff --git a/src/kernel_services/ast_queries/logic_to_c.ml b/src/kernel_services/ast_queries/logic_to_c.ml
new file mode 100644
index 0000000000000000000000000000000000000000..3969ee179d3718659be5974ab9121361100fa947
--- /dev/null
+++ b/src/kernel_services/ast_queries/logic_to_c.ml
@@ -0,0 +1,215 @@
+(**************************************************************************)
+(* *)
+(* 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
+
+exception No_conversion
+
+let error_lval () = raise No_conversion
+
+let rec logic_type_to_typ = function
+ | Ctype typ -> typ
+ | Linteger -> TInt(ILongLong,[]) (*TODO: to have an unlimited integer type
+ in the logic interpretation*)
+ | Lreal -> TFloat(FDouble,[]) (* TODO: handle reals, not floats... *)
+ | Ltype({lt_name = name},[]) when name = Utf8_logic.boolean ->
+ TInt(ILongLong,[])
+ | Ltype({lt_name = "set"},[t]) -> logic_type_to_typ t
+ | Ltype _ | Lvar _ | Larrow _ -> error_lval ()
+
+
+(* Expect conversion to be possible on all sub-terms, otherwise raise an error. *)
+
+let logic_var_to_var { lv_origin = lv } =
+ match lv with
+ | None -> error_lval ()
+ | Some lv -> lv
+
+let create_const_list loc kind low high =
+ let rec aux acc i =
+ if Integer.lt i low then acc
+ else
+ aux (new_exp ~loc (Const (CInt64 (i,kind,None)))::acc) (Integer.pred i)
+ in aux [] high
+
+let range low high =
+ let loc = fst low.eloc, snd high.eloc in
+ match (Cil.constFold true low).enode, (Cil.constFold true high).enode with
+ Const(CInt64(low,kind,_)), Const(CInt64(high,_,_)) ->
+ create_const_list loc kind low high
+ | _ -> error_lval()
+
+let singleton f loc =
+ match f loc with
+ [ l ] -> l
+ | _ -> error_lval()
+
+let rec loc_lval_to_lval ?result (lh, lo) =
+ Extlib.product
+ (fun x y -> (x,y))
+ (loc_lhost_to_lhost ?result lh)
+ (loc_offset_to_offset ?result lo)
+
+and loc_lhost_to_lhost ?result = function
+ | TVar lvar -> [Var (logic_var_to_var lvar)]
+ | TMem lterm -> List.map (fun x -> Mem x) (loc_to_exp ?result lterm)
+ | TResult _ ->
+ ( match result with
+ None -> error_lval()
+ | Some v -> [Var v])
+
+and loc_offset_to_offset ?result = function
+ | TNoOffset -> [NoOffset]
+ | TModel _ -> error_lval ()
+ | TField (fi, lo) ->
+ List.map (fun x -> Field (fi,x)) (loc_offset_to_offset ?result lo)
+ | TIndex (lexp, lo) ->
+ Extlib.product
+ (fun x y -> Index(x,y))
+ (loc_to_exp ?result lexp)
+ (loc_offset_to_offset ?result lo)
+
+and loc_to_exp ?result {term_node = lnode ; term_type = ltype; term_loc = loc} =
+ match lnode with
+ | TLval lv ->
+ List.map (fun x -> new_exp ~loc (Lval x)) (loc_lval_to_lval ?result lv)
+ | TAddrOf lv ->
+ List.map (fun x -> new_exp ~loc (AddrOf x)) (loc_lval_to_lval ?result lv)
+ | TStartOf lv ->
+ List.map (fun x -> new_exp ~loc (StartOf x)) (loc_lval_to_lval ?result lv)
+ | TSizeOfE lexp ->
+ List.map (fun x -> new_exp ~loc (SizeOfE x)) (loc_to_exp ?result lexp)
+ | TAlignOfE lexp ->
+ List.map (fun x -> new_exp ~loc (AlignOfE x)) (loc_to_exp ?result lexp)
+ | TUnOp (unop, lexp) ->
+ List.map
+ (fun x -> new_exp ~loc (UnOp (unop, x, logic_type_to_typ ltype)))
+ (loc_to_exp ?result lexp)
+ | TBinOp (binop, lexp1, lexp2) ->
+ Extlib.product
+ (fun x y -> new_exp ~loc (BinOp (binop, x,y, logic_type_to_typ ltype)))
+ (loc_to_exp ?result lexp1)
+ (loc_to_exp ?result lexp2)
+ | TSizeOfStr string -> [new_exp ~loc (SizeOfStr string)]
+ | TConst constant ->
+ (* TODO: Very likely to fail on large integer and incorrect on reals not
+ representable as floats *)
+ [new_exp ~loc (Const (Logic_utils.lconstant_to_constant constant))]
+ | TCastE (typ, lexp) ->
+ List.map
+ (fun x -> new_exp ~loc (CastE (typ, x))) (loc_to_exp ?result lexp)
+ | TAlignOf typ -> [new_exp ~loc (AlignOf typ)]
+ | TSizeOf typ -> [new_exp ~loc (SizeOf typ)]
+ | Trange (Some low, Some high) ->
+ let low = singleton (loc_to_exp ?result) low in
+ let high = singleton (loc_to_exp ?result) high in
+ range low high
+ | Tunion l -> List.concat (List.map (loc_to_exp ?result) l)
+ | Tempty_set -> []
+ | Tinter _ | Tcomprehension _ -> error_lval()
+ | Tat ({term_node = TAddrOf (TVar _, TNoOffset)} as taddroflval, _) ->
+ loc_to_exp ?result taddroflval
+ | TLogic_coerce(Linteger, t) when Logic_typing.is_integral_type t.term_type ->
+ loc_to_exp ?result t
+ | TLogic_coerce(Lreal, t) when Logic_typing.is_integral_type t.term_type ->
+ List.map
+ (fun x -> new_exp ~loc (CastE (logic_type_to_typ Lreal, x)))
+ (loc_to_exp ?result t)
+ | TLogic_coerce(Lreal, t) when Logic_typing.is_arithmetic_type t.term_type ->
+ loc_to_exp ?result t
+ | TLogic_coerce (set, t)
+ when
+ Logic_const.is_set_type set &&
+ Logic_utils.is_same_type
+ (Logic_typing.type_of_set_elem set) t.term_type ->
+ loc_to_exp ?result t
+ | Tnull -> [ Cil.mkCast ~newt:(TPtr(TVoid [], [])) (Cil.zero ~loc) ]
+
+ (* additional constructs *)
+ | Tapp _ | Tlambda _ | Trange _ | Tlet _
+ | TDataCons _
+ | Tif _
+ | Tat _
+ | Tbase_addr _
+ | Toffset _
+ | Tblock_length _
+ | TUpdate _ | Ttypeof _ | Ttype _
+ | TLogic_coerce _
+ -> error_lval ()
+
+let rec loc_to_lval ?result t =
+ match t.term_node with
+ | TLval lv -> loc_lval_to_lval ?result lv
+ | TAddrOf lv -> loc_lval_to_lval ?result lv
+ | TStartOf lv -> loc_lval_to_lval ?result lv
+ | Tunion l1 -> List.concat (List.map (loc_to_lval ?result) l1)
+ | Tempty_set -> []
+ (* coercions to arithmetic types cannot be lval. We only have to consider
+ a coercion to set here.
+ *)
+ | TLogic_coerce(set, t) when
+ Logic_typing.is_set_type set &&
+ Logic_utils.is_same_type
+ (Logic_typing.type_of_set_elem set) t.term_type ->
+ loc_to_lval ?result t
+ | Tinter _ -> error_lval() (* TODO *)
+ | Tcomprehension _ -> error_lval()
+ | TSizeOfE _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TSizeOfStr _
+ | TConst _ | TCastE _ | TAlignOf _ | TSizeOf _ | Tapp _ | Tif _
+ | Tat _ | Toffset _ | Tbase_addr _ | Tblock_length _ | Tnull | Trange _
+ | TDataCons _ | TUpdate _ | Tlambda _
+ | Ttypeof _ | Ttype _ | Tlet _ | TLogic_coerce _ ->
+ error_lval ()
+
+let loc_to_offset ?result loc =
+ let rec aux h =
+ function
+ TLval(h',o) | TStartOf (h',o) ->
+ (match h with None -> Some h', loc_offset_to_offset ?result o
+ | Some h when Logic_utils.is_same_lhost h h' ->
+ Some h, loc_offset_to_offset ?result o
+ | Some _ -> error_lval()
+ )
+ | Tat ({ term_node = TLval(TResult _,_)} as lv, BuiltinLabel Post) ->
+ aux h lv.term_node
+ | Tunion locs -> List.fold_left
+ (fun (b,l) x ->
+ let (b,l') = aux b x.term_node in b, l @ l') (h,[]) locs
+ | Tempty_set -> h,[]
+ | Trange _ | TAddrOf _ | Tat _
+ | TSizeOfE _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TSizeOfStr _
+ | TConst _ | TCastE _ | TAlignOf _ | TSizeOf _ | Tapp _ | Tif _
+ | Toffset _ | Tbase_addr _ | Tblock_length _ | Tnull
+ | TDataCons _ | TUpdate _ | Tlambda _
+ | Ttypeof _ | Ttype _ | Tcomprehension _ | Tinter _ | Tlet _
+ | TLogic_coerce _
+ -> error_lval ()
+ in snd (aux None loc.term_node)
+
+let term_lval_to_lval ?result = singleton (loc_lval_to_lval ?result)
+
+let term_to_lval ?result = singleton (loc_to_lval ?result)
+
+let term_to_exp ?result = singleton (loc_to_exp ?result)
+
+let term_offset_to_offset ?result = singleton (loc_offset_to_offset ?result)
diff --git a/src/kernel_services/ast_queries/logic_to_c.mli b/src/kernel_services/ast_queries/logic_to_c.mli
new file mode 100644
index 0000000000000000000000000000000000000000..aa0a051920a8acfd815dec3214bd2f6a7e219030
--- /dev/null
+++ b/src/kernel_services/ast_queries/logic_to_c.mli
@@ -0,0 +1,59 @@
+(**************************************************************************)
+(* *)
+(* 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
+
+exception No_conversion
+
+val logic_type_to_typ : logic_type -> typ
+val logic_var_to_var : logic_var -> varinfo
+
+val loc_lval_to_lval : ?result:varinfo -> term_lval -> lval list
+val loc_lhost_to_lhost : ?result:varinfo -> term_lhost -> lhost list
+val loc_offset_to_offset : ?result:varinfo -> term_offset -> offset list
+
+val loc_to_exp : ?result:varinfo -> term -> exp list
+(** @return a list of C expressions.
+ @raise No_conversion if the argument is not a valid set of
+ expressions. *)
+
+val loc_to_lval : ?result:varinfo -> term -> lval list
+(** @return a list of C locations.
+ @raise No_conversion if the argument is not a valid set of
+ left values. *)
+
+val loc_to_offset : ?result:varinfo -> term -> offset list
+(** @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 *)
+
+val term_lval_to_lval : ?result:varinfo -> term_lval -> lval
+(** @raise No_conversion if the argument is not a left value. *)
+
+val term_to_lval : ?result:varinfo -> term -> lval
+(** @raise No_conversion if the argument is not a left value. *)
+
+val term_to_exp : ?result:varinfo -> term -> exp
+(** @raise No_conversion if the argument is not a valid expression. *)
+
+val term_offset_to_offset : ?result:varinfo -> term_offset -> offset
+(** @raise No_conversion if the argument is not a valid offset. *)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index cdc7e48ad020238b2fed5ca800136e243175f19e..9de89b3bbd52faf2f891fa3e459652c61145fa1e 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -625,6 +625,26 @@ let is_plain_pointer_type t =
let is_array_type = plain_or_set is_plain_array_type
let is_pointer_type = plain_or_set is_plain_pointer_type
+module type S =
+sig
+ val type_of_field:
+ location -> string -> Cil_types.logic_type ->
+ (term_offset * Cil_types.logic_type)
+ val mk_cast:
+ ?explicit:bool -> Cil_types.term -> Cil_types.logic_type -> Cil_types.term
+ val term : Lenv.t -> Logic_ptree.lexpr -> term
+ val predicate : Lenv.t -> Logic_ptree.lexpr -> predicate
+ val code_annot :
+ Cil_types.location -> string list ->
+ Cil_types.logic_type -> Logic_ptree.code_annot -> code_annotation
+ val type_annot : location -> Logic_ptree.type_annot -> logic_info
+ val model_annot : location -> Logic_ptree.model_annot -> model_info
+ val annot : Logic_ptree.decl -> global_annotation
+ val funspec :
+ string list ->
+ varinfo -> (varinfo list) option -> typ -> Logic_ptree.spec -> funspec
+end
+
module Make
(C:
sig
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index ef8c2d3c9ffe5eb8231fa04760fdbd083f3fa8c2..a9ee8eed4a14fe9ba9929d240f436faab4921714 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -147,52 +147,8 @@ type typing_context = {
*)
}
-module Make
- (C :
- sig
- val is_loop: unit -> bool
- (** whether the annotation we want to type is contained in a loop.
- Only useful when creating objects of type [code_annotation]. *)
-
- val anonCompFieldName : string
- val conditionalConversion : typ -> typ -> typ
- val find_macro : string -> Logic_ptree.lexpr
- val find_var : ?label:string -> string -> logic_var
- (** see corresponding field in {!Logic_typing.typing_context}. *)
-
- val find_enum_tag : string -> exp * typ
- val find_type : type_namespace -> string -> typ
- val find_comp_field: compinfo -> string -> offset
- val find_label : string -> stmt ref
-
- val remove_logic_function : string -> unit
- val remove_logic_info: logic_info -> unit
- val remove_logic_type: string -> unit
- val remove_logic_ctor: string -> unit
-
- val add_logic_function: logic_info -> unit
- val add_logic_type: string -> logic_type_info -> unit
- val add_logic_ctor: string -> logic_ctor_info -> unit
-
- val find_all_logic_functions : string -> Cil_types.logic_info list
- val find_logic_type: string -> logic_type_info
- val find_logic_ctor: string -> logic_ctor_info
- (** What to do when we have a term of type Integer in a context
- expecting a C integral type.
- @raise Failure to reject such conversion
- @since Nitrogen-20111001
- *)
- val integral_cast: Cil_types.typ -> Cil_types.term -> Cil_types.term
-
- (** raises an error at the given location and with the given message.
- @since Magnesium-20151001 *)
- val error: location -> ('a,Format.formatter,unit, 'b) format4 -> 'a
-
- (** see {!Logic_typing.typing_context}. *)
- val on_error: ('a -> 'b) -> ((location * string) -> unit) -> 'a -> 'b
-
- end) :
+module type S =
sig
(** @since Nitrogen-20111001 *)
@@ -245,6 +201,54 @@ sig
end
+module Make
+ (C :
+ sig
+ val is_loop: unit -> bool
+ (** whether the annotation we want to type is contained in a loop.
+ Only useful when creating objects of type [code_annotation]. *)
+
+ val anonCompFieldName : string
+ val conditionalConversion : typ -> typ -> typ
+ val find_macro : string -> Logic_ptree.lexpr
+ val find_var : ?label:string -> string -> logic_var
+ (** see corresponding field in {!Logic_typing.typing_context}. *)
+
+ val find_enum_tag : string -> exp * typ
+ val find_type : type_namespace -> string -> typ
+ val find_comp_field: compinfo -> string -> offset
+ val find_label : string -> stmt ref
+
+ val remove_logic_function : string -> unit
+ val remove_logic_info: logic_info -> unit
+ val remove_logic_type: string -> unit
+ val remove_logic_ctor: string -> unit
+
+ val add_logic_function: logic_info -> unit
+ val add_logic_type: string -> logic_type_info -> unit
+ val add_logic_ctor: string -> logic_ctor_info -> unit
+
+ val find_all_logic_functions : string -> Cil_types.logic_info list
+ val find_logic_type: string -> logic_type_info
+ val find_logic_ctor: string -> logic_ctor_info
+
+ (** What to do when we have a term of type Integer in a context
+ expecting a C integral type.
+ @raise Failure to reject such conversion
+ @since Nitrogen-20111001
+ *)
+ val integral_cast: Cil_types.typ -> Cil_types.term -> Cil_types.term
+
+ (** raises an error at the given location and with the given message.
+ @since Magnesium-20151001 *)
+ val error: location -> ('a,Format.formatter,unit, 'b) format4 -> 'a
+
+ (** see {!Logic_typing.typing_context}. *)
+ val on_error: ('a -> 'b) -> ((location * string) -> unit) -> 'a -> 'b
+
+ end) : S
+
+
(** append the Old and Post labels in the environment *)
val append_old_and_post_labels: Lenv.t -> Lenv.t
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 539411cd3e6f333e884bc9c2f1702c8fdb6d32a1..bdf3b9686268c96151ce2b9021c74d342caf38ad 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -683,151 +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
-
- (** Interpretation and conversions of of formulas *)
- let code_annot = mk_fun "Properties.Interp.code_annot"
- let term_lval = mk_fun "Properties.Interp.term_lval"
- let term = mk_fun "Properties.Interp.term"
- let predicate = mk_fun "Properties.Interp.predicate"
- let term_lval_to_lval = mk_resultfun "Properties.Interp.term_lval_to_lval"
- let term_to_exp = mk_resultfun "Properties.Interp.term_to_exp"
- let term_to_lval = mk_resultfun "Properties.Interp.term_to_lval"
- let loc_to_lval = mk_resultfun "Properties.Interp.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 = mk_resultfun "Properties.Interp.loc_to_offset"
- let loc_to_exp = mk_resultfun "Properties.Interp.loc_to_exp"
- let term_offset_to_offset =
- mk_resultfun "Properties.Interp.term_offset_to_offset"
-
- module To_zone : sig
- (** The signature of the mli is copy pasted here because of
- http://caml.inria.fr/mantis/view.php?id=7313 *)
- 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 = {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 = {var: Varinfo.Set.t ; (* related to vars of the annot *)
- lbl: Logic_label.Set.t} (* related to labels of the annot *)
- type t_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
- = struct
- type t_ctx =
- { state_opt: bool option;
- ki_opt: (stmt * bool) option;
- kf:Kernel_function.t }
- let mk_ctx_func_contrat = mk_fun "Interp.To_zone.mk_ctx_func_contrat"
- let mk_ctx_stmt_contrat = mk_fun "Interp.To_zone.mk_ctx_stmt_contrat"
- let mk_ctx_stmt_annot = mk_fun "Interp.To_zone.mk_ctx_stmt_annot"
- type t = {before:bool ; ki:stmt ; zone:Locations.Zone.t}
- type t_zone_info = (t list) option
- type t_decl =
- { var: Varinfo.Set.t;
- lbl: Logic_label.Set.t }
- type t_pragmas =
- { ctrl: Stmt.Set.t;
- stmt: Stmt.Set.t }
- let from_term = mk_fun "Interp.To_zone.from_term"
- let from_terms= mk_fun "Interp.To_zone.from_terms"
- let from_pred = mk_fun "Interp.To_zone.from_pred"
- let from_preds= mk_fun "Interp.To_zone.from_preds"
- let from_zone = mk_fun "Interp.To_zone.from_zone"
- let from_stmt_annot= mk_fun "Interp.To_zone.from_stmt_annot"
- let from_stmt_annots= mk_fun "Interp.To_zone.from_stmt_annots"
- let from_func_annots= mk_fun "Interp.To_zone.from_func_annots"
- let code_annot_filter= mk_fun "Interp.To_zone.code_annot_filter"
- end
-
- let to_result_from_pred =
- mk_fun "Properties.Interp.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 cdf6565253e401472131c324436f6b7de1dd7645..16a3b015d7f20125b3a5ff540f734facc9787e90 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -527,195 +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 = {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 = {var: Varinfo.Set.t ; (* related to vars of the annot *)
- lbl: Logic_label.Set.t} (* related to labels of the annot *)
- type t_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
-
(* ************************************************************************* *)
(** {2 Plugins} *)
(* ************************************************************************* *)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 3b01353a856e3a5e391be69702788182fad68504..d36e2198c59e4b45cdb8ac8bfa790fc28b6e49e9 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -727,6 +727,10 @@ module Eva_results: sig
val change_callstacks:
(Value_types.callstack -> Value_types.callstack) -> results -> results
+ val eval_tlval_as_location :
+ ?result:Cil_types.varinfo ->
+ Cvalue.Model.t -> Cil_types.term -> Locations.location
+
end
module Unit_tests: sig
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index 357298d59aa5092fa423865771fdf2188e1bcb99..dad1935488d6d4f6a65bb5cd5cb34100ddbe3202 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -162,8 +162,8 @@ let () = Request.register ~package
(* ----- Register Eva information ------------------------------------------- *)
let term_lval_to_lval tlval =
- try !Db.Properties.Interp.term_lval_to_lval ~result:None tlval
- with Db.Properties.Interp.No_conversion -> raise Not_found
+ try Logic_to_c.term_lval_to_lval tlval
+ with Logic_to_c.No_conversion -> raise Not_found
let print_value fmt loc =
let is_scalar = Cil.isScalarType in
diff --git a/src/plugins/eva/gui/register_gui.ml b/src/plugins/eva/gui/register_gui.ml
index 31d005daf3e195dac525dbafe363ac52e7ba978c..e91019d1c695d319ea934b17b08a95eb0d16c49c 100644
--- a/src/plugins/eva/gui/register_gui.ml
+++ b/src/plugins/eva/gui/register_gui.ml
@@ -331,16 +331,16 @@ module Select (Eval: Eval) = struct
if txt = "NULL" then
select_null main_ui loc
else
- let term = !Db.Properties.Interp.term ~env kf txt in
+ let term = Logic_parse_string.term ~env kf txt in
match term.term_node with
| TLval _ | TStartOf _ -> select_tlv main_ui loc term
| _ -> select_term main_ui loc term
end
| Pred ->
- let pred = !Db.Properties.Interp.predicate ~env kf txt in
+ let pred = Logic_parse_string.predicate ~env kf txt in
select_predicate main_ui loc pred
with
- | Logic_interp.Error (_, mess) ->
+ | Logic_parse_string.Error (_, mess) ->
main_ui#error "Invalid %a: %s" pp_term_or_pred tp mess
| Parsing.Parse_error ->
main_ui#error "Invalid %a: Parse error" pp_term_or_pred tp
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index ce12bb0f25478cd2cd9a23dbb6344017e4d4679c..b256b6c25465a3a5d4fe8196ada362dea25ffffc 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -2774,30 +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
-
-
-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 Db.Properties.Interp.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 Db.Properties.Interp.No_conversion
- );
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../../.."
-End:
-*)
diff --git a/src/plugins/eva/legacy/logic_inout.ml b/src/plugins/eva/legacy/logic_inout.ml
index 7ae89d1e63344cad129208aff8220dfd5ef1e1da..34ed60bad552a00cac80bb75364e007797e383dc 100644
--- a/src/plugins/eva/legacy/logic_inout.ml
+++ b/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
diff --git a/src/plugins/eva/partitioning/partitioning_parameters.ml b/src/plugins/eva/partitioning/partitioning_parameters.ml
index cf0779ba267244d0f02d5d86d12190d23e34d629..591ef7cbc8bf9ba803433ba9b53f051ad051d475 100644
--- a/src/plugins/eva/partitioning/partitioning_parameters.ml
+++ b/src/plugins/eva/partitioning/partitioning_parameters.ml
@@ -55,9 +55,6 @@ struct
| Per_stmt_slevel.NoMerge -> false
| Per_stmt_slevel.Merge f -> f stmt
- let term_to_exp term =
- !Db.Properties.Interp.term_to_exp ~result:None term
-
let min_loop_unroll = MinLoopUnroll.get ()
let auto_loop_unroll = AutoLoopUnroll.get ()
let default_loop_unroll = DefaultLoopUnroll.get ()
@@ -96,8 +93,8 @@ struct
try
match Logic_utils.constFoldTermToInt t with
| Some n -> Partition.IntLimit (Integer.to_int_exn n)
- | None -> Partition.ExpLimit (term_to_exp t)
- with Z.Overflow | Db.Properties.Interp.No_conversion ->
+ | None -> Partition.ExpLimit (Logic_to_c.term_to_exp t)
+ with Z.Overflow | Logic_to_c.No_conversion ->
warn "invalid loop unrolling parameter; ignoring";
default
end
@@ -134,7 +131,7 @@ struct
in
action :: acc
with
- Db.Properties.Interp.No_conversion ->
+ Logic_to_c.No_conversion ->
warn "split/merge expressions must be valid expressions; ignoring";
acc (* Impossible to convert term to lval *)
in
diff --git a/src/plugins/eva/utils/eva_annotations.ml b/src/plugins/eva/utils/eva_annotations.ml
index 448f89f6bdedf25d89fefd9a0c6ab81f42d661b3..cd9dde0c3620b809156f9d6efdb561c1d79339f3 100644
--- a/src/plugins/eva/utils/eva_annotations.ml
+++ b/src/plugins/eva/utils/eva_annotations.ml
@@ -191,7 +191,7 @@ struct
when possible, to avoid changes due to its reconversion to a C term. *)
type t = split_term * Cil_types.term option
- let term_to_exp = !Db.Properties.Interp.term_to_exp ~result:None
+ let term_to_exp = Logic_to_c.term_to_exp ?result:None
let parse ~typing_context:context = function
| [t] ->
@@ -206,7 +206,7 @@ struct
with
| No_term ->
Predicate (context.type_predicate context context.pre_state t), None
- | Db.Properties.Interp.No_conversion ->
+ | Logic_to_c.No_conversion ->
Kernel.warning ~wkey:Kernel.wkey_annot_error ~once:true ~current:true
"split/merge expressions must be valid expressions; ignoring";
raise Parse_error
@@ -354,8 +354,6 @@ let get_allocation = Allocation.get
module ArraySegmentation = Register (struct
- module Interp = Db.Properties.Interp
-
type t = Cil_types.varinfo * Cil_types.offset * Cil_types.exp list
let name = "array_partition"
let is_loop_annot = false
@@ -363,11 +361,12 @@ module ArraySegmentation = Register (struct
let convert = function
| {term_node = TLval (TVar {lv_origin=Some vi}, toffset)} :: tbounds ->
begin try
- let offset = !Interp.term_offset_to_offset ~result:None toffset
- and bounds = List.map (!Interp.term_to_exp ~result:None) tbounds in
+ let offset = Logic_to_c.term_offset_to_offset toffset
+ and bounds = List.map (Logic_to_c.term_to_exp ?result:None) tbounds
+ in
Some (vi, offset, bounds)
with
- Interp.No_conversion -> None
+ Logic_to_c.No_conversion -> None
end
| _ -> None
diff --git a/src/plugins/eva/utils/eva_results.ml b/src/plugins/eva/utils/eva_results.ml
index fcdde083d16286edfcb8b0059f098e4381f94ae6..0d89c3a001b26a3f1abe5f22be0d05f3054e67ef 100644
--- a/src/plugins/eva/utils/eva_results.ml
+++ b/src/plugins/eva/utils/eva_results.ml
@@ -263,6 +263,10 @@ let merge r1 r2 =
{ main; before_states; after_states; kf_initial_states;
initial_state; initial_args; alarms; statuses; kf_callers }
+let eval_tlval_as_location ?result state term =
+ let env = Eval_terms.env_post_f ~pre:state ~post:state ~result () in
+ try Eval_terms.eval_tlval_as_location ~alarm_mode:Ignore env term
+ with Eval_terms.LogicEvalError _ -> raise Logic_to_c.No_conversion
(*
Local Variables:
diff --git a/src/plugins/eva/utils/eva_results.mli b/src/plugins/eva/utils/eva_results.mli
index 19e35f6bd7b67061ba4db590f2d0f1ea614690bf..ca502d65f62b59dd73636b9b2868904ce97d0b49 100644
--- a/src/plugins/eva/utils/eva_results.mli
+++ b/src/plugins/eva/utils/eva_results.mli
@@ -46,6 +46,10 @@ val merge: results -> results -> results
val change_callstacks:
(Value_types.callstack -> Value_types.callstack) -> results -> results
+val eval_tlval_as_location :
+ ?result:Cil_types.varinfo ->
+ Cvalue.Model.t -> Cil_types.term -> Locations.location
+
[@@@ api_end]
(*
diff --git a/src/plugins/eva/utils/widen_hints_ext.ml b/src/plugins/eva/utils/widen_hints_ext.ml
index a43cf73ee5ebbb5021f04f3a5c44ad1a1f7b8261..e31a802ec9ff94a86d978f6cf51bdd1bef03997d 100644
--- a/src/plugins/eva/utils/widen_hints_ext.ml
+++ b/src/plugins/eva/utils/widen_hints_ext.ml
@@ -114,7 +114,7 @@ let widen_hint_terms_of_terms terms =
Some (named_lval, hint_thresholds)
| {term_node = TLval tlv} ->
let (lhost, offset) =
- !Db.Properties.Interp.term_lval_to_lval ~result:None tlv
+ Logic_to_c.term_lval_to_lval tlv
in
let hint_vars = match lhost with
| Mem e -> HintMem (e, offset)
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 14f127e123d57181ee9a74c02a66775eeeecc107..fe608f7c3eab7d16d4b97df2364afb1cd840ed20 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -101,9 +101,7 @@ let compute_using_prototype_for_state state kf assigns =
now, so we assume it is all data dependencies *)
let inputs_deps = Function_Froms.Deps.from_data_deps zone_from in
try
- let coffs =
- !Db.Properties.Interp.loc_to_offset ~result:None out.it_content
- in
+ let coffs = Logic_to_c.loc_to_offset out.it_content in
List.fold_left
(fun acc coff ->
let (base,width) = bitsOffset rt_typ coff in
@@ -112,7 +110,7 @@ let compute_using_prototype_for_state state kf assigns =
~start:base ~size ~m:acc inputs_deps)
)
acc coffs
- with Db.Properties.Interp.No_conversion | SizeOfError _ ->
+ with Logic_to_c.No_conversion | SizeOfError _ ->
From_parameters.result ~once:true ~current:true
"Unable to extract a proper offset. \
Using FROM for the whole \\result";
diff --git a/src/plugins/occurrence/register.ml b/src/plugins/occurrence/register.ml
index bd78fc766d3b73356947fd2c133532ad0d8caee1..99e106aa9291f102439916a320fb517342a80579 100644
--- a/src/plugins/occurrence/register.ml
+++ b/src/plugins/occurrence/register.ml
@@ -124,11 +124,11 @@ class occurrence = object (self)
method! vterm_lval tlv =
(try
- let lv = !Db.Properties.Interp.term_lval_to_lval ~result:None tlv in
+ let lv = Logic_to_c.term_lval_to_lval tlv in
ignore (self#vlval lv)
with
(* Translation to lval failed.*)
- | Db.Properties.Interp.No_conversion -> ());
+ | Logic_to_c.No_conversion -> ());
DoChildren
method! vstmt_aux s =
diff --git a/src/plugins/pdg/annot.ml b/src/plugins/pdg/annot.ml
index 09c37fa94373490d0eb7133f4c09be10d36bccec..da0865896fa1318201e1e18505b146cd79d5f947 100644
--- a/src/plugins/pdg/annot.ml
+++ b/src/plugins/pdg/annot.ml
@@ -35,9 +35,9 @@ type decl_info = PdgTypes.Node.t list
let zone_info_nodes pdg data_info =
let add_info_nodes pdg (nodes_acc, undef_acc) info =
- let stmt = info.Db.Properties.Interp.To_zone.ki in
- let before = info.Db.Properties.Interp.To_zone.before in
- let zone = info.Db.Properties.Interp.To_zone.zone in
+ let stmt = info.Logic_deps.ki in
+ let before = info.Logic_deps.before in
+ let zone = info.Logic_deps.zone in
Pdg_parameters.debug ~level:2 "[pdg:annotation] need %a %s stmt %d@."
Locations.Zone.pretty zone
(if before then "before" else "after") stmt.sid;
@@ -70,38 +70,35 @@ let find_nodes_for_function_contract pdg f_interpret =
let (data_info, decl_label_info) = f_interpret kf in
let data_dpds = zone_info_nodes pdg data_info in
let decl_nodes = (* No way to get stmt from labels of at construct into function contracts *)
- get_decl_nodes pdg decl_label_info.Db.Properties.Interp.To_zone.var
+ get_decl_nodes pdg decl_label_info.Logic_deps.var
in
decl_nodes, data_dpds
let find_fun_precond_nodes (pdg:PdgTypes.Pdg.t) p =
let f_interpret kf =
- let f_ctx = !Db.Properties.Interp.To_zone.mk_ctx_func_contrat
- ~state_opt:(Some true) kf in
- !Db.Properties.Interp.To_zone.from_pred p f_ctx
+ let f_ctx = Logic_deps.mk_ctx_func_contract ~before:true kf in
+ Logic_deps.from_pred p f_ctx
in find_nodes_for_function_contract pdg f_interpret
let find_fun_postcond_nodes pdg p =
let f_interpret kf =
- let f_ctx = !Db.Properties.Interp.To_zone.mk_ctx_func_contrat
- ~state_opt:(Some false) kf in
- !Db.Properties.Interp.To_zone.from_pred p f_ctx
+ let f_ctx = Logic_deps.mk_ctx_func_contract ~before:false kf in
+ Logic_deps.from_pred p f_ctx
in let nodes,deps = find_nodes_for_function_contract pdg f_interpret
in let nodes =
(* find is \result is used in p, and if it is the case,
* add the node [Sets.find_output_node pdg]
* to the returned list of nodes.
*)
- if !Db.Properties.Interp.to_result_from_pred p then
+ if Logic_deps.to_result_from_pred p then
(Sets.find_output_node pdg)::nodes
else nodes
in nodes,deps
let find_fun_variant_nodes pdg t =
let f_interpret kf =
- let f_ctx = !Db.Properties.Interp.To_zone.mk_ctx_func_contrat
- ~state_opt:(Some true) kf in
- !Db.Properties.Interp.To_zone.from_term t f_ctx
+ let f_ctx = Logic_deps.mk_ctx_func_contract ~before:true kf in
+ Logic_deps.from_term t f_ctx
in find_nodes_for_function_contract pdg f_interpret
let find_code_annot_nodes pdg stmt annot =
@@ -112,11 +109,11 @@ let find_code_annot_nodes pdg stmt annot =
begin
let kf = PdgTypes.Pdg.get_kf pdg in
let (data_info, decl_label_info), pragmas =
- !Db.Properties.Interp.To_zone.from_stmt_annot annot (stmt, kf)
+ Logic_deps.from_stmt_annot annot (stmt, kf)
in
let data_dpds = zone_info_nodes pdg data_info in
- let decl_nodes = get_decl_nodes pdg decl_label_info.Db.Properties.Interp.To_zone.var in
- let labels = decl_label_info.Db.Properties.Interp.To_zone.lbl in
+ let decl_nodes = get_decl_nodes pdg decl_label_info.Logic_deps.var in
+ let labels = decl_label_info.Logic_deps.lbl in
let stmt_key = Key.stmt_key stmt in
let stmt_node = match stmt_key with
| Key.Stmt _ -> Sets.find_stmt_node pdg stmt
@@ -130,7 +127,7 @@ let find_code_annot_nodes pdg stmt annot =
in
(* can safely ignore pragmas.ctrl
* because we already have the ctrl dpds from the stmt node. *)
- let stmt_pragmas = pragmas.Db.Properties.Interp.To_zone.stmt in
+ let stmt_pragmas = pragmas.Logic_deps.stmt in
let ctrl_dpds = Stmt.Set.fold add_stmt_nodes stmt_pragmas ctrl_dpds in
let add_label_nodes l acc = match l with
| StmtLabel stmt ->
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index 4c806545b623c8a67acf61c01b88d467f5eef64c..fb75aea9329b888d89e3f8d285cb77e4719a85e6 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -428,9 +428,9 @@ exception ToDo
let get_annot_zone kf stmt annot =
let add_zone z info =
- let s = info.Db.Properties.Interp.To_zone.ki in
- let before = info.Db.Properties.Interp.To_zone.before in
- let zone = info.Db.Properties.Interp.To_zone.zone in
+ let s = info.Logic_deps.ki in
+ let before = info.Logic_deps.before in
+ let zone = info.Logic_deps.zone in
R.debug ~level:2 "[forward_prop_scope] need %a %s stmt %d@."
Locations.Zone.pretty zone
(if before then "before" else "after") s.sid;
@@ -439,9 +439,7 @@ let get_annot_zone kf stmt annot =
else (* TODO *)
raise ToDo
in
- let (info, _), _ =
- !Db.Properties.Interp.To_zone.from_stmt_annot annot (stmt, kf)
- in
+ let (info, _), _ = Logic_deps.from_stmt_annot annot (stmt, kf) in
match info with
| None -> raise ToDo
| Some info ->
diff --git a/src/plugins/scope/gui/dpds_gui.ml b/src/plugins/scope/gui/dpds_gui.ml
index aa096ad902f723e0dbbeb68ef3416d65f8828e47..9dac7c1995da8278845ecc7f99ba61c555c1d0f1 100644
--- a/src/plugins/scope/gui/dpds_gui.ml
+++ b/src/plugins/scope/gui/dpds_gui.ml
@@ -55,9 +55,9 @@ let ask_for_lval (main_ui:Design.main_window_extension_points) kf =
match txt with None | Some "" -> None
| Some txt ->
try
- let term_lval = !Db.Properties.Interp.term_lval kf txt in
+ let term_lval = Logic_parse_string.term_lval kf txt in
let lval =
- !Db.Properties.Interp.term_lval_to_lval ~result:None term_lval
+ Logic_to_c.term_lval_to_lval term_lval
in
Some (txt, lval)
with e ->
@@ -77,9 +77,7 @@ let get_lval_opt main_ui kf_opt localizable =
Some (lv_txt, lv)
| PTermLval (Some _kf, Kstmt _stmt, _, tlv) -> begin
try
- let lv =
- !Db.Properties.Interp.term_lval_to_lval ~result:None tlv
- in
+ let lv = Logic_to_c.term_lval_to_lval tlv in
let lv_txt = Format.asprintf "%a" Printer.pp_term_lval tlv in
Some (lv_txt, lv)
with Invalid_argument _ -> None
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 1abf9ab1efbf4e4770fe1f41c422085f0397eef8..4427387a682885b0b42fc8e940f44da9364be553 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -41,8 +41,8 @@ module Cache = Hashtbl.Make(Key)
let get_term kf term =
let env = logic_environment () in
- try Some (!Db.Properties.Interp.term ~env kf term)
- with Logic_interp.Error _ | Parsing.Parse_error -> None
+ try Some (Logic_parse_string.term ~env kf term)
+ with Logic_parse_string.Error _ | Parsing.Parse_error -> None
let key_of_localizable =
let open Printer_tag in
@@ -819,12 +819,12 @@ let build_marker =
Option.map @@ fun input ->
let env = logic_environment () in
let kf = Kernel_function.find_englobing_kf input.atStmt in
- let term = !Db.Properties.Interp.term ~env kf input.term in
+ let term = Logic_parse_string.term ~env kf input.term in
let key = (input.atStmt, term) in
match Cache.find_opt cache key with
| Some tag -> tag
| None ->
- let exp = !Db.Properties.Interp.term_to_exp ~result:None term in
+ let exp = Logic_to_c.term_to_exp term in
let tag = Printer_tag.PExp (Some kf, Kstmt input.atStmt, exp) in
Cache.add cache key tag ; tag
diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml
index 7bdf6c01161551dac897a8076f0e7664630573f4..8b8b3944fd7b0f9f909c80b45285f440c5bcc763 100644
--- a/src/plugins/slicing/slicingCmds.ml
+++ b/src/plugins/slicing/slicingCmds.ml
@@ -316,9 +316,9 @@ let select_stmt_lval set mark lval_str ~before ki ~eval kf =
let zone =
Datatype.String.Set.fold
(fun lval_str acc ->
- let lval_term = !Db.Properties.Interp.term_lval kf lval_str in
+ let lval_term = Logic_parse_string.term_lval kf lval_str in
let lval =
- !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term
+ Logic_to_c.term_lval_to_lval lval_term
in
let zone = get_lval_zone eval lval in
Locations.Zone.join zone acc)
@@ -347,8 +347,8 @@ let select_lval_rw set mark ~rd ~wr ~eval kf ki_opt=
let zone =
Datatype.String.Set.fold
(fun lval_str acc ->
- let lval_term = !Db.Properties.Interp.term_lval kf lval_str in
- let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
+ let lval_term = Logic_parse_string.term_lval kf lval_str in
+ let lval = Logic_to_c.term_lval_to_lval lval_term in
let zone = get_lval_zone ~for_writing eval lval in
Locations.Zone.join zone acc)
lval_str Locations.Zone.bottom
@@ -437,19 +437,19 @@ let select_ZoneAnnot_pragmas set ~spare pragmas kf =
Cil_datatype.Stmt.Set.fold
(* selection related to statement assign and //@ slice pragma stmt *)
(fun ki' acc -> select_stmt acc ~spare ki' kf)
- pragmas.Db.Properties.Interp.To_zone.stmt set
+ pragmas.Logic_deps.stmt set
in
Cil_datatype.Stmt.Set.fold
(* selection related to //@ slice pragma ctrl/expr *)
(fun ki' acc -> select_stmt_ctrl acc ~spare ki' kf)
- pragmas.Db.Properties.Interp.To_zone.ctrl
+ pragmas.Logic_deps.ctrl
set
let select_ZoneAnnot_zones_decl_vars set mark (zones,decl_vars) kf =
let set =
Cil_datatype.Varinfo.Set.fold
(fun vi acc -> select_decl_var acc mark vi kf)
- decl_vars.Db.Properties.Interp.To_zone.var
+ decl_vars.Logic_deps.var
set
in
let set =
@@ -457,16 +457,16 @@ let select_ZoneAnnot_zones_decl_vars set mark (zones,decl_vars) kf =
(fun l acc ->
let selection = SlicingSelect.select_label kf l mark
in add_to_selection acc selection)
- decl_vars.Db.Properties.Interp.To_zone.lbl
+ decl_vars.Logic_deps.lbl
set
in
List.fold_right
(fun z acc ->
(* selection related to the parsing/compilation of the annotation *)
select_stmt_zone acc mark
- z.Db.Properties.Interp.To_zone.zone
- ~before:z.Db.Properties.Interp.To_zone.before
- z.Db.Properties.Interp.To_zone.ki
+ z.Logic_deps.zone
+ ~before:z.Logic_deps.before
+ z.Logic_deps.ki
kf)
zones set
@@ -474,7 +474,7 @@ let get_or_raise (info_data_opt, info_decl) = match info_data_opt with
| None ->
(* TODO: maybe we can know how to use [info_decl] ? *)
SlicingParameters.not_yet_implemented
- "%s" !Logic_interp.To_zone.not_yet_implemented
+ "%s" !Logic_deps.not_yet_implemented
| Some info_data -> info_data, info_decl
(** Registered as a slicing selection function:
@@ -482,8 +482,7 @@ let get_or_raise (info_data_opt, info_decl) = match info_data_opt with
Note: add also a transparent selection on the whole statement. *)
let select_stmt_pred set mark pred ki kf =
let zones_decl_vars =
- !Db.Properties.Interp.To_zone.from_pred pred
- (!Db.Properties.Interp.To_zone.mk_ctx_stmt_annot kf ki)
+ Logic_deps.from_pred pred (Logic_deps.mk_ctx_stmt_annot kf ki)
in
select_ZoneAnnot_zones_decl_vars set mark (get_or_raise zones_decl_vars) kf
@@ -492,8 +491,7 @@ let select_stmt_pred set mark pred ki kf =
Note: add also a transparent selection on the whole statement. *)
let select_stmt_term set mark term ki kf =
let zones_decl_vars =
- !Db.Properties.Interp.To_zone.from_term term
- (!Db.Properties.Interp.To_zone.mk_ctx_stmt_annot kf ki)
+ Logic_deps.from_term term (Logic_deps.mk_ctx_stmt_annot kf ki)
in
select_ZoneAnnot_zones_decl_vars set mark (get_or_raise zones_decl_vars) kf
@@ -502,7 +500,7 @@ let select_stmt_term set mark term ki kf =
Note: add also a transparent selection on the whole statement. *)
let select_stmt_annot set mark ~spare annot ki kf =
let zones_decl_vars,pragmas =
- !Db.Properties.Interp.To_zone.from_stmt_annot annot (ki, kf)
+ Logic_deps.from_stmt_annot annot (ki, kf)
in let set = select_ZoneAnnot_pragmas set ~spare pragmas kf
in select_ZoneAnnot_zones_decl_vars set mark (get_or_raise zones_decl_vars) kf
@@ -511,8 +509,8 @@ let select_stmt_annot set mark ~spare annot ki kf =
Note: add also a transparent selection on the whole statement. *)
let select_stmt_annots set mark ~spare ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop_var ki kf =
let zones_decl_vars,pragmas =
- !Db.Properties.Interp.To_zone.from_stmt_annots
- (Some (!Db.Properties.Interp.To_zone.code_annot_filter
+ Logic_deps.from_stmt_annots
+ (Some (Logic_deps.code_annot_filter
~threat ~user_assert ~slicing_pragma
~loop_inv ~loop_var ~others:false))
(ki, kf)
@@ -524,9 +522,9 @@ let select_stmt_annots set mark ~spare ~threat ~user_assert ~slicing_pragma ~lo
let select_func_annots set mark ~spare ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop_var kf =
try
let zones_decl_vars,pragmas =
- !Db.Properties.Interp.To_zone.from_func_annots Kinstr.iter_from_func
+ Logic_deps.from_func_annots Kinstr.iter_from_func
(Some
- (!Db.Properties.Interp.To_zone.code_annot_filter
+ (Logic_deps.code_annot_filter
~threat ~user_assert ~slicing_pragma ~loop_inv
~loop_var ~others:false))
kf
@@ -685,7 +683,7 @@ let add_persistent_cmdline () =
SlicingParameters.Select.WrAccess.clear () ;
end;
add_persistent_selection !selection;
- with Logic_interp.Error(_loc,msg) ->
+ with Logic_parse_string.Error(_loc,msg) ->
SlicingParameters.warning ~wkey:SlicingParameters.wkey_cmdline
"%s. Slicing requests from the command line are ignored." msg
end;
diff --git a/src/plugins/slicing/slicingTransform.ml b/src/plugins/slicing/slicingTransform.ml
index 2915223eec08c36ed39b517038169b951525e899..9bba77427e608749ec3b569c40433dfe6cba409b 100644
--- a/src/plugins/slicing/slicingTransform.ml
+++ b/src/plugins/slicing/slicingTransform.ml
@@ -260,7 +260,7 @@ module Visibility (SliceName : sig
SlicingParameters.debug ~level:2
"[SlicingTransform.Visibility.annotation_visible] \
not implemented -> invisible"; false
- | Logic_interp.To_zone.NYI msg ->
+ | Logic_deps.NYI msg ->
SlicingParameters.warning ~current:true ~once:true
"Dropping unsupported ACSL annotation";
SlicingParameters.debug ~level:2
diff --git a/src/plugins/sparecode/spare_marks.ml b/src/plugins/sparecode/spare_marks.ml
index bc433062ccc8929f0be579864f7878a07a6f8cee..cdf9349121c2583c00be620840f9a98bfb1a7006 100644
--- a/src/plugins/sparecode/spare_marks.ml
+++ b/src/plugins/sparecode/spare_marks.ml
@@ -314,7 +314,7 @@ class annot_visitor ~filter pdg = object (self)
to_select <- add_nodes_and_undef_to_select true info to_select
with
Not_found -> () (* unreachable *)
- | Logic_interp.To_zone.NYI _ ->
+ | Logic_deps.NYI _ ->
Sparecode_params.warning ~current:true ~once:true
"Dropping annotation";
()
diff --git a/src/plugins/studia/gui/studia_gui.ml b/src/plugins/studia/gui/studia_gui.ml
index 0abf647801ac257e643f8ca71ad62cb79623fbf5..416743fba1d02b46a776581906f7ab0caff015b2 100644
--- a/src/plugins/studia/gui/studia_gui.ml
+++ b/src/plugins/studia/gui/studia_gui.ml
@@ -42,7 +42,7 @@ let ask_for_lval (main_ui:Design.main_window_extension_points) kf =
match txt with None | Some "" -> None
| Some txt ->
try
- let term_lval = !Db.Properties.Interp.term_lval kf txt in
+ let term_lval = Logic_parse_string.term_lval kf txt in
Some (txt, term_lval)
with e ->
main_ui#error "[ask for lval] '%s' invalid expression: %s@."
diff --git a/tests/misc/bts1347.ml b/tests/misc/bts1347.ml
index d7196ae5940a4fc1316bb328207cfdc4044e0803..ea417ba7710a999aa54681cf88770f622473b46f 100644
--- a/tests/misc/bts1347.ml
+++ b/tests/misc/bts1347.ml
@@ -18,7 +18,7 @@ let run () =
[]
in
let s = Kernel_function.find_return kf in
- let ca = !Db.Properties.Interp.code_annot kf s "assert 32.5>=10.;" in
+ let ca = Logic_parse_string.code_annot kf s "assert 32.5>=10.;" in
Annotations.add_code_annot emitter ~kf s ca;
let ip = Property.ip_of_code_annot_single kf s ca in
Property_status.emit emitter ~hyps ip Property_status.True
diff --git a/tests/pdg/dyn_dpds.ml b/tests/pdg/dyn_dpds.ml
index 402616dac4b83282d03f51ba07270078fd889677..5bf2774757d4402519d82ae1590fef2b179ca7ea 100644
--- a/tests/pdg/dyn_dpds.ml
+++ b/tests/pdg/dyn_dpds.ml
@@ -6,8 +6,8 @@ zgrviewer tests/pdg/dyn_dpds_2.dot ;
*)
let get_zones str_data (stmt, kf) =
- let lval_term = !Db.Properties.Interp.term_lval kf str_data in
- let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
+ let lval_term = Logic_parse_string.term_lval kf str_data in
+ let lval = Logic_to_c.term_lval_to_lval lval_term in
let exp = Cil.new_exp ~loc:Cil_datatype.Location.unknown (Cil_types.Lval lval) in
Eva.Results.(before stmt |> expr_deps exp)
diff --git a/tests/scope/bts971.ml b/tests/scope/bts971.ml
index 5a4231067b4463e3e5e1647b6eb1acdb39d278fc..308f4e84faac142bf859f27f65f499b5d4aa70fc 100644
--- a/tests/scope/bts971.ml
+++ b/tests/scope/bts971.ml
@@ -8,8 +8,8 @@ let find_pp kf_name =
let compute_and_print pp str_data =
let stmt, kf = pp in
- let lval_term = !Db.Properties.Interp.term_lval kf str_data in
- let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
+ let lval_term = Logic_parse_string.term_lval kf str_data in
+ let lval = Logic_to_c.term_lval_to_lval lval_term in
let defs = Scope.Defs.get_defs kf stmt lval in
Format.printf "* @[<v 2>Defs for (%s) at current program point=@[<v 2>@."
str_data;
diff --git a/tests/scope/zones.ml b/tests/scope/zones.ml
index 1e06b3584e36988ad6886ac41835386b5d0a74f2..44c8841ce20ff11081d17df4ce27678a661ef8a5 100644
--- a/tests/scope/zones.ml
+++ b/tests/scope/zones.ml
@@ -35,8 +35,8 @@ let find_label kf_name lab_name =
let compute_and_print pp str_data =
let stmt, kf = pp in
- let lval_term = !Db.Properties.Interp.term_lval kf str_data in
- let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
+ let lval_term = Logic_parse_string.term_lval kf str_data in
+ let lval = Logic_to_c.term_lval_to_lval lval_term in
let (_used_stmts, zones) = Scope.Zones.build_zones kf stmt lval in
Format.printf "Zones for %s at current program point =@.%a\n@\n"
str_data Scope.Zones.pretty_zones zones
diff --git a/tests/slicing/libSelect.ml b/tests/slicing/libSelect.ml
index f7eb9feb2d4d8f570fac58f298a24a3cef441a36..09aed9706740778962c1c6659d66b083a4214ed1 100644
--- a/tests/slicing/libSelect.ml
+++ b/tests/slicing/libSelect.ml
@@ -74,8 +74,8 @@ let get_stmt sid = fst (Kernel_function.find_from_sid sid)
(** build the [zone] which represents [data] before [kinst] *)
let get_zones str_data (stmt, kf) =
- let lval_term = !Db.Properties.Interp.term_lval kf str_data in
- let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
+ let lval_term = Logic_parse_string.term_lval kf str_data in
+ let lval = Logic_to_c.term_lval_to_lval lval_term in
let loc = Eva.Results.(before stmt |> eval_address lval |> as_location) in
Locations.(enumerate_valid_bits Read loc)
;;