module Pretty_source:sig
..end
typelocalizable =
Printer_tag.localizable
=
| |
PStmt of |
|||
| |
PStmtStart of |
|||
| |
PLval of |
|||
| |
PExp of |
|||
| |
PTermLval of |
|||
| |
PVDecl of |
(* |
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 |
(* |
all globals but variable declarations and function
definitions.
| *) |
| |
PIP of |
module Locs:sig
..end
val fold_preconds_at_callsite : Cil_types.stmt -> unit
val are_preconds_unfolded : Cil_types.stmt -> bool
val display_source : Cil_types.global list ->
GSourceView.source_buffer ->
host:Gtk_helper.host ->
highlighter:(localizable -> start:int -> stop:int -> unit) ->
selector:(button:int -> localizable -> unit) ->
Locs.state -> unit
not !Gtk_helper.gui_unlocked
.
This clears the Locs.state
passed as argument, then fills it.val hilite : Locs.state -> unit
val stmt_start : Locs.state -> Cil_types.stmt -> int
state
, _without_ ACSL assertions/contracts, etc.val locate_localizable : Locs.state -> localizable -> (int * int) option
Locs.locs
.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 localizable_from_locs : Locs.state ->
file:Datatype.Filepath.t -> line:int -> localizable list
file
at line
visible in the current Locs.state
.
This function is inefficient as it iterates on all the current
Locs.state
.val loc_to_localizable : ?precise_col:bool -> Filepath.position -> localizable option
precise_col
is true
, takes the column number into
account (possibly a more precise, but costly, result).