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.

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 Blog 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