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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct