Index of class methods


A
add [Toolbox.notebook]
add_accelerator [Menu_manager.item]
Add an accelerator iff there is a menu item.
add_block [Toolbox.dialog]
add_column_empty [Gtk_helper.Custom.columns]
add_column_pixbuf [Gtk_helper.Custom.columns]
add_column_text [Gtk_helper.Custom.columns]
add_column_toggle [Gtk_helper.Custom.columns]
add_debug [Menu_manager.menu_manager]
Add entries to the menu dedicated to debugging tools.
add_entries [Menu_manager.menu_manager]
Add entries in the given menu.
add_field [Toolbox.form]
Inserts an entry in the form.
add_global_filter [Filetree.t]
add_global_filter text key f adds a filter for the visibility of the globals, according to f.
add_item [Toolbox.popup]
Adds an item.
add_label [Toolbox.form]
Inserts a field name.
add_label_widget [Toolbox.form]
Inserts a small (fixed) widget in place of a label.
add_menu [Menu_manager.menu_manager]
add_newline [Toolbox.form]
Inserts an emty line.
add_plugin [Menu_manager.menu_manager]
Add entries dedicated to a plug-in.
add_radio [Toolbox.switch]
add_row [Toolbox.dialog]
add_row [Toolbox.form]
Inserts a wide entry in the form, spanning the two columns.
add_section [Toolbox.form]
Starts a new section.
add_select_function [Filetree.t]
Register a callback that is called whenever an element of the file tree is selected or unselected.
add_separator [Toolbox.popup]
Inserts a separator.
add_toggle [Toolbox.switch]
allocation [Printer_api.extensible_printer_type]
first parameter is the introducing keyword (e.g.
annot_window [Design.main_window_extension_points]
The information panel.
annotated_stmt [Printer_api.extensible_printer_type]
Print an annotated statement.
append [Toolbox.warray]
append_pixbuf_column [Filetree.t]
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.
assigns [Printer_api.extensible_printer_type]
first parameter is the introducing keyword (e.g.
assumes [Printer_api.extensible_printer_type]
attribute [Printer_api.extensible_printer_type]
Attribute.
attributes [Printer_api.extensible_printer_type]
Attribute lists
attrparam [Printer_api.extensible_printer_type]
Attribute paramter

B
behavior [Printer_api.extensible_printer_type]
behavior [Cil.cilVisitor]
the kind of behavior expected for the behavior.
binop [Printer_api.extensible_printer_type]
block [Printer_api.extensible_printer_type]
Prints a block.
buffer [Design.reactive_buffer]
button [Toolbox.dialog]
Closes the dialog.

C
check_menu_item [Menu_manager.item]
child_at [Gtk_helper.Custom.Tree.model]
children [Gtk_helper.Custom.Tree.model]
clear [Toolbox.text]
clear [Toolbox.popup]
Remove all items
clear [Gtk_helper.MAKE_CUSTOM_LIST.custom_list_class]
code_annotation [Printer_api.extensible_printer_type]
coerce [Toolbox.widget]
coerce [Toolbox.label]
coerce [Gtk_helper.Custom.columns]
widget of the scroll
complete_behaviors [Printer_api.extensible_printer_type]
connect [Toolbox.signal]
constant [Printer_api.extensible_printer_type]
count_selected [Gtk_helper.Custom.columns]
create [Toolbox.warray]
current_behavior [Printer_api.extensible_printer_type]
current_func [Cil.cilVisitor]
link to the current function being visited.
current_function [Printer_api.extensible_printer_type]
current_kf [Visitor.frama_c_visitor]
link to the kernel function currently being visited.
current_kinstr [Cil.cilVisitor]
Kstmt stmt when visiting statement stmt, Kglobal when called outside of a statement.
current_stmt [Printer_api.extensible_printer_type]
current_stmt [Cil.cilVisitor]
link to the current statement being visited.
custom_decode_iter [Gtk_helper.MAKE_CUSTOM_LIST.custom_list_class]
custom_encode_iter [Gtk_helper.MAKE_CUSTOM_LIST.custom_list_class]
custom_get_iter [Gtk_helper.MAKE_CUSTOM_LIST.custom_list_class]
custom_get_path [Gtk_helper.MAKE_CUSTOM_LIST.custom_list_class]
custom_iter_children [Gtk_helper.MAKE_CUSTOM_LIST.custom_list_class]
custom_iter_has_child [Gtk_helper.MAKE_CUSTOM_LIST.custom_list_class]
custom_iter_n_children [Gtk_helper.MAKE_CUSTOM_LIST.custom_list_class]
custom_iter_next [Gtk_helper.MAKE_CUSTOM_LIST.custom_list_class]
custom_iter_nth_child [Gtk_helper.MAKE_CUSTOM_LIST.custom_list_class]
custom_iter_parent [Gtk_helper.MAKE_CUSTOM_LIST.custom_list_class]
custom_value [Gtk_helper.MAKE_CUSTOM_LIST.custom_list_class]

D
decreases [Printer_api.extensible_printer_type]
default [Toolbox.button]
delete [Toolbox.entry]
When removed
disjoint_behaviors [Printer_api.extensible_printer_type]
display [Toolbox.filechooser_button]
Set the pretty-printer for button.
display_globals [Design.view_code]
Display the given globals in the pretty-printed source viewer.

E
error [Gtk_helper.host]
error [Design.main_window_extension_points]
Popup a modal dialog displaying an error message
exp [Printer_api.extensible_printer_type]
Print expressions

F
factory [Menu_manager.menu_manager]
field [Printer_api.extensible_printer_type]
fieldinfo [Printer_api.extensible_printer_type]
A field declaration
file [Printer_api.extensible_printer_type]
file_tree [Design.main_window_extension_points]
The tree containing the list of files and functions
file_tree_view [Design.main_window_extension_points]
The tree view containing the list of files and functions
fill_global_tables [Cil.cilVisitor]
fill the global environment tables at the end of a full copy in a new project.
filter [Toolbox.filechooser_dialog]
fire [Toolbox.signal]
fkind [Printer_api.extensible_printer_type]
flat_mode [Filetree.t]
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).
fmt [Toolbox.text]
The formatter used by printf method.
focus [Toolbox.text]
force_brace [Printer_api.extensible_printer_type]
self#force_brace printer fmt x pretty prints x by using printer, but add some extra braces '{' and '}' which are hidden by default.
frama_c_plain_copy [Visitor.frama_c_visitor]
same as plain_copy_visitor but for frama-c specific methods
from [Printer_api.extensible_printer_type]
prints an assignment with its dependencies.
full_protect [Gtk_helper.host]
full_protect [Design.main_window_extension_points]
Lock the GUI ; run the funtion ; catch all exceptions ; Unlock GUI ; returns f ().
funspec [Printer_api.extensible_printer_type]

G
get [Toolbox.warray]
get [Toolbox.listbox]
get [Toolbox.selector]
get [Gtk_helper.Custom.List.model]
get_cur_eh [Availexpslv.aeVisitorClass]
get_cur_iosh [Reachingdefs.rdVisitorClass]
get_file_globals [Filetree.t]
Return the names and the attributes (currently only the strikethrough property) of the globals in the file passed as argument
get_filling_actions [Cil.cilVisitor]
get the queue of actions to be performed at the end of a full copy.
get_instr_terminator [Printer_api.extensible_printer_type]
What terminator to print after an instruction.
get_items [Toolbox.menulist]
global [Printer_api.extensible_printer_type]
Global (vars, types, etc.).
global_annotation [Printer_api.extensible_printer_type]
good_var [Rmciltmps.unusedRemoverClass]

H
has_annot [Printer_api.extensible_printer_type]
true if current_stmt has some annotations attached to it.
has_child [Gtk_helper.Custom.Tree.model]
help_message [Design.main_window_extension_points]
Help message displayed when entering the widget
highlight [Toolbox.text]

I
identified_predicate [Printer_api.extensible_printer_type]
identified_term [Printer_api.extensible_printer_type]
ikind [Printer_api.extensible_printer_type]
index [Gtk_helper.Custom.Tree.model]
index [Gtk_helper.Custom.List.model]
init [Printer_api.extensible_printer_type]
Print initializers.
inline_block [Printer_api.extensible_printer_type]
insert [Toolbox.warray]
insert [Toolbox.listbox]
insert [Gtk_helper.MAKE_CUSTOM_LIST.custom_list_class]
insert_row [Gtk_helper.Custom.columns]
instr [Printer_api.extensible_printer_type]
Invoked on each instruction occurrence.
is_selected [Gtk_helper.Custom.columns]
item [Gtk_form.form]
iter_selected [Gtk_helper.Custom.columns]

L
label [Printer_api.extensible_printer_type]
Label
label [Gtk_form.form]
launcher [Design.main_window_extension_points]
Display the analysis configuration dialog and offer the opportunity to launch to the user
line_directive [Printer_api.extensible_printer_type]
Print a line-number.
location [Printer_api.extensible_printer_type]
locs [Design.reactive_buffer]
logic_constant [Printer_api.extensible_printer_type]
logic_info [Printer_api.extensible_printer_type]
logic_label [Printer_api.extensible_printer_type]
logic_type [Printer_api.extensible_printer_type]
logic_type_def [Printer_api.extensible_printer_type]
logic_var [Printer_api.extensible_printer_type]
lower_notebook [Design.main_window_extension_points]
The lower notebook with messages tabs
lval [Printer_api.extensible_printer_type]
Invoked on each lvalue occurence

M
main_window [Launcher.basic_main]
main_window [Gtk_helper.source_files_chooser_host]
main_window [Design.main_window_extension_points]
The main window
may_be_skipped [Printer_api.extensible_printer_type]
This is called to check that a given statement may be compacted with another one.
mem [Toolbox.warray]
menu [Menu_manager.item]
Return the menu in which the item has been inserted, if meaningful
menu_item [Menu_manager.item]
menu_item_skel [Menu_manager.item]
menu_manager [Design.main_window_extension_points]
The object managing the menubar and the toolbar.
menubar [Menu_manager.menu_manager]
model [Filetree.t]
model_field [Printer_api.extensible_printer_type]
model_info [Printer_api.extensible_printer_type]

N
next_stmt [Printer_api.extensible_printer_type]

O
offset [Printer_api.extensible_printer_type]
Invoked on each offset occurence.
on_check [Toolbox.signal]
on_click [Gtk_helper.Custom.columns]
on_double_click [Gtk_helper.Custom.columns]
on_event [Toolbox.signal]
on_focus [Toolbox.notebook]
on_insert_request [Toolbox.listbox]
on_link [Toolbox.text]
on_right_click [Gtk_helper.Custom.columns]
on_selection [Gtk_helper.Custom.columns]
on_value [Toolbox.signal]
opt_funspec [Printer_api.extensible_printer_type]
original_source_viewer [Design.main_window_extension_points]
The multi-tab source file display widget containing the original source.

P
pack [Gtk_helper.Custom.columns]
packs the scroll
parent [Gtk_helper.Custom.Tree.model]
plain_copy_visitor [Cil.cilVisitor]
a visitor who only does copies of the nodes according to behavior
pop_info [Design.main_window_extension_points]
Remove last temporary information in the status bar
pop_stmt [Cil.cilVisitor]
popup [Toolbox.popup]
Run the menu.
post_cond [Printer_api.extensible_printer_type]
pretty prints a post condition according to the exit kind it represents
predicate [Printer_api.extensible_printer_type]
predicate_named [Printer_api.extensible_printer_type]
pretty_information [Design.main_window_extension_points]
Pretty print a message in the annot_window.
printf [Toolbox.text]
Append material to the text buffer.
project [Cil.cilVisitor]
Project the visitor operates on.
protect [Gtk_helper.host]
protect [Design.main_window_extension_points]
Lock the GUI ; run the funtion ; 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.
push_info [Design.main_window_extension_points]
Pretty print a temporary information in the status bar
push_stmt [Cil.cilVisitor]

Q
quantifiers [Printer_api.extensible_printer_type]
queueInstr [Cil.cilVisitor]
Add here instructions while visiting to queue them to preceede the current statement or instruction being processed.

R
reactive_buffer [Design.main_window_extension_points]
The buffer containing the AST.
redisplay [Design.reactive_buffer]
redisplay [Design.main_window_extension_points]
refresh [Menu_manager.menu_manager]
Reset the activation state of the buttons
refresh_columns [Filetree.t]
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 [Design.main_window_extension_points]
register_panel (name, widget, refresh) registers a panel in GUI.
register_reset_extension [Filetree.t]
Register a function to be called whenever the reset method of the filetree is called.
register_source_highlighter [Design.main_window_extension_points]
register an highlighting function to run on a given localizable between start and stop in the given buffer.
register_source_selector [Design.main_window_extension_points]
register an action to perform when button is released on a given localizable.
rehighlight [Design.reactive_buffer]
rehighlight [Design.main_window_extension_points]
Force to rehilight the current displayed buffer.
relation [Printer_api.extensible_printer_type]
reload [Gtk_helper.Custom.columns]
Structure has changed
reload [Gtk_helper.Custom.custom]
reload [Gtk_helper.Custom.Tree.model]
reload [Gtk_helper.Custom.List.model]
remove [Toolbox.warray]
require_braces [Printer_api.extensible_printer_type]
requires [Printer_api.extensible_printer_type]
reset [Printer_api.extensible_printer_type]
reset [Launcher.basic_main]
reset [Gtk_helper.source_files_chooser_host]
reset [Filetree.t]
Resynchronize the tree view with the current project state.
reset [Design.main_window_extension_points]
Reset the GUI and its extensions to its initial state
reset_current_func [Cil.cilVisitor]
reset_current_kf [Visitor.frama_c_visitor]
Internal use only.
row [Gtk_form.form]
run [Toolbox.dialog]
Opens the dialog (asynchroneously).

S
scroll [Gtk_helper.Custom.columns]
scrolled tree (build on demand)
scroll [Design.view_code]
Move the pretty-printed source viewer to the given localizable if possible.
select [Toolbox.dialog]
Closes the dialog.
select [Toolbox.filechooser_dialog]
select_global [Filetree.t]
Selects the given global in the tree view and run the associated callbacks.
select_or_display_global [Design.view_code]
This function tries to select the global in the treeview.
selected_globals [Filetree.t]
send [Toolbox.selector]
set [Toolbox.warray]
set [Toolbox.listbox]
set [Toolbox.selector]
set_current_func [Cil.cilVisitor]
set_current_kf [Visitor.frama_c_visitor]
Internal use only.
set_enabled [Toolbox.widget]
set_enabled [Toolbox.signal]
set_file_attribute [Filetree.t]
Manually set some attributes of the given filename.
set_focus [Gtk_helper.Custom.columns]
set_global_attribute [Filetree.t]
Manually set some attributes of the given variable.
set_icon [Toolbox.toggle]
set_icon [Toolbox.button]
set_instr_terminator [Printer_api.extensible_printer_type]
set_items [Toolbox.menulist]
set_label [Toolbox.toggle]
set_label [Toolbox.button]
set_relief [Toolbox.toggle]
set_relief [Toolbox.button]
set_reset [Gtk_helper.host]
set_selection_mode [Gtk_helper.Custom.columns]
set_sensitive [Menu_manager.menu_manager]
Set the sensitive property of all the entries.
set_text [Toolbox.label]
size [Gtk_helper.Custom.List.model]
source_viewer [Design.main_window_extension_points]
The GText.view showing the AST.
stmt [Printer_api.extensible_printer_type]
Control-flow statement.
stmt_labels [Printer_api.extensible_printer_type]
Print only the labels of the statement.
stmtkind [Printer_api.extensible_printer_type]
Print a statement kind.
storage [Printer_api.extensible_printer_type]

T
term [Printer_api.extensible_printer_type]
term_binop [Printer_api.extensible_printer_type]
term_lval [Printer_api.extensible_printer_type]
term_node [Printer_api.extensible_printer_type]
term_offset [Printer_api.extensible_printer_type]
terminates [Printer_api.extensible_printer_type]
toggle_tool_button [Menu_manager.item]
tool_button [Menu_manager.item]
tool_button_skel [Menu_manager.item]
toolbar [Menu_manager.menu_manager]
tooltip [Toolbox.filechooser_button]
Set the pretty-printer for tooptip.
toplevel [Design.main_window_extension_points]
The whole GUI aka self
typ [Printer_api.extensible_printer_type]
Use of some type in some declaration.

U
unop [Printer_api.extensible_printer_type]
unqueueInstr [Cil.cilVisitor]
Gets the queue of instructions and resets the queue.
update [Toolbox.entry]
Signal
update [Toolbox.warray]
update_all [Gtk_helper.Custom.columns]
(only) Content of rows has changed
update_row [Gtk_helper.Custom.columns]

V
vEnterScope [Cabsvisit.cabsVisitor]
vExitScope [Cabsvisit.cabsVisitor]
vallocates [Cil.cilVisitor]
vallocation [Cil.cilVisitor]
vannotation [Cil.cilVisitor]
variant [Printer_api.extensible_printer_type]
varinfo [Printer_api.extensible_printer_type]
Invoked on each variable use.
varname [Printer_api.extensible_printer_type]
Invoked each time an identifier name is to be printed.
vassigns [Cil.cilVisitor]
vattr [Cil.cilVisitor]
Attribute.
vattr [Cabsvisit.cabsVisitor]
vattrparam [Cil.cilVisitor]
Attribute parameters.
vbehavior [Cil.cilVisitor]
vblock [Rmciltmps.removeBrackets]
vblock [Rmciltmps.unusedRemoverClass]
vblock [Cil.cilVisitor]
Block.
vblock [Cabsvisit.cabsVisitor]
vcode_annot [Cil.cilVisitor]
vcompinfo [Cil.cilVisitor]
declaration of a struct/union
vdecl [Printer_api.extensible_printer_type]
Invoked for each variable declaration.
vdecltype [Cabsvisit.cabsVisitor]
vdef [Cabsvisit.cabsVisitor]
vdeps [Cil.cilVisitor]
venuminfo [Cil.cilVisitor]
declaration of an enumeration
venumitem [Cil.cilVisitor]
visit the declaration of an enumeration item
vexpr [Rmciltmps.callTempElimClass]
vexpr [Rmciltmps.incdecTempElimClass]
vexpr [Rmciltmps.expLvTmpElimClass]
vexpr [Rmciltmps.expTempElimClass]
vexpr [Rmciltmps.useListerClass]
vexpr [Rmciltmps.memReadOrAddrOfFinderClass]
vexpr [Usedef.useDefVisitorClass]
vexpr [Cil.cilVisitor]
Invoked on each expression occurrence.
vexpr [Cabsvisit.cabsVisitor]
vexpr [Availexpslv.volatileFinderClass]
vexpr [Availexpslv.memReadOrAddrOfFinderClass]
vfieldinfo [Cil.cilVisitor]
visit the declaration of a field of a structure or union
vfile [Cil.cilVisitor]
visit a whole file.
vfrees [Cil.cilVisitor]
vfrom [Cil.cilVisitor]
vfunc [Rmciltmps.unusedRemoverClass]
vfunc [Liveness.doFeatureClass]
vfunc [Cil.cilVisitor]
Function definition.
vglob [Cil.cilVisitor]
Global (vars, types, etc.)
vglob_aux [Visitor.frama_c_visitor]
Replacement of vglob.
videntified_predicate [Cil.cilVisitor]
videntified_term [Cil.cilVisitor]
view [Gtk_helper.Custom.columns]
the tree
view [Filetree.t]
The tree view associated in which the file tree is packed.
view_original [Design.view_code]
Display the given location in the original_source_viewer
view_original_stmt [Design.view_code]
Display the given stmt in the original source viewer
view_stmt [Design.view_code]
Display the given stmt in the source_viewer and in the original_source_viewer.
vimpact_pragma [Cil.cilVisitor]
vinit [Cil.cilVisitor]
Initializers for globals, pass the global where this occurs, and the offset
vinitexpr [Cabsvisit.cabsVisitor]
vinitoffs [Cil.cilVisitor]
Invoked on each offset appearing in the list of a CompoundInit initializer.
vinst [Rmciltmps.callTempElimClass]
vinst [Reachingdefs.rdVisitorClass]
vinst [Usedef.useDefVisitorClass]
vinst [Cil.cilVisitor]
Invoked on each instruction occurrence.
vinst [Availexpslv.aeVisitorClass]
vlogic_ctor_info_decl [Cil.cilVisitor]
vlogic_ctor_info_use [Cil.cilVisitor]
vlogic_info_decl [Cil.cilVisitor]
vlogic_info_use [Cil.cilVisitor]
vlogic_label [Cil.cilVisitor]
vlogic_type [Cil.cilVisitor]
vlogic_type_def [Cil.cilVisitor]
vlogic_type_info_decl [Cil.cilVisitor]
vlogic_type_info_use [Cil.cilVisitor]
vlogic_var_decl [Cil.cilVisitor]
vlogic_var_use [Cil.cilVisitor]
vloop_pragma [Cil.cilVisitor]
vlval [Usedef.useDefVisitorClass]
If onlyNoOffsetsAreDefs is true, then we need to see the varinfo in an lval along with the offset.
vlval [Cil.cilVisitor]
Invoked on each lvalue occurrence
vlval [Availexpslv.lvalFinderClass]
vmodel_info [Cil.cilVisitor]
vname [Cabsvisit.cabsVisitor]
voffs [Cil.cilVisitor]
Invoked on each offset occurrence that is *not* as part of an initializer list specification, i.e.
vpredicate [Cil.cilVisitor]
vpredicate_named [Cil.cilVisitor]
vquantifiers [Cil.cilVisitor]
vslice_pragma [Cil.cilVisitor]
vspec [Cil.cilVisitor]
vspec [Cabsvisit.cabsVisitor]
vstmt [Rmciltmps.unusedRemoverClass]
vstmt [Rmciltmps.defCollectorClass]
vstmt [Rmciltmps.stmtFinderClass]
vstmt [Reachingdefs.rdVisitorClass]
vstmt [Liveness.doFeatureClass]
vstmt [Liveness.nullAdderClass]
vstmt [Cil.cilVisitor]
Control-flow statement.
vstmt [Cabsvisit.cabsVisitor]
vstmt [Availexpslv.aeVisitorClass]
vstmt_aux [Visitor.frama_c_visitor]
Replacement of vstmt.
vterm [Cil.cilVisitor]
vterm_lhost [Cil.cilVisitor]
vterm_lval [Cil.cilVisitor]
vterm_node [Cil.cilVisitor]
vterm_offset [Cil.cilVisitor]
vtype [Expcompare.volatileFinderClass]
vtype [Cil.cilVisitor]
Use of some type.
vtypespec [Cabsvisit.cabsVisitor]
vvar [Cabsvisit.cabsVisitor]
vvdec [Cil.cilVisitor]
Invoked for each variable declaration.
vvrbl [Rmciltmps.memReadOrAddrOfFinderClass]
vvrbl [Usedef.useDefVisitorClass]
this will be invoked on variable definitions only because we intercept all uses of variables in expressions !
vvrbl [Cil.cilVisitor]
Invoked on each variable use.
vvrbl [Availexpslv.addrOfOrGlobalFinderClass]
vvrbl [Availexpslv.viFinderClass]
vvrbl [Availexpslv.memReadOrAddrOfFinderClass]

W
widget [Toolbox.entry]
Returns the widget
without_annot [Printer_api.extensible_printer_type]
self#without_annot printer fmt x pretty prints x by using printer, without pretty-printing its function contracts and code annotations.