diff --git a/Makefile b/Makefile
index 5c8a9a2b9f15054e4fd3e7219bba502eef91cc87..f88ac42621097efd24a58aeb773cec7e6ea0125a 100644
--- a/Makefile
+++ b/Makefile
@@ -576,6 +576,7 @@ KERNEL_CMO=\
src/kernel_services/abstract_interp/lmap_bitwise.cmo \
src/kernel_services/visitors/visitor.cmo \
src/kernel_services/ast_data/statuses_by_call.cmo \
+ src/kernel_services/ast_printing/printer_tag.cmo \
$(PLUGIN_TYPES_CMO_LIST) \
src/kernel_services/plugin_entry_points/db.cmo \
src/libraries/utils/command.cmo \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 43be8eb708ab85c08c4cac5f985bcb17876bbc51..bd2f620f30888cf870d2a2fc03e33b986398352f 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -502,6 +502,8 @@ src/kernel_services/ast_printing/printer.mli: CEA_LGPL
src/kernel_services/ast_printing/printer_api.mli: CEA_LGPL
src/kernel_services/ast_printing/printer_builder.ml: CEA_LGPL
src/kernel_services/ast_printing/printer_builder.mli: CEA_LGPL
+src/kernel_services/ast_printing/printer_tag.ml: CEA_LGPL
+src/kernel_services/ast_printing/printer_tag.mli: CEA_LGPL
src/kernel_services/ast_queries/README.md: .ignore
src/kernel_services/ast_queries/ast_info.ml: CEA_LGPL
src/kernel_services/ast_queries/ast_info.mli: CEA_LGPL
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
new file mode 100644
index 0000000000000000000000000000000000000000..023b14d756ba29bfdb59887a107e17a6915b6c1c
--- /dev/null
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -0,0 +1,547 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Localizable API --- *)
+(* -------------------------------------------------------------------------- *)
+
+open Cil_types
+open Cil_datatype
+
+type localizable =
+ | PStmt of (kernel_function * stmt)
+ | PStmtStart of (kernel_function * stmt)
+ | PLval of (kernel_function option * kinstr * lval)
+ | PExp of (kernel_function option * kinstr * exp)
+ | PTermLval of (kernel_function option * kinstr * Property.t * term_lval)
+ | PVDecl of (kernel_function option * kinstr * varinfo)
+ | PGlobal of global
+ | PIP of Property.t
+
+module Localizable =
+ Datatype.Make
+ (struct
+ include Datatype.Undefined
+ type t = localizable
+
+ let name = "Printer_tag.Localizable"
+ let reprs = List.map (fun g -> PGlobal g) Global.reprs
+ let mem_project = Datatype.never_any_project
+
+ let hash = function
+ | PStmtStart (_,s) ->
+ Hashtbl.hash( 0, Stmt.hash s )
+ | PStmt (_,s) ->
+ Hashtbl.hash( 1, Stmt.hash s )
+ | PLval (_,ki,lv) ->
+ Hashtbl.hash( 2, Kinstr.hash ki, Lval.hash lv )
+ | PTermLval(_,ki,pi,lv) ->
+ Hashtbl.hash( 3, Kinstr.hash ki, Property.hash pi, Term_lval.hash lv)
+ | PVDecl(_,_,v) ->
+ Hashtbl.hash( 4, Varinfo.hash v )
+ | PExp(_,_,e) ->
+ Hashtbl.hash( 5, Exp.hash e )
+ | PIP ip ->
+ Hashtbl.hash( 6, Property.hash ip )
+ | PGlobal g ->
+ Hashtbl.hash( 7, Global.hash g )
+
+ let equal l1 l2 = match l1,l2 with
+ | PStmt (_,ki1), PStmt (_,ki2) -> ki1.sid = ki2.sid
+ | PStmtStart (_,ki1), PStmtStart (_,ki2) -> ki1.sid = ki2.sid
+ | PLval (_,ki1,lv1), PLval (_,ki2,lv2) ->
+ Kinstr.equal ki1 ki2 && lv1 == lv2
+ | PTermLval (_,ki1,pi1,lv1), PTermLval (_,ki2,pi2,lv2) ->
+ Kinstr.equal ki1 ki2 && Property.equal pi1 pi2 &&
+ Logic_utils.is_same_tlval lv1 lv2
+ (* [JS 2008/01/21] term_lval are not shared: cannot use == *)
+ | PVDecl (_,_,v1), PVDecl (_,_,v2) -> Varinfo.equal v1 v2
+ | PExp (_,_,e1), PExp(_,_,e2) -> Exp.equal e1 e2
+ | PIP ip1, PIP ip2 -> Property.equal ip1 ip2
+ | PGlobal g1, PGlobal g2 -> Global.equal g1 g2
+ | (PStmt _ | PStmtStart _ | PLval _ | PExp _ | PTermLval _ | PVDecl _
+ | PIP _ | PGlobal _), _
+ -> false
+
+ let pp_ki_loc fmt ki =
+ match ki with
+ | Kglobal -> (* no location, print 'global' *)
+ Format.fprintf fmt "global"
+ | Kstmt st ->
+ Cil_datatype.Location.pretty fmt (Stmt.loc st)
+
+ let pretty fmt = function
+ | PStmtStart (_, s) ->
+ Format.fprintf fmt "LocalizableStart %d (%a)"
+ s.sid Printer.pp_location (Cil_datatype.Stmt.loc s)
+ | PStmt (_, s) ->
+ Format.fprintf fmt "LocalizableStmt %d (%a)"
+ s.sid Printer.pp_location (Cil_datatype.Stmt.loc s)
+ | PLval (_, ki, lv) ->
+ Format.fprintf fmt "LocalizableLval %a (%a)"
+ Printer.pp_lval lv pp_ki_loc ki
+ | PExp (_, ki, lv) ->
+ Format.fprintf fmt "LocalizableExp %a (%a)"
+ Printer.pp_exp lv pp_ki_loc ki
+ | PTermLval (_, ki, _pi, tlv) ->
+ Format.fprintf fmt "LocalizableTermLval %a (%a)"
+ Printer.pp_term_lval tlv pp_ki_loc ki
+ | PVDecl (_, _, vi) ->
+ Format.fprintf fmt "LocalizableVDecl %a" Printer.pp_varinfo vi
+ | PGlobal g ->
+ Format.fprintf fmt "LocalizableGlobal %a" Printer.pp_global g
+ | PIP ip ->
+ Format.fprintf fmt "LocalizableIP %a" Description.pp_property ip
+ end)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Utility Accessors --- *)
+(* -------------------------------------------------------------------------- *)
+
+let kf_of_localizable loc =
+ match loc with
+ | PLval (kf_opt, _, _)
+ | PExp (kf_opt,_,_)
+ | PTermLval(kf_opt, _,_,_)
+ | PVDecl (kf_opt, _, _) -> kf_opt
+ | PStmt (kf, _) | PStmtStart(kf,_) -> Some kf
+ | PIP ip -> Property.get_kf ip
+ | PGlobal (GFun ({svar = vi}, _)) -> Some (Globals.Functions.get vi)
+ | PGlobal _ -> None
+
+let ki_of_localizable loc = match loc with
+ | PLval (_, ki, _)
+ | PExp (_, ki, _)
+ | PTermLval(_, ki,_,_)
+ | PVDecl (_, ki, _) -> ki
+ | PStmt (_, st) | PStmtStart(_, st) -> Kstmt st
+ | PIP ip -> Property.get_kinstr ip
+ | PGlobal _ -> Kglobal
+
+let varinfo_of_localizable loc =
+ match kf_of_localizable loc with
+ | Some kf -> Some (Kernel_function.get_vi kf)
+ | None ->
+ match loc with
+ | PGlobal (GVar (vi, _, _) | GVarDecl (vi, _)
+ | GFunDecl (_, vi, _) | GFun ({svar = vi }, _)) -> Some vi
+ | _ -> None
+
+let loc_of_localizable = function
+ | PStmt (_,st) | PStmtStart(_,st)
+ | PLval (_,Kstmt st,_) | PExp(_,Kstmt st, _)
+ | PTermLval(_,Kstmt st,_,_) ->
+ Stmt.loc st
+ | PIP ip ->
+ (match Property.get_kinstr ip with
+ | Kglobal ->
+ (match Property.get_kf ip with
+ None -> Location.unknown
+ | Some kf -> Kernel_function.get_location kf)
+ | Kstmt st -> Stmt.loc st)
+ | PVDecl (_,_,vi) -> vi.vdecl
+ | PGlobal g -> Global.loc g
+ | (PLval _ | PTermLval _ | PExp _) as localize ->
+ (match kf_of_localizable localize with
+ | None -> Location.unknown
+ | Some kf -> Kernel_function.get_location kf)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Printer API --- *)
+(* -------------------------------------------------------------------------- *)
+
+module type TAG =
+sig
+ val create : localizable -> string
+ val unfold : stmt -> bool
+end
+
+(* We delay the creation of the class to execution time, so that all
+ pretty-printer extensions get properly registered (as we want to inherit
+ from them). The only known solution is to use a functor *)
+module BUILD(Tag : TAG)(X: Printer.PrinterClass) : Printer.PrinterClass =
+struct
+
+ class printer : Printer.extensible_printer = object(self)
+
+ inherit X.printer as super
+
+ val mutable current_property = None
+
+ method private current_kinstr =
+ match self#current_stmt with
+ | None -> Kglobal
+ | Some st -> Kstmt st
+
+ method private current_sid =
+ match super#current_stmt with
+ | None -> assert false
+ | Some st -> st.sid
+
+ method private current_kf =
+ match super#current_function with
+ | None -> None
+ | Some fd -> Some (Globals.Functions.get fd)
+
+ val mutable current_ca = None
+
+ val mutable active_behaviors = []
+
+ method private current_behavior_or_loop =
+ match current_ca with
+ None ->
+ let active = Datatype.String.Set.of_list active_behaviors in
+ Property.Id_contract (active ,Extlib.the self#current_behavior)
+ | Some ca -> Property.Id_loop ca
+
+ (* When [stmt] is a call, this method "inlines" the preconditions of the
+ functions that may be called here, with some context. This way,
+ bullets are more precise, etc. *)
+ method private preconditions_at_call fmt stmt =
+ match stmt.skind with
+ | Instr (Call _)
+ | Instr (Local_init (_, ConsInit _, _)) ->
+ let extract_instance_predicate = function
+ | Property.IPPropertyInstance (_kf, _stmt, pred, _prop) -> pred
+ (* Other cases should not happen, unless a plugin has replaced call
+ preconditions. In this case, print nothing but do not crash. *)
+ | _ -> raise Not_found
+ in
+ let extract_predicate = function
+ | Property.IPPredicate (_, _, _, p) -> p
+ | _ -> assert false
+ in
+ (* Functons called at this point *)
+ let called = Statuses_by_call.all_functions_with_preconditions stmt in
+ let warn_missing = false in
+ let add_by_kf kf acc =
+ let ips =
+ Statuses_by_call.all_call_preconditions_at ~warn_missing kf stmt
+ in
+ if ips = [] then acc else (kf, ips) :: acc
+ in
+ let ips_all_kfs = Kernel_function.Hptset.fold add_by_kf called [] in
+ let pp_one fmt (original_p, p) =
+ match extract_instance_predicate p with
+ | Some pred -> Format.fprintf fmt "@[%a@]" self#requires_aux (p, pred)
+ | None ->
+ let pred = extract_predicate original_p in
+ (* Makes the original predicate non clickable, as it may involve
+ the formal parameters which are not in scope at the call site. *)
+ Format.fprintf fmt "@[Non transposable: %s@]"
+ (Format.asprintf "@[%a@]" self#requires_aux (original_p, pred))
+ | exception Not_found -> ()
+ in
+ let pp_by_kf fmt (kf, ips) =
+ Format.fprintf fmt "@[preconditions of %a:@]@ %a"
+ Kernel_function.pretty kf
+ (Pretty_utils.pp_list ~pre:"" ~sep:"@ " ~suf:"" pp_one) ips
+ in
+ if ips_all_kfs <> [] then
+ Pretty_utils.pp_list ~pre:"@[<v 3>/* " ~sep:"@ " ~suf:" */@]@ "
+ pp_by_kf fmt ips_all_kfs
+ | _ -> ()
+
+
+ method! next_stmt next fmt current =
+ if Tag.unfold current
+ then self#preconditions_at_call fmt current;
+ Format.fprintf fmt "@{<%s>%a@}"
+ (Tag.create (PStmt (Extlib.the self#current_kf,current)))
+ (super#next_stmt next) current
+
+ method! lval fmt lv =
+ match self#current_kinstr with
+ | Kglobal -> super#lval fmt lv
+ (* Do not highlight the lvals in initializers. *)
+ | Kstmt _ as ki ->
+ Format.fprintf fmt "@{<%s>"
+ (Tag.create (PLval (self#current_kf,ki,lv)));
+ (match lv with
+ | Var vi, (Field _| Index _ as o) ->
+ (* Small hack to be able to click on the arrays themselves
+ in the easy cases *)
+ self#lval fmt (Var vi, NoOffset);
+ self#offset fmt o
+ | _ -> super#lval fmt lv
+ );
+ Format.fprintf fmt "@}"
+
+ method! exp fmt e =
+ match e.enode with
+ | Lval lv ->
+ (* Do not mark immediate l-values as they would not be
+ selectable anyway because of the embedded tags of self#lval.
+ This is only an optimization. *)
+ self#lval fmt lv
+ | _ ->
+ Format.fprintf fmt "@{<%s>"
+ (Tag.create (PExp (self#current_kf,self#current_kinstr,e)));
+ super#exp fmt e;
+ Format.fprintf fmt "@}"
+
+ method! term_lval fmt lv =
+ (* similar to pLval, except that term_lval can appear in specifications
+ of functions (ki = None, kf <> None). Initializers are ignored. *)
+ if self#current_kinstr = Kglobal && self#current_kf = None then begin
+ super#term_lval fmt lv (* Do not highlight the lvals in initializers. *)
+ end else begin
+ match current_property with
+ | None -> (* Also use default printer for this case (possible inside
+ pragmas, for example). *)
+ super#term_lval fmt lv
+ | Some ip ->
+ Format.fprintf fmt "@{<%s>"
+ (Tag.create
+ (PTermLval (self#current_kf, self#current_kinstr, ip, lv)));
+ (match lv with
+ | TVar vi, (TField _| TIndex _ as o) ->
+ self#term_lval fmt (TVar vi, TNoOffset);
+ self#term_offset fmt o
+ | _ -> super#term_lval fmt lv
+ );
+ Format.fprintf fmt "@}"
+ end
+
+ method! vdecl fmt vi =
+ Format.fprintf fmt "@{<%s>%a@}"
+ (Tag.create (PVDecl (self#current_kf, self#current_kinstr, vi)))
+ super#vdecl vi
+
+ method private tag_property p =
+ current_property <- Some p;
+ Tag.create (PIP p)
+
+ method! code_annotation fmt ca =
+ match ca.annot_content with
+ | APragma p when not (Logic_utils.is_property_pragma p) ->
+ (* Not currently localizable. Will be linked to the next stmt *)
+ super#code_annotation fmt ca
+ | AAssert _ | AInvariant _ | APragma _ | AVariant _ ->
+ let ip =
+ Property.ip_of_code_annot_single
+ (Extlib.the self#current_kf)
+ (Extlib.the self#current_stmt)
+ ca
+ in
+ Format.fprintf fmt "@{<%s>%a@}"
+ (self#tag_property ip)
+ super#code_annotation ca;
+ | AStmtSpec (active,_) | AExtended(active,_,_) ->
+ (* tags will be set in the inner nodes. *)
+ active_behaviors <- active;
+ super#code_annotation fmt ca;
+ active_behaviors <- [];
+ | AAllocation _
+ | AAssigns _ ->
+ (* tags will be set in the inner nodes. *)
+ current_ca <- Some ca;
+ super#code_annotation fmt ca;
+ current_ca <- None
+
+ method! global fmt g =
+ match g with
+ (* these globals are already covered by PVDecl *)
+ | GVarDecl _ | GVar _ | GFunDecl _ | GFun _ -> super#global fmt g
+ | _ ->
+ Format.fprintf fmt "@{<%s>%a@}"
+ (Tag.create (PGlobal g))
+ super#global
+ g
+
+ method! extended fmt ext =
+ let loc =
+ match self#current_kf with
+ | None -> Property.ELGlob
+ | Some kf -> Property.e_loc_of_stmt kf self#current_kinstr
+ in
+ Format.fprintf fmt "@{<%s>%a@}"
+ (self#tag_property Property.(ip_of_extended loc ext))
+ super#extended ext;
+
+ method private requires_aux fmt (ip, p) =
+ Format.fprintf fmt "@{<%s>%a@}"
+ (self#tag_property ip)
+ super#requires p;
+
+ method! requires fmt p =
+ let b = Extlib.the self#current_behavior in
+ let ip =
+ Property.ip_of_requires
+ (Extlib.the self#current_kf) self#current_kinstr b p
+ in
+ self#requires_aux fmt (ip, p)
+
+ method! behavior fmt b =
+ Format.fprintf fmt "@{<%s>%a@}"
+ (self#tag_property
+ (Property.ip_of_behavior
+ (Extlib.the self#current_kf)
+ self#current_kinstr
+ active_behaviors b))
+ super#behavior b
+
+ method! decreases fmt t =
+ Format.fprintf fmt "@{<%s>%a@}"
+ (self#tag_property
+ (Property.ip_of_decreases
+ (Extlib.the self#current_kf) self#current_kinstr t))
+ super#decreases t;
+
+ method! terminates fmt t =
+ Format.fprintf fmt "@{<%s>%a@}"
+ (self#tag_property
+ (Property.ip_of_terminates
+ (Extlib.the self#current_kf) self#current_kinstr t))
+ super#terminates t;
+
+ method! complete_behaviors fmt t =
+ Format.fprintf fmt "@{<%s>%a@}"
+ (self#tag_property
+ (Property.ip_of_complete
+ (Extlib.the self#current_kf)
+ self#current_kinstr
+ active_behaviors
+ t))
+ super#complete_behaviors t
+
+ method! disjoint_behaviors fmt t =
+ Format.fprintf fmt "@{<%s>%a@}"
+ (self#tag_property
+ (Property.ip_of_disjoint
+ (Extlib.the self#current_kf)
+ self#current_kinstr
+ active_behaviors
+ t))
+ super#disjoint_behaviors t
+
+ method! assumes fmt p =
+ let b = Extlib.the self#current_behavior in
+ Format.fprintf fmt "@{<%s>%a@}"
+ (self#tag_property
+ (Property.ip_of_assumes
+ (Extlib.the self#current_kf) self#current_kinstr b p))
+ super#assumes p;
+
+ method! post_cond fmt pc =
+ let b = Extlib.the self#current_behavior in
+ Format.fprintf fmt "@{<%s>%a@}"
+ (self#tag_property
+ (Property.ip_of_ensures
+ (Extlib.the self#current_kf) self#current_kinstr b pc))
+ super#post_cond pc;
+
+ method! assigns s fmt a =
+ match
+ Property.ip_of_assigns (Extlib.the self#current_kf) self#current_kinstr
+ self#current_behavior_or_loop a
+ with
+ None -> super#assigns s fmt a
+ | Some ip ->
+ Format.fprintf fmt "@{<%s>%a@}"
+ (self#tag_property ip) (super#assigns s) a
+
+ method! from s fmt ((_, f) as from) =
+ match f with
+ | FromAny -> super#from s fmt from
+ | From _ ->
+ let ip =
+ Extlib.the
+ (Property.ip_of_from
+ (Extlib.the self#current_kf) self#current_kinstr
+ self#current_behavior_or_loop from)
+ in
+ Format.fprintf fmt "@{<%s>%a@}"
+ (Tag.create (PIP ip)) (super#from s) from
+
+ method! global_annotation fmt a =
+ match Property.ip_of_global_annotation_single a with
+ | None -> super#global_annotation fmt a
+ | Some ip ->
+ Format.fprintf fmt "@{<%s>%a@}"
+ (Tag.create (PIP ip)) super#global_annotation a
+
+ method! allocation ~isloop fmt a =
+ match
+ Property.ip_of_allocation (Extlib.the self#current_kf) self#current_kinstr
+ self#current_behavior_or_loop a
+ with
+ None -> super#allocation ~isloop fmt a
+ | Some ip ->
+ Format.fprintf fmt "@{<%s>%a@}"
+ (Tag.create (PIP ip)) (super#allocation ~isloop) a;
+
+ method! stmtkind sattr next fmt sk =
+ (* Special tag denoting the start of the statement, WITHOUT any ACSL
+ assertion/statement contract, etc. *)
+ let s = Extlib.the self#current_stmt in
+ let f = Extlib.the self#current_kf in
+ let tag = Tag.create (PStmtStart(f,s)) in
+ Format.fprintf fmt "@{<%s>%a@}" tag (super#stmtkind sattr next) sk
+
+ initializer force_brace <- true
+
+ end
+end
+
+module type Tag =
+sig
+ val create : localizable -> string
+end
+
+module type S_pp =
+sig
+ include Printer_api.S_pp
+ val with_unfold_precond : (stmt -> bool) ->
+ (Format.formatter -> 'a -> unit) ->
+ (Format.formatter -> 'a -> unit)
+end
+
+module Make(T : Tag) =
+struct
+
+ let unfold = ref (fun (_ : stmt) -> false)
+
+ let printer =
+ let pref : Printer.extensible_printer option ref = ref None in
+ fun () ->
+ match !pref with Some pp -> pp | None ->
+ let pp = Printer.current_printer () in
+ let module PP = (val pp: Printer.PrinterClass) in
+ let module TAG = struct
+ let create = T.create
+ let unfold s = !unfold s
+ end in
+ let module TagPrinterClass = BUILD(TAG)(PP) in
+ let printer = new TagPrinterClass.printer in
+ pref := Some printer ; printer
+
+ let with_unfold_precond unfolder f fmt x =
+ let stack = !unfold in
+ try unfold := unfolder ; f fmt x ; unfold := stack
+ with err -> unfold := stack ; raise err
+
+ include Printer_builder.Make_pp(struct let printer = printer end)
+
+end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/kernel_services/ast_printing/printer_tag.mli b/src/kernel_services/ast_printing/printer_tag.mli
new file mode 100644
index 0000000000000000000000000000000000000000..f73418ed2cdad25390cb63d18d6047b0ee14035e
--- /dev/null
+++ b/src/kernel_services/ast_printing/printer_tag.mli
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Utilities to pretty print source with located Ast elements *)
+
+open Cil_types
+
+(** The kind of object that can be selected in the source viewer. *)
+type localizable =
+ | PStmt of (kernel_function * stmt)
+ | PStmtStart of (kernel_function * stmt)
+ | PLval of (kernel_function option * kinstr * lval)
+ | PExp of (kernel_function option * kinstr * exp)
+ | PTermLval of (kernel_function option * kinstr * Property.t * term_lval)
+ | PVDecl of (kernel_function option * kinstr * varinfo)
+ (** Declaration and definition of variables and function. Check the type
+ of the varinfo to distinguish between the various possibilities.
+ If the varinfo is a global or a local, the kernel_function is the
+ one in which the variable is declared. The [kinstr] argument is given
+ for local variables with an explicit initializer. *)
+ | PGlobal of global (** all globals but variable declarations and function
+ definitions. *)
+ | PIP of Property.t
+
+module Localizable: Datatype.S with type t = localizable
+
+val kf_of_localizable : localizable -> kernel_function option
+val ki_of_localizable : localizable -> kinstr
+val varinfo_of_localizable : localizable -> varinfo option
+val loc_of_localizable : localizable -> location
+(** Might return [Location.unknown] *)
+
+module type Tag =
+sig
+ val create : localizable -> string
+end
+
+module type S_pp =
+sig
+ include Printer_api.S_pp
+ val with_unfold_precond : (stmt -> bool) ->
+ (Format.formatter -> 'a -> unit) ->
+ (Format.formatter -> 'a -> unit)
+end
+
+module Make(T : Tag) : S_pp
+
+(* -------------------------------------------------------------------------- *)