package frama-c

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

Module Frama_c_gui.Pretty_sourceSource

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

Sourcemodule Locs : sig ... end
Sourceval fold_preconds_at_callsite : Frama_c_kernel.Cil_types.stmt -> unit
Sourceval are_preconds_unfolded : Frama_c_kernel.Cil_types.stmt -> bool
Sourceval 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.

Sourceval hilite : Locs.state -> unit

Offset at which the current statement starts in the buffer corresponding to state, _without_ ACSL assertions/contracts, etc.

Sourceval 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.

Sourceval varinfo_of_localizable : localizable -> Frama_c_kernel.Cil_types.varinfo option
Sourceval 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