From e8177b547ffd439738a527989534a86fd741721e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 5 Feb 2019 17:02:06 +0100
Subject: [PATCH] [gui] make use of printer-tag in gui
---
src/plugins/gui/design.ml | 3 +-
src/plugins/gui/history.ml | 8 +-
src/plugins/gui/pretty_source.ml | 540 ++-----------------
src/plugins/gui/pretty_source.mli | 7 +-
src/plugins/gui/property_navigator.ml | 2 +-
src/plugins/occurrence/register_gui.ml | 2 +-
src/plugins/scope/dpds_gui.ml | 3 +-
src/plugins/security_slicing/register_gui.ml | 1 +
src/plugins/slicing/register_gui.ml | 1 +
src/plugins/value/gui_files/register_gui.ml | 3 +-
src/plugins/wp/GuiSource.ml | 5 +-
11 files changed, 66 insertions(+), 509 deletions(-)
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index e43e2bfe48d..f9e63b4bf31 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -419,6 +419,7 @@ let to_do_on_select
in
if button = 1 then begin
match selected with
+ | PStmtStart _ -> ()
| PStmt (kf, stmt) ->
current_statement_msg (Some kf) (Kstmt stmt);
print_code_annotations main_ui kf stmt;
@@ -1175,7 +1176,7 @@ class main_window () : main_window_extension_points =
varinfo or a global for [loc], then scroll to [loc]. *)
method scroll loc =
Gui_parameters.debug ~dkey:dkey_scroll
- "main_ui: scroll: localizable %a" Pretty_source.Localizable.pretty loc;
+ "main_ui: scroll: localizable %a" Printer_tag.Localizable.pretty loc;
(* Used to avoid having two different history events, one created
by [select_global], the other by [scroll] *)
let history = History.on_current_history () in
diff --git a/src/plugins/gui/history.ml b/src/plugins/gui/history.ml
index d3b93d134ab..8522852a003 100644
--- a/src/plugins/gui/history.ml
+++ b/src/plugins/gui/history.ml
@@ -37,7 +37,7 @@ module HistoryElt = struct
let equal e1 e2 = match e1, e2 with
| Global g1, Global g2 -> Cil_datatype.Global.equal g1 g2
| Localizable l1, Localizable l2 ->
- Pretty_source.Localizable.equal l1 l2
+ Printer_tag.Localizable.equal l1 l2
| (Global _ | Localizable _), __ -> false
end)
(* Identify two elements that belong to the same function *)
@@ -254,9 +254,9 @@ let translate_history_elt old_helt =
match old_helt with
| Global old_g -> global_Global old_g
| Localizable (PGlobal old_g) -> global_Global old_g
- | Localizable(PVDecl(Some kf,_,_)) ->
- global_Global (kf_to_global kf)
- | Localizable ( PStmt(kf,_) | PLval(Some kf,_,_) | PExp(Some kf,_,_)
+ | Localizable(PVDecl(Some kf,_,_)) -> global_Global (kf_to_global kf)
+ | Localizable ( PStmt(kf,_) | PStmtStart(kf,_) |
+ PLval(Some kf,_,_) | PExp(Some kf,_,_)
| PTermLval(Some kf,_,_,_) as loc) ->
begin match global (kf_to_global kf) with
| None ->
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index ec69447e74d..5a1f810e04f 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -20,100 +20,32 @@
(* *)
(**************************************************************************)
-open Format
open Cil_types
open Gtk_helper
open Cil_datatype
+open Printer_tag
-let dkey = Gui_parameters.register_category "pretty-source"
-
-(** The kind of object that can be selected in the source viewer *)
-type localizable =
+type localizable = Printer_tag.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
+ (** 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.Make
- (struct
- include Datatype.Undefined
- type t = localizable
- let name = "Pretty_source.Localizable"
- let reprs = List.map (fun g -> PGlobal g) Global.reprs
- let equal l1 l2 = match l1,l2 with
- | PStmt (_,ki1), PStmt (_,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) -> Cil_datatype.Exp.equal e1 e2
- | PIP ip1, PIP ip2 -> Property.equal ip1 ip2
- | PGlobal g1, PGlobal g2 -> Cil_datatype.Global.equal g1 g2
- | (PStmt _ | PLval _ | PExp _ | PTermLval _ | PVDecl _
- | PIP _ | PGlobal _), _
- -> false
- let mem_project = Datatype.never_any_project
- let pp_ki_loc fmt ki =
- match ki with
- | Kglobal -> (* no location, print 'global' *)
- Format.fprintf fmt "global"
- | Kstmt st ->
- Format.fprintf fmt "%a" Cil_datatype.Location.pretty (Stmt.loc st)
- let pretty fmt = function
- | 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)
-
-let kf_of_localizable loc = match loc with
- | PLval (kf_opt, _, _)
- | PExp (kf_opt,_,_)
- | PTermLval(kf_opt, _,_,_)
- | PVDecl (kf_opt, _, _) -> kf_opt
- | PStmt (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) -> 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 dkey = Gui_parameters.register_category "pretty-source"
+let kf_of_localizable = Printer_tag.kf_of_localizable
+let ki_of_localizable = Printer_tag.ki_of_localizable
+let varinfo_of_localizable = Printer_tag.varinfo_of_localizable
module Locs:sig
type state
@@ -126,7 +58,6 @@ module Locs:sig
val set_hilite : state -> (unit -> unit) -> unit
val add_finalizer: state -> (unit -> unit) -> unit
val size : state -> int
- val add_stmt_start: state -> int (* sid *) -> int (* offset *) -> unit
val stmt_start: state -> stmt -> int
end
=
@@ -169,12 +100,12 @@ struct
For example: 'loop assigns x;' will be indexed as an assigns
and not as a code annotation.
*)
- let add state loc v =
- if not (Hashtbl.mem state.table loc) then
- Hashtbl.add state.table loc v
-
- let add_stmt_start state sid start =
- Datatype.Int.Hashtbl.add state.stmt_start sid start
+ let add state range = function
+ | Printer_tag.PStmtStart(_,st) ->
+ Datatype.Int.Hashtbl.add state.stmt_start st.sid (fst range)
+ | localizable ->
+ if not (Hashtbl.mem state.table range) then
+ Hashtbl.add state.table range localizable
let stmt_start state s =
Datatype.Int.Hashtbl.find state.stmt_start s.sid
@@ -274,383 +205,31 @@ let fold_preconds_at_callsite stmt =
let are_preconds_unfolded stmt =
Cil_datatype.Stmt.Hashtbl.mem unfold_preconds stmt
+module Tag =
+struct
-module Tag = struct
- exception Wrong_decoder
- let make_modem charcode =
- let h = Hashtbl.create 17 in
- let current = ref 0 in
- (function lv ->
- incr current;
- Hashtbl.add h !current lv;
- sprintf "guitag:%c%x" charcode !current),
- (function code ->
- Scanf.sscanf code "guitag:%c%x"
- (fun c code ->
- if c=charcode then
- try Hashtbl.find h code with Not_found -> assert false
- else raise Wrong_decoder))
-
- let encode_stmt,decode_stmt = make_modem 's'
- let encode_lval,decode_lval = make_modem 'l'
- let encode_exp,decode_exp = make_modem 'e'
- let encode_termlval,decode_termlval = make_modem 't'
- let encode_vdecl,decode_vdecl = make_modem 'd'
- let encode_global,decode_global = make_modem 'g'
- let encode_ip,decode_ip = make_modem 'i'
-
- let create = function
- | PStmt sid -> encode_stmt sid
- | PLval lval -> encode_lval lval
- | PExp e -> encode_exp e
- | PTermLval lval -> encode_termlval lval
- | PVDecl vi -> encode_vdecl vi
- | PGlobal g -> encode_global g
- | PIP ip -> encode_ip ip
+ let hashtbl = Hashtbl.create 0
+ let current = ref 0
+ let charcode = function
+ | PStmt _ -> 's'
+ | PStmtStart _ -> 'k'
+ | PLval _ -> 'l'
+ | PExp _ -> 'e'
+ | PTermLval _ -> 't'
+ | PVDecl _ -> 'd'
+ | PGlobal _ -> 'g'
+ | PIP _ -> 'i'
+
+ let create loc =
+ incr current ;
+ let tag = Printf.sprintf "guitag:%c%x" (charcode loc) !current in
+ Hashtbl.replace hashtbl tag loc ; tag
+
+ let get = Hashtbl.find hashtbl
- let get s =
- try
- PExp (decode_exp s)
- with Wrong_decoder -> try
- PStmt (decode_stmt s)
- with Wrong_decoder -> try
- PLval (decode_lval s)
- with Wrong_decoder -> try
- PTermLval (decode_termlval s)
- with Wrong_decoder -> try
- PVDecl (decode_vdecl s)
- with Wrong_decoder -> try
- PGlobal (decode_global s)
- with Wrong_decoder -> try
- PIP (decode_ip s)
- with Wrong_decoder ->
- assert false
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 TagPrinterClassDeferred (X: Printer.PrinterClass) = struct
-
- class tagPrinterClass : 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 Cil_datatype.Stmt.Hashtbl.mem unfold_preconds 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
- Format.fprintf fmt "@{<gui:stmt_start%d>%a@}" s.sid (super#stmtkind sattr next) sk
-
- initializer force_brace <- true
-
- end
-end
+module Printer = Printer_tag.Make(Tag)
exception Found of int*int
@@ -683,29 +262,11 @@ let locate_localizable state loc =
with Found (b,e) -> Some (b,e)
let localizable_from_locs state ~file ~line =
- let loc_localizable = function
- | PStmt (_,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)
- in
let r = ref [] in
Locs.iter
state
(fun _ v ->
- let loc,_ = loc_localizable v in
+ let loc,_ = loc_of_localizable v in
if line = loc.Filepath.pos_lnum && loc.Filepath.pos_path = file then
r := v::!r);
!r
@@ -715,13 +276,7 @@ let buffer_formatter state source =
let emit_open_tag s =
(* Ignore tags that are not ours *)
if Extlib.string_prefix "guitag:" s then
- Stack.push (source#end_iter#offset, Tag.get s) starts
- else begin
- try
- let sid = Scanf.sscanf s "gui:stmt_start%d" Extlib.id in
- Locs.add_stmt_start state sid source#end_iter#offset
- with Scanf.Scan_failure _ | End_of_file -> ()
- end;
+ Stack.push (source#end_iter#offset, Tag.get s) starts ;
""
in
let emit_close_tag s =
@@ -789,6 +344,7 @@ let display_source globals
in
highlighter v ~start:pb ~stop:pe
with Not_found -> ())
+ | PStmtStart _
| PTermLval _ | PLval _ | PVDecl _ | PGlobal _
| PIP _ | PExp _ ->
highlighter v ~start:pb ~stop:pe
@@ -800,12 +356,10 @@ let display_source globals
in
Locs.set_hilite state hiliter;
let gtk_fmt = buffer_formatter state (source:>GText.buffer) in
- let pp = Printer.current_printer () in
- let module CurrentPP = (val pp: Printer.PrinterClass) in
- let module TagPrinterClass = TagPrinterClassDeferred(CurrentPP) in
- let tagPrinter = new TagPrinterClass.tagPrinterClass in
let display_global g =
- tagPrinter#global gtk_fmt g;
+ Printer.with_unfold_precond
+ are_preconds_unfolded
+ Printer.pp_global gtk_fmt g ;
Format.pp_print_flush gtk_fmt ()
in
let counter = ref 0 in
diff --git a/src/plugins/gui/pretty_source.mli b/src/plugins/gui/pretty_source.mli
index 452f6727f9c..998910fda3a 100644
--- a/src/plugins/gui/pretty_source.mli
+++ b/src/plugins/gui/pretty_source.mli
@@ -25,9 +25,9 @@
open Cil_types
-(** The kind of object that can be selected in the source viewer. *)
-type localizable =
+type localizable = Printer_tag.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)
@@ -41,8 +41,6 @@ type localizable =
definitions. *)
| PIP of Property.t
-module Localizable: Datatype.S with type t = localizable
-
module Locs: sig
type state
(** To call when the source buffer is about to be discarded *)
@@ -79,7 +77,6 @@ val locate_localizable : Locs.state -> localizable -> (int*int) option
(** @return Some (start,stop) in offset from start of buffer if the
given localizable has been displayed according to [Locs.locs]. *)
-
val kf_of_localizable : localizable -> kernel_function option
val ki_of_localizable : localizable -> kinstr
val varinfo_of_localizable : localizable -> varinfo option
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index 2bfb3dd73f3..2fd3a11560a 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -813,7 +813,7 @@ let highlighter (buffer:reactive_buffer) localizable ~start ~stop =
in
Design.Feedback.mark buffer#buffer ~call_site:stmt ~offset validity
- | Pretty_source.PStmt _
+ | Pretty_source.PStmt _ | Pretty_source.PStmtStart _
| Pretty_source.PGlobal _| Pretty_source.PVDecl _
| Pretty_source.PTermLval _| Pretty_source.PLval _
| Pretty_source.PExp _ -> ()
diff --git a/src/plugins/occurrence/register_gui.ml b/src/plugins/occurrence/register_gui.ml
index f5de64c4877..9fbba556725 100644
--- a/src/plugins/occurrence/register_gui.ml
+++ b/src/plugins/occurrence/register_gui.ml
@@ -134,7 +134,7 @@ let occurrence_highlighter buffer loc ~start ~stop =
if List.exists same_tlval result then highlight ()
| PVDecl(_, _,vi') when Varinfo.equal vi vi' ->
highlight ()
- | PExp _ | PVDecl _ | PStmt _ | PGlobal _ | PIP _ -> ()
+ | PExp _ | PVDecl _ | PStmt _ | PStmtStart _ | PGlobal _ | PIP _ -> ()
module FollowFocus =
State_builder.Ref
diff --git a/src/plugins/scope/dpds_gui.ml b/src/plugins/scope/dpds_gui.ml
index 6347c073154..b8b5b779c6e 100644
--- a/src/plugins/scope/dpds_gui.ml
+++ b/src/plugins/scope/dpds_gui.ml
@@ -466,7 +466,8 @@ let highlighter (buffer:Design.reactive_buffer) localizable ~start ~stop =
put_tag (ShowDef.tag_stmt stmt)
| PIP (Property.IPCodeAnnot (_, _, annot)) ->
put_tag (Pscope.tag_annot annot)
- | PExp _ | PVDecl _ | PTermLval _ | PLval _ | PGlobal _ | PIP _ -> ()
+ | PStmtStart _ | PExp _
+ | PVDecl _ | PTermLval _ | PLval _ | PGlobal _ | PIP _ -> ()
with Not_found -> ()
let check_value (main_ui:Design.main_window_extension_points) =
diff --git a/src/plugins/security_slicing/register_gui.ml b/src/plugins/security_slicing/register_gui.ml
index b18a51f45e0..685cbf1dc90 100644
--- a/src/plugins/security_slicing/register_gui.ml
+++ b/src/plugins/security_slicing/register_gui.ml
@@ -57,6 +57,7 @@ let security_highlighter buffer loc ~start ~stop =
if List.exists (fun k -> k.sid=s.sid) d then begin
let tag = make_tag buffer"direct" [`BACKGROUND "green" ] in
apply_tag buffer tag start stop end
+ | PStmtStart _
| PExp _ | PVDecl _ | PTermLval _ | PLval _ | PGlobal _ | PIP _ -> ()
let security_selector
diff --git a/src/plugins/slicing/register_gui.ml b/src/plugins/slicing/register_gui.ml
index 5a962f17d8a..1db715334e4 100644
--- a/src/plugins/slicing/register_gui.ml
+++ b/src/plugins/slicing/register_gui.ml
@@ -461,6 +461,7 @@ let slicing_highlighter(buffer:Design.reactive_buffer) localizable ~start ~stop=
match localizable with
| Pretty_source.PStmt (kf,stmt) -> tag_stmt kf stmt start stop
| Pretty_source.PVDecl (Some kf,_,vi) -> tag_vdecl kf vi start stop
+ | Pretty_source.PStmtStart _
| Pretty_source.PVDecl (None,_,_)
| Pretty_source.PLval _
| Pretty_source.PTermLval _
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index d08b1885786..08eabb21cd9 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -479,7 +479,7 @@ module Select (Eval: Eval) = struct
| PExp ((_,Kglobal,_) | (None, Kstmt _, _))
| PTermLval (None, _, _, _)-> ()
| PVDecl (_kf,_ki,_vi) -> ()
- | PGlobal _ | PIP _ -> ()
+ | PGlobal _ | PIP _ | PStmtStart _ -> ()
with
| Eval_terms.LogicEvalError ee ->
main_ui#pretty_information "Cannot evaluate term: %a@."
@@ -519,6 +519,7 @@ module Select (Eval: Eval) = struct
| _ -> ()
)
end
+ | PStmtStart _
| PVDecl (None, _, _) | PExp _ | PTermLval _ | PGlobal _ | PIP _ -> ()
let _right_click_value_not_computed (main_ui:main_ui) (menu:menu) localizable =
diff --git a/src/plugins/wp/GuiSource.ml b/src/plugins/wp/GuiSource.ml
index a47a570c5e8..f08f6d217e1 100644
--- a/src/plugins/wp/GuiSource.ml
+++ b/src/plugins/wp/GuiSource.ml
@@ -42,7 +42,7 @@ and call = {
}
let selection_of_localizable = function
- | PStmt( kf , stmt )
+ | PStmt( kf , stmt ) | PStmtStart( kf , stmt )
| PLval( Some kf , Kstmt stmt , _ )
| PTermLval( Some kf , Kstmt stmt , _, _ ) ->
begin
@@ -250,7 +250,8 @@ class highlighter (main:Design.main_window_extension_points) =
if DEPS.mem ip deps then
apply_depend buffer start stop
end
- | PGlobal _|PVDecl _|PTermLval _|PLval _| PExp _ -> ()
+ | PStmtStart _ | PGlobal _
+ | PVDecl _ | PTermLval _ | PLval _ | PExp _ -> ()
end
end
--
GitLab