diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 26c3fe00ed8721799d8be86fd275eb1b1d8ef434..c1c28dde8e8ad5e441a7d42361016f86e0ec3488 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -36,6 +36,7 @@ type localizable =
| PVDecl of (kernel_function option * kinstr * varinfo)
| PGlobal of global
| PIP of Property.t
+ | PType of typ
let glabel = function
| GType(tinfo,_) -> tinfo.tname
@@ -57,6 +58,7 @@ let label = function
| PTermLval _ -> "(term)"
| PGlobal g -> glabel g
| PIP _ -> "(property)"
+ | PType _ -> "(type)"
let decl_of = function
| GCompTag(comp,loc) -> GCompTagDecl(comp,loc)
@@ -79,6 +81,7 @@ let pretty fmt = function
| PGlobal g -> Printer.pp_global fmt (decl_of g)
| PStmt(_,stmt) | PStmtStart (_, stmt) ->
Printer.(without_annot pp_stmt) fmt stmt
+ | PType t -> Printer.pp_typ fmt t
let pp_ki_loc fmt ki =
match ki with
@@ -108,6 +111,8 @@ let pp_debug fmt = function
Format.fprintf fmt "LocalizableGlobal %a" Printer.pp_global g
| PIP ip ->
Format.fprintf fmt "LocalizableIP %a" Description.pp_property ip
+ | PType typ ->
+ Format.fprintf fmt "LocalizableType %a" Printer.pp_typ typ
module Localizable =
Datatype.Make_with_collections
@@ -136,6 +141,8 @@ module Localizable =
Hashtbl.hash( 6, Property.hash ip )
| PGlobal g ->
Hashtbl.hash( 7, Global.hash g )
+ | PType t ->
+ Hashtbl.hash( 8, Typ.hash t )
let equal l1 l2 = match l1,l2 with
| PStmt (_,ki1), PStmt (_,ki2) -> ki1.sid = ki2.sid
@@ -151,8 +158,9 @@ module Localizable =
| PExp (_,_,e1), PExp(_,_,e2) -> Exp.equal e1 e2
| PIP ip1, PIP ip2 -> Property.equal ip1 ip2
| PGlobal g1, PGlobal g2 -> Global.equal g1 g2
+ | PType t1, PType t2 -> Typ.equal t1 t2
| (PStmt _ | PStmtStart _ | PLval _ | PExp _ | PTermLval _ | PVDecl _
- | PIP _ | PGlobal _), _
+ | PIP _ | PGlobal _ | PType _), _
-> false
let compare l1 l2 = match l1,l2 with
@@ -184,6 +192,9 @@ module Localizable =
| PIP p1 , PIP p2 -> Property.compare p1 p2
| PIP _ , _ -> (-1)
| _ , PIP _ -> 1
+ | PType t1, PType t2 -> Typ.compare t1 t2
+ | PType _, _ -> (-1)
+ | _, PType _ -> 1
| PGlobal g1 , PGlobal g2 -> Global.compare g1 g2
let pretty = pretty (* defined above *)
@@ -204,6 +215,7 @@ let kf_of_localizable loc =
| PIP ip -> Property.get_kf ip
| PGlobal (GFun ({svar = vi}, _)) -> Some (Globals.Functions.get vi)
| PGlobal _ -> None
+ | PType _ -> None
let ki_of_localizable loc = match loc with
| PLval (_, ki, _)
@@ -213,6 +225,7 @@ let ki_of_localizable loc = match loc with
| PStmt (_, st) | PStmtStart(_, st) -> Kstmt st
| PIP ip -> Property.get_kinstr ip
| PGlobal _ -> Kglobal
+ | PType _ -> Kglobal
let varinfo_of_localizable = function
| PLval (_, _, (Var vi, NoOffset)) -> Some vi
@@ -244,7 +257,7 @@ let loc_of_localizable = function
(match kf_of_localizable localize with
| None -> Location.unknown
| Some kf -> Kernel_function.get_location kf)
-
+ | PType _ -> Location.unknown
(* -------------------------------------------------------------------------- *)
(* --- Helper for Globals --- *)
diff --git a/src/kernel_services/ast_printing/printer_tag.mli b/src/kernel_services/ast_printing/printer_tag.mli
index f7dfedd6e3a1e050fdf5fb8d658f20db3610fb11..57de33aaba62d745b1886efcaf7f2a12568ea862 100644
--- a/src/kernel_services/ast_printing/printer_tag.mli
+++ b/src/kernel_services/ast_printing/printer_tag.mli
@@ -40,6 +40,7 @@ type localizable =
| PGlobal of global (** all globals but variable declarations and function
definitions. *)
| PIP of Property.t
+ | PType of typ
(** Name (or category). *)
val label: localizable -> string
diff --git a/src/plugins/eva/gui/register_gui.ml b/src/plugins/eva/gui/register_gui.ml
index 4289d6ee4310ab68a556a5cf4165129587a3a308..252ce46fd4154c61d57839114efea25fe62a64e8 100644
--- a/src/plugins/eva/gui/register_gui.ml
+++ b/src/plugins/eva/gui/register_gui.ml
@@ -494,7 +494,7 @@ module Select (Eval: Eval) = struct
| PExp ((_,Kglobal,_) | (None, Kstmt _, _))
| PTermLval (None, _, _, _)-> ()
| PVDecl (_kf,_ki,_vi) -> ()
- | PGlobal _ | PIP _ | PStmtStart _ -> ()
+ | PGlobal _ | PIP _ | PStmtStart _ | PType _ -> ()
with
| Eval_terms.LogicEvalError ee ->
main_ui#pretty_information "Cannot evaluate term: %a@."
@@ -540,7 +540,8 @@ module Select (Eval: Eval) = struct
)
end
| PStmtStart _
- | PVDecl (None, _, _) | PExp _ | PTermLval _ | PGlobal _ | PIP _ -> ()
+ | PVDecl (None, _, _) | PExp _ | PTermLval _ | PGlobal _ | PIP _
+ | PType _-> ()
let _right_click_value_not_computed (main_ui:main_ui) (menu:menu) localizable =
match localizable with
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index c89557ac63e5d1ed8f5f098f10f2bce5b7e100dc..ac0059e6eb55df035483240efa238b894749fa44 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -525,6 +525,7 @@ let to_do_on_select
(* these properties are not selectable *)
assert false
| PGlobal _g -> main_ui#pretty_information "This is a global.@.";
+ | PType _t -> main_ui#pretty_information "This is a type.@.";
| PLval (kf, ki,lv) ->
let ty = typeOfLval lv in
diff --git a/src/plugins/gui/history.ml b/src/plugins/gui/history.ml
index f72b4909808a2aa3a560effbc276f7130d4b9054..281c9345adbfe77d553aa2ce020e3a52e2b8683f 100644
--- a/src/plugins/gui/history.ml
+++ b/src/plugins/gui/history.ml
@@ -291,7 +291,7 @@ let translate_history_elt old_helt =
end
end
| Localizable (PLval(None,_,_) | PExp(None,_,_) | PTermLval(None,_,_,_)
- | PVDecl(None,_,_)) -> (* no names useful? *) None
+ | PVDecl(None,_,_) | PType _) -> (* no names useful? *) None
| Localizable (PIP _ ) -> (* no names available *) None
(*
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index 655c61f11df4284fd0c42b2dde197e317e059ca0..106b7a7f810e2c19f087b2005d263e1810e35597 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -39,6 +39,7 @@ type localizable = Printer_tag.localizable =
| PGlobal of global (** all globals but variable declarations and function
definitions. *)
| PIP of Property.t
+ | PType of typ
let kf_of_localizable = Printer_tag.kf_of_localizable
let ki_of_localizable = Printer_tag.ki_of_localizable
@@ -216,6 +217,7 @@ struct
| PVDecl _ -> 'd'
| PGlobal _ -> 'g'
| PIP _ -> 'i'
+ | PType _ -> 'y'
let create loc =
incr current ;
@@ -348,7 +350,7 @@ let display_source globals
with Not_found -> ())
| PStmtStart _
| PTermLval _ | PLval _ | PVDecl _ | PGlobal _
- | PIP _ | PExp _ ->
+ | PIP _ | PExp _ | PType _ ->
highlighter v ~start:pb ~stop:pe
with Not_found -> () ) ;
incr index
diff --git a/src/plugins/gui/pretty_source.mli b/src/plugins/gui/pretty_source.mli
index 714c91f3b26636aa1660b3ff5e54fefbb3398802..b0630901280b09b82beadb28181b9322b68618ee 100644
--- a/src/plugins/gui/pretty_source.mli
+++ b/src/plugins/gui/pretty_source.mli
@@ -43,6 +43,7 @@ type localizable = Printer_tag.localizable =
| PGlobal of global (** all globals but variable declarations and function
definitions. *)
| PIP of Property.t
+ | PType of typ
module Locs: sig
type state
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index f1314ed44d5268fb44cc2e98e6a02ed23ba44b36..581eb4e7aaca12f3de21187f158d83c3e8a8c95b 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -844,7 +844,7 @@ let highlighter (buffer:reactive_buffer) localizable ~start ~stop =
| Pretty_source.PStmt _ | Pretty_source.PStmtStart _
| Pretty_source.PGlobal _| Pretty_source.PVDecl _
| Pretty_source.PTermLval _| Pretty_source.PLval _
- | Pretty_source.PExp _ -> ()
+ | Pretty_source.PExp _ | Pretty_source.PType _ -> ()
diff --git a/src/plugins/occurrence/gui/register_gui.ml b/src/plugins/occurrence/gui/register_gui.ml
index 2f07b0e5c44a6f136e04ea784ea6c1aeda305107..d943ba24441e9205dd7a8609761138fbf196c954 100644
--- a/src/plugins/occurrence/gui/register_gui.ml
+++ b/src/plugins/occurrence/gui/register_gui.ml
@@ -132,7 +132,8 @@ 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 _ | PStmtStart _ | PGlobal _ | PIP _ -> ()
+ | PExp _ | PVDecl _ | PStmt _ | PStmtStart _ | PGlobal _ | PIP _
+ | PType _ -> ()
module FollowFocus =
State_builder.Ref
diff --git a/src/plugins/scope/gui/dpds_gui.ml b/src/plugins/scope/gui/dpds_gui.ml
index 1ee519027cf4692301c8bb961929b90270b5a8b5..d37c64e31e4f39462befeb80444b9952cce17bd0 100644
--- a/src/plugins/scope/gui/dpds_gui.ml
+++ b/src/plugins/scope/gui/dpds_gui.ml
@@ -463,7 +463,7 @@ let highlighter (buffer:Design.reactive_buffer) localizable ~start ~stop =
| PIP (Property.(IPCodeAnnot {ica_ca})) ->
put_tag (Pscope.tag_annot ica_ca)
| PStmtStart _ | PExp _
- | PVDecl _ | PTermLval _ | PLval _ | PGlobal _ | PIP _ -> ()
+ | PVDecl _ | PTermLval _ | PLval _ | PGlobal _ | PIP _ | PType _ -> ()
with Not_found -> ()
let check_value (main_ui:Design.main_window_extension_points) =
diff --git a/src/plugins/security_slicing/gui/register_gui.ml b/src/plugins/security_slicing/gui/register_gui.ml
index 658ddac4a73cd2ce3a14fa89e3709740eccd3bc0..7103aa68d01ab029097eb11c52a578a2dab419b5 100644
--- a/src/plugins/security_slicing/gui/register_gui.ml
+++ b/src/plugins/security_slicing/gui/register_gui.ml
@@ -58,7 +58,8 @@ let security_highlighter buffer loc ~start ~stop =
let tag = make_tag buffer ~name:"direct" [`BACKGROUND "green" ] in
apply_tag buffer tag start stop end
| PStmtStart _
- | PExp _ | PVDecl _ | PTermLval _ | PLval _ | PGlobal _ | PIP _ -> ()
+ | PExp _ | PVDecl _ | PTermLval _ | PLval _ | PGlobal _ | PIP _
+ | PType _ -> ()
let security_selector
(popup_factory:GMenu.menu GMenu.factory) main_ui ~button localizable =
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 15d045d4a95e02e116ba565dddafd97b43980f13..ef58a432ab19f21ccdc8855397d22cf450f9f195 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -47,8 +47,9 @@ let get_term kf term =
let key_of_localizable =
let open Printer_tag in
function
- | PStmt _ | PStmtStart _ | PTermLval _ | PVDecl _ | PGlobal _ | PIP _ -> None
- | PLval (_, Kglobal, _) | PExp (_, Kglobal, _) -> None
+ | PStmt _ | PStmtStart _ | PTermLval _ | PVDecl _ | PGlobal _ | PIP _
+ | PType _ | PLval (_, Kglobal, _) | PExp (_, Kglobal, _)
+ -> None
| PLval (kf, Kstmt stmt, lval) ->
let str = Format.asprintf "%a" Cil_datatype.Lval.pretty lval in
Option.(bind kf (fun kf -> get_term kf str) |> map (fun t -> (stmt, t)))
@@ -144,6 +145,7 @@ module MarkerKind = struct
let glob = kind "global"
let term = kind "term"
let prop = kind "property"
+ let typ = kind "type"
let () =
Enum.set_lookup
@@ -158,7 +160,8 @@ module MarkerKind = struct
| PExp _ -> expr
| PTermLval _ -> term
| PGlobal _ -> glob
- | PIP _ -> prop)
+ | PIP _ -> prop
+ | PType _ -> typ)
let data =
Request.dictionary
@@ -196,7 +199,7 @@ module MarkerVar = struct
if Cil.isFunctionType vi.vtype then fct else var
| PGlobal (GFun _ | GFunDecl _) -> fct
| PLval _ | PStmt _ | PStmtStart _
- | PExp _ | PTermLval _ | PGlobal _ | PIP _ -> none)
+ | PExp _ | PTermLval _ | PGlobal _ | PIP _ | PType _ -> none)
let data =
Request.dictionary
@@ -304,6 +307,7 @@ struct
| PTermLval _ -> Printf.sprintf "#t%d" (incr kid ; !kid)
| PGlobal _ -> Printf.sprintf "#g%d" (incr kid ; !kid)
| PIP _ -> Printf.sprintf "#p%d" (incr kid ; !kid)
+ | PType _ -> Printf.sprintf "#y%d" (incr kid ; !kid)
let create loc =
let add_cache key = Cache.add cache key loc in
diff --git a/src/plugins/slicing/gui/register_gui.ml b/src/plugins/slicing/gui/register_gui.ml
index 4db1660355c6c0b74d189b5bb1afd3203d8d0e5e..2f72013186da255ff1611d09dcd7c87abdb743cc 100644
--- a/src/plugins/slicing/gui/register_gui.ml
+++ b/src/plugins/slicing/gui/register_gui.ml
@@ -467,7 +467,8 @@ let slicing_highlighter(buffer:Design.reactive_buffer) localizable ~start ~stop=
| Pretty_source.PTermLval _
| Pretty_source.PGlobal _
| Pretty_source.PIP _
- | Pretty_source.PExp _ -> ()
+ | Pretty_source.PExp _
+ | Pretty_source.PType _ -> ()
in
(* 2. Highlights the 'Slicing' *)
SlicingState.may highlight
diff --git a/src/plugins/wp/gui/GuiSource.ml b/src/plugins/wp/gui/GuiSource.ml
index 6c624cb5a3d119b8e8d9798ef4520aad710001d9..0f2e07a6e6cc5f11da35c79e281852fc1f27446e 100644
--- a/src/plugins/wp/gui/GuiSource.ml
+++ b/src/plugins/wp/gui/GuiSource.ml
@@ -68,7 +68,7 @@ let selection_of_localizable = function
end
| PVDecl (Some kf,_,{vglob=true}) -> S_fun kf
| PIP ip -> S_prop ip
- | PVDecl _ | PLval _ | PExp _ | PTermLval _ | PGlobal _ -> S_none
+ | PVDecl _ | PLval _ | PExp _ | PTermLval _ | PGlobal _ | PType _ -> S_none
let kind_of_property = function
| Property.IPLemma _ -> "lemma"
@@ -250,7 +250,7 @@ class highlighter (main:Design.main_window_extension_points) =
apply_depend buffer start stop
end
| PGlobal _
- | PVDecl _ | PTermLval _ | PLval _ | PExp _ -> ()
+ | PVDecl _ | PTermLval _ | PLval _ | PExp _ | PType _ -> ()
end
end