Index of class methods

Register an entry

Add an accelerator iff there is a menu item.

Add an empty column that always appears after the columns created by the other add_column methods.

Add entries to the menu dedicated to debugging tools.

Add entries in the given menu.

Inserts an entry in the form.

add_global_filter text key f adds a filter for the visibility of the globals, according to f.

Adds an item.

Inserts a field name.

Inserts a small (fixed) widget in place of a label.

Inserts an empty line.

Add entries dedicated to a plug-in.

Inserts a wide entry in the form, spanning the two columns.

Starts a new section.

Register a callback that is called whenever an element of the file tree is selected or unselected.

Inserts a separator.

Append a palette-tool.

Append an arbitrary widget among other widget tools.

first parameter is the introducing keyword (e.g.

The information panel.

Print an annotated statement.

append_pixbuf_column title f visible appends a new column with name title to the file tree and registers f as a callback computing the list of properties for this column.

append_text_column ~title ~tooltip ~visible ~text ~sort appends a new column with name title to the file tree, and registers text as a callback computing the text for each global variable.

first parameter is the introducing keyword (e.g.

Attribute.

Attribute lists

Attribute parameter

the kind of behavior expected for the behavior.

Prints a block.

Closes the dialog.

Remove all items

Deactivate and hide the action button.

widget of the scroll

connect f calls f s on each signal s.

Register a callback invoked by the widget each time the value is edited.

link to the current function being visited.

link to the kernel function currently being visited.

Kstmt stmt when visiting statement stmt, Kglobal when called outside of a statement.

link to the current statement being visited.

When removed

Display the given globals in the pretty-printed source viewer.

Popup a modal dialog displaying an error message.

Print expressions

A field declaration

Print initializers.

The tree containing the list of files and functions

The tree view containing the list of files and functions

fill the global environment tables at the end of a full copy in a new project.

find_visible_global str searches for the next occurrence of a visible global whose name contains str, starting at the currently selected element.

Emits the signal to all connected listeners, if enabled and not locked.

Return true if the filetree currently displays all globals in flat mode (all children of the same node), false otherwise (children of the file they are declared in).

The formatter used by printf method.

self#force_brace printer fmt x pretty prints x by using printer, but add some extra braces '{' and '}' which are hidden by default.

same as plain_copy_visitor but for frama-c specific methods

prints an assignment with its dependencies.

Lock the GUI ; run the function ; catch all exceptions ; Unlock GUI ; returns f ().

Return the names and the attributes (currently only the strikethrough property) of the globals in the file passed as argument

get the queue of actions to be performed at the end of a full copy.

What terminator to print after an instruction.

Returns the viewer object (and the buffer it contains).

Global (vars, types, etc.).

true if current_stmt has some annotations attached to it.

Help message displayed when entering the widget

Print an horizontal rule.

Open a ghost context if the the first bool is true and we are not already in a ghost context.

Invoked on each instruction occurrence.

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

Print a line-number.

If not locked, lock and execute the continuation and finally release the lock.

The lower notebook with messages tabs

Invoked on each lvalue occurrence

The main window

Register the entry around the pretty-printed material.

This is called to check that a given statement may be compacted with another one.

Return the menu in which the item has been inserted, if meaningful

The object managing the menubar and the toolbar.

Invoked on each offset occurrence.

on_check v emits boolean signal (s=v) on signal s.

on_check v fires a boolean signal (s=v) on signal s.

on_event emits a unit signal on any signal s.

on_event fires a unit signal on any signal.

Short cut to links#on_click (callback without range).

on_value v emits a unit signal on signal s=v.

on_value v fires a unit signal on signal s when s=v.

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

packs the scroll

a visitor who only does copies of the nodes according to behavior

Remove last temporary information in the status bar

pretty prints a post condition according to the exit kind it represents

All ACSL keywords except logic types

Called before/after printing an annotation comment.

Modifying pretty-printer behavior

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

Append material to the text buffer, optionally scrolling it to the beginning of the message (defaults to autoscrolling setting).

Project the visitor operates on.

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.

Pretty print a temporary information in the status bar

Add here instructions while visiting to queue them to precede the current statement being processed.

The buffer containing the AST.

Reset the activation state of the buttons

Refresh the state of all the non-source columns of the filetree, by hiding those that should be hidden, and displaying the others.

register_panel (name, widget, refresh) registers a panel in GUI.

Register a function to be called whenever the reset method of the filetree is called.

register an highlighting function to run on a given localizable between start and stop in the given buffer.

register an action to perform when button is released on a given localizable.

Force to rehighlight the current displayed buffer.

Structure has changed

Resynchronize the tree view with the current project state.

Reset the GUI and its extensions to its initial state

Internal use only.

Opens the dialog (asynchronously).

Run the menu.

Default line is last one.

scrolled tree (build on demand)

Move the pretty-printed source viewer to the given localizable if possible.

When scroll:false (default), only minimal scrolling is performed to make the selection visible.

Closes the dialog.

Open the dialog.

Selects the given global in the tree view and run the associated callbacks.

This function tries to select the global in the treeview.

send f calls f with the current value via the signal lock.

Set's widget value to given one.

Makes the action button visible.

Automatically scroll to lastly inserted text (console behavior).

Shall be used at most once, and before #coerce or #widget.

Override properties for the given tag name.

Internal use only.

Set the pretty-printer for button.

Turns emission of signals on or off.

Install the new-entry creator.

Manually set some attributes of the given filename.

Set the font used to display the text.

Manually set some attributes of the given variable.

The style of hovered entries.

Set a monospace font

Set the sensitive property of all the entries.

The style of added entries.

Set the pretty-printer for tooltip.

If true, the messages shown in the GUI can mention internal ids (vid, sid, etc.).

The GText.view showing the AST.

The scrolling of the GText.view showing the AST.

Control-flow statement.

true if the given statement has some annotations attached to it.

Print only the labels of the statement.

Print a statement kind.

Self cast

The whole GUI aka self

Use of some type in some declaration.

Gets the queue of instructions and resets the queue.

On array request

Request update on each entry.

(only) Content of rows has changed

Invoked on each variable use.

Invoked each time an identifier name is to be printed.

Attribute.

Attribute parameters.

Block.

declaration of a struct/union

Invoked for each variable declaration.

declaration of an enumeration

visit the declaration of an enumeration item

Invoked on each expression occurrence.

visit the declaration of a field of a structure or union

visit a whole file.

Function definition.

Global (vars, types, etc.)

Replacement of vglob.

the tree

The tree view associated in which the file tree is packed.

Display the given location in the original_source_viewer

Display the given stmt in the original source viewer

Display the given stmt in the source_viewer and in the original_source_viewer.

Initializers.

Invoked on each offset appearing in the list of a CompoundInit initializer.

Invoked on each instruction occurrence.

local initializer.

Invoked on each lvalue occurrence

Invoked on each offset occurrence that is *not* as part of an initializer list specification, i.e.

Control-flow statement.

Replacement of vstmt.

Use of some type.

Invoked for each variable declaration.

Invoked on each variable use.

Returns the widget

self#without_annot printer fmt x pretty prints x by using printer, without pretty-printing its function contracts and code annotations.

Register with #add an entry around its pretty-print.

Print with a callback to the actual bounds of the printed material after boxing.