Frama_c_kernel.Printer_tag
Utilities to pretty print source with located Ast elements
type localizable =
| PStmt of Cil_types.kernel_function * Cil_types.stmt
Full statement (with attributes, annotations, etc.)
*)| PStmtStart of Cil_types.kernel_function * Cil_types.stmt
Naked statement (only skind, without attributes, annotations, etc.)
*)| PLval of Cil_types.kernel_function option * Cil_types.kinstr * Cil_types.lval
L-Values
*)| PExp of Cil_types.kernel_function option * Cil_types.kinstr * Cil_types.exp
Non l-value expressions
*)| PTermLval of Cil_types.kernel_function option
* Cil_types.kinstr
* Property.t
* Cil_types.term_lval
Term l-values inside properties
*)| PVDecl of Cil_types.kernel_function option
* Cil_types.kinstr
* Cil_types.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 Cil_types.global
Global definitions except global variables and functions.
*)| PIP of Property.t
| PType of Cil_types.typ
The kind of object that can be selected in the source viewer.
val label : localizable -> string
Name (or category).
val glabel : Cil_types.global -> string
Name (or category).
val pretty : Stdlib.Format.formatter -> localizable -> unit
Description of a localizable.
val pp_debug : Stdlib.Format.formatter -> localizable -> unit
Debugging.
module Localizable : Datatype.S_with_collections with type t = localizable
val localizable_of_global : Cil_types.global -> localizable
val localizable_of_kf : Cil_types.kernel_function -> localizable
val kf_of_localizable : localizable -> Cil_types.kernel_function option
val ki_of_localizable : localizable -> Cil_types.kinstr
val varinfo_of_localizable : localizable -> Cil_types.varinfo option
val typ_of_localizable : localizable -> Cil_types.typ option
val loc_of_localizable : localizable -> Cil_types.location
Might return Location.unknown
val loc_to_localizable :
?precise_col:bool ->
Filepath.position ->
localizable option
return the (hopefully) most precise localizable that contains the given Filepath.position. If precise_col
is true
, takes the column number into account (possibly a more precise, but costly, result).
module type Tag = sig ... end
module type S_pp = sig ... end