Frama_c_gui.Pretty_source
Utilities to pretty print source with located elements in a Gtk TextBuffer.
type localizable = Frama_c_kernel.Printer_tag.localizable
module Locs : sig ... end
val fold_preconds_at_callsite : Frama_c_kernel.Cil_types.stmt -> unit
val are_preconds_unfolded : Frama_c_kernel.Cil_types.stmt -> bool
val display_source :
Frama_c_kernel.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
The selector and the highlighter are always host#protected. The selector will not be called when 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 -> Frama_c_kernel.Cil_types.stmt -> int
Offset at which the current statement starts in the buffer corresponding to state
, _without_ ACSL assertions/contracts, etc.
val locate_localizable : Locs.state -> localizable -> (int * int) option
val kf_of_localizable :
localizable ->
Frama_c_kernel.Cil_types.kernel_function option
val ki_of_localizable : localizable -> Frama_c_kernel.Cil_types.kinstr
val varinfo_of_localizable :
localizable ->
Frama_c_kernel.Cil_types.varinfo option
val localizable_from_locs :
Locs.state ->
file:Frama_c_kernel.Datatype.Filepath.t ->
line:int ->
localizable list
Returns the lists of localizable in file
at line
visible in the current Locs.state
. This function is inefficient as it iterates on all the current Locs.state
.