package frama-c

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

Main Components

The whole GUI aka self

method menu_manager : unit -> Frama_c_gui.Menu_manager.menu_manager

The object managing the menubar and the toolbar.

  • since Boron-20100401
method file_tree : Frama_c_gui.Filetree.t

The tree containing the list of files and functions

method file_tree_view : GTree.view

The tree view containing the list of files and functions

method main_window : GWindow.window

The main window

method annot_window : Frama_c_gui.Wtext.text

The information panel. The text is automatically cleared whenever the selection is changed. You should not directly use the buffer contained in the annot_window to add text. Use the method pretty_information.

method pretty_information : 'a. ?scroll:bool -> ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a

Pretty print a message in the annot_window, optionally scrolling it to the beginning of the message.

method lower_notebook : GPack.notebook

The lower notebook with messages tabs

Source viewers

The GText.view showing the AST.

method source_viewer_scroll : GBin.scrolled_window

The scrolling of the GText.view showing the AST.

method reactive_buffer : reactive_buffer

The buffer containing the AST.

  • since Carbon-20101201
method original_source_viewer : Frama_c_gui.Source_manager.t

The multi-tab source file display widget containing the original source.

Dialog Boxes

method launcher : unit -> unit

Display the analysis configuration dialog and offer the opportunity to launch to the user

method error : 'a. ?parent:GWindow.window_skel -> ?reset:bool -> ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a

Popup a modal dialog displaying an error message. If reset is true (default is false), the gui is reset after the dialog has been displayed.

Extension Points

method register_source_selector : (GMenu.menu GMenu.factory -> main_window_extension_points -> button:int -> Frama_c_gui.Pretty_source.localizable -> unit) -> unit

register an action to perform when button is released on a given localizable. If the button 3 is released, the first argument is popped as a contextual menu.

method register_source_highlighter : (reactive_buffer -> Frama_c_gui.Pretty_source.localizable -> start:int -> stop:int -> unit) -> unit

register an highlighting function to run on a given localizable between start and stop in the given buffer. Priority of Gtext.tags is used to decide which tag is rendered on top of the other.

method register_panel : (main_window_extension_points -> string * GObj.widget * (unit -> unit) option) -> unit

register_panel (name, widget, refresh) registers a panel in GUI. The arguments are the name of the panel to create, the widget containing the panel and a function to be called on refresh.

General features

method reset : unit -> unit

Reset the GUI and its extensions to its initial state

method rehighlight : unit -> unit

Force to rehighlight the current displayed buffer. Plugins should call this method whenever they have changed the states on which the function given to register_source_highlighter have been updated.

method redisplay : unit -> unit

Force to redisplay the current displayed buffer. Plugins should call this method whenever they have changed the globals. For example whenever a plugin adds an annotation, the buffers need to be redisplayed.

  • since Nitrogen-20111001
method protect : cancelable:bool -> ?parent:GWindow.window_skel -> (unit -> unit) -> unit

Lock the GUI ; run the function ; catch all exceptions ; Unlock GUI The parent window must be set if this method is not called directly by the main window: it will ensure that error dialogs are transient for the right window.

Set cancelable to true if the protected action should be cancellable by the user through button `Stop'.

method full_protect : 'a. cancelable:bool -> ?parent:GWindow.window_skel -> (unit -> 'a) -> 'a option

Lock the GUI ; run the function ; catch all exceptions ; Unlock GUI ; returns f (). The parent window must be set if this method is not called directly by the main window: it will ensure that error dialogs are transient for the right window.

Set cancelable to true if the protected action should be cancellable by the user through button `Stop'.

method push_info : 'a. ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a

Pretty print a temporary information in the status bar

method pop_info : unit -> unit

Remove last temporary information in the status bar

method show_ids : bool

If true, the messages shown in the GUI can mention internal ids (vid, sid, etc.). If false, other means of identification should be used (line numbers, etc.).

method help_message : 'a 'b. < event : GObj.event_ops.. > as 'a -> ('b, Stdlib.Format.formatter, unit) Stdlib.format -> 'b

Help message displayed when entering the widget

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