Pretty_source (frama-c.Frama_c_gui.Pretty

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

returns
Some (start,stop) in offset from start of buffer if the given localizable has been displayed according to Locs.locs.

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.