package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Main Components
1. Source viewers
Dialog Boxes
Extension Points
General features

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.1-Nickel.tar.gz

sha256=0220bc743b7da2468ceb926f331edc7ddfaa7c603ba47962de3e33c8e1e3f593

doc/frama-c.gui/Frama_c_gui/Design/class-main_window/index.html

Class `Design.main_window`Source

inherit view_code

Main Components

method toplevel : main_window_extension_points

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, Format.formatter, unit) 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

method source_viewer : Frama_c_gui.GSourceView.source_view

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, Format.formatter, unit) 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.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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, Format.formatter, unit) 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, Format.formatter, unit) format ->
  'b

Help message displayed when entering the widget