package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Utilities to pretty print source with located elements in a Gtk TextBuffer.

type localizable = Frama_c_kernel.Printer_tag.localizable =
  1. | PStmt of Frama_c_kernel.Cil_types.kernel_function * Frama_c_kernel.Cil_types.stmt
  2. | PStmtStart of Frama_c_kernel.Cil_types.kernel_function * Frama_c_kernel.Cil_types.stmt
  3. | PLval of Frama_c_kernel.Cil_types.kernel_function option * Frama_c_kernel.Cil_types.kinstr * Frama_c_kernel.Cil_types.lval
  4. | PExp of Frama_c_kernel.Cil_types.kernel_function option * Frama_c_kernel.Cil_types.kinstr * Frama_c_kernel.Cil_types.exp
  5. | PTermLval of Frama_c_kernel.Cil_types.kernel_function option * Frama_c_kernel.Cil_types.kinstr * Frama_c_kernel.Property.t * Frama_c_kernel.Cil_types.term_lval
  6. | PVDecl of Frama_c_kernel.Cil_types.kernel_function option * Frama_c_kernel.Cil_types.kinstr * Frama_c_kernel.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.

    *)
  7. | PGlobal of Frama_c_kernel.Cil_types.global
    (*

    all globals but variable declarations and function definitions.

    *)
  8. | PIP of Frama_c_kernel.Property.t
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.