Frama-C API - Gui_printers
Special pretty-printers for the GUI. Some sub-elements are annotated by format tags, in order to make them reactive.
val get_type_specifier : Frama_c_kernel.Cil_types.typ -> Frama_c_kernel.Cil_types.typReturns the base type for a pointer/array, otherwise t itself. E.g. for t = int***, returns int.
val pp_typ : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.typ -> unitSame as Printer.pp_typ, except that the type is output between Format tags @{<link:typN>}, that are recognized by the GUI.
val pp_typ_unfolded : Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.typ -> unitPretty-prints a type, unfolding it once if it is a typedef, enum, struct or union.
Special pretty-printer that outputs tags link:vidN around varinfos, and link:typN around types.
val varinfo_of_link : string -> Frama_c_kernel.Cil_types.varinfoConvert a string of the form link:vidN into the varinfo of vid N. This varinfo must have been printed by a pretty-printer extended with LinkPrinter. Raise NoMatch if the link is not of the form link:vidN.
val typ_of_link : string -> Frama_c_kernel.Cil_types.typConvert a string of the form link:typN into a type. The association between N and the type is done by printing the type once using pp_typ, or by using a printer extended with LinkPrinter. Raise NoMatch if the link is not of the form link:typN.
val loc_of_link : string -> Frama_c_kernel.Cil_types.locationConvert a string of the form link:locN into the location of id N. This location must have been printed by a pretty-printer extended with LinkPrinter. Raise NoMatch if the link is not of the form link:locN.