A | |
access_kind [Alarms] | |
accessor [Typed_parameter] | |
action [Toolbox] | |
action [Dataflow2] | |
action [Dataflow] | |
alarm [Alarms] | |
alarm_behavior [CilE] | |
align [Toolbox] | |
allocation [Cil_types] |
allocates and frees.
|
alphaTableData [Alpha] |
This is the type of the elements of the alpha renaming table.
|
annot [Logic_ptree] |
all kind of annotations
|
asm_details [Cabs] | |
assigns [Logic_ptree] |
assignment performed by a C function.
|
assigns [Cil_types] |
zone assigned with its dependencies.
|
attribute [Cil_types] | |
attribute [Cabs] | |
attributeClass [Cil] |
Various classes of attributes
|
attributes [Cil_types] |
Attributes are lists sorted by the attribute name.
|
attrparam [Cil_types] |
The type of parameters of attributes
|
B | |
base [Base] | |
behavior [Cil_types] |
Behavior of a function.
|
behavior_or_loop [Property] |
assigns can belong either to a contract or a loop annotation
|
binary_operator [Cabs] | |
binop [Logic_ptree] |
arithmetic and logic binary operators.
|
binop [Cil_types] |
Binary operations
|
bitsSizeofTyp [Cil_types] |
This is used to cache the computation of the size of types in bits.
|
bitsSizeofTypCache [Cil_types] | |
block [Cil_types] |
A block is a sequence of statements with the control falling through from
one element to the next
|
block [Cabs] | |
bound_kind [Alarms] | |
builtin_logic_info [Cil_types] | |
builtin_sig [Db.Value] |
Type for a Value builtin function
|
C | |
cabsexp [Cabs] | |
cabsloc [Cabs] | |
cache_type [Hptmap.Make] |
Some functions of this module may optionally use internal caches.
|
cacheable [Value_types] | |
call_result [Value_types] |
Results of a a call to a function
|
call_site [Value_types] | |
callback_result [Value_types] | |
callback_state [Menu_manager] |
Callback for the buttons that can be in the menus.
|
callgraph [Callgraph] |
a call graph is a hashtable, mapping a function name to
the node which describes that function's call structure
|
callnode [Callgraph] |
a call node describes the local calling structure for a
single function: which functions it calls, and which
functions call it
|
callstack [Value_types] |
Value callstacks, as used e.g.
|
callstack [Value_messages] | |
callstack [Db.Value] | |
category [Log] |
category for debugging/verbose messages.
|
channel [Log] | |
chooser [Gtk_helper] |
The created widget is packed in the box.
|
cil_function [Cil_types] |
Internal representation of decorated C functions
|
code_annot [Logic_ptree] | |
code_annot [Cil_types] |
all annotations that can be found in the code.
|
code_annotation [Cil_types] |
code annotation with an unique identifier.
|
code_transformation_category [File] |
type of registered code transformations
|
column [Gtk_helper.Custom] | |
compinfo [Cil_types] |
The definition of a structure or union type.
|
cond [Cabscond] | |
configData [Gtk_helper.Configuration] | |
configData [Cilconfig] |
The configuration data can be of several types *
|
consolidated_status [Property_status.Consolidation] | |
constant [Logic_ptree] |
logic constants.
|
constant [Cil_types] |
Literal constants
|
constant [Cabs] | |
cstring [Base] | |
custom_list [Gtk_helper.MAKE_CUSTOM_LIST] | |
custom_tree [Logic_ptree] | |
custom_tree [Cil_types] | |
cvspec [Cabs] | |
D | |
data [State_builder.Weak_hashtbl] | |
data [Datatype.Sub_caml_weak_hashtbl] | |
data [Dataflow.StmtStartData] | |
data [State_builder.Ref] |
Type of the referenced value.
|
data [State_builder.Hashtbl] | |
data [Buckx.S] | |
data [Dataflow2.StmtStartData] | |
data_in_list [State_builder.List_ref] | |
decide_fast [Hptmap.Make] | |
decl [Logic_ptree] |
global declarations.
|
decl_node [Logic_ptree] | |
decl_type [Cabs] | |
definition [Cabs] | |
demon [Gtk_form] | |
deps [Logic_ptree] |
C locations.
|
deps [Cil_types] |
dependencies of an assigned location.
|
E | |
edge [Service_graph.Make] | |
elt [State_builder.Queue] | |
elt [Lattice_type.Lattice_Set_Generic.O] | |
elt [FCSet.S_Basic_Compare] |
The type of the set elements.
|
elt [State_builder.Set_ref] | |
emitted_status [Property_status] |
Type of status emitted by analyzers.
|
emitter [Emitter] | |
emitter_with_properties [Property_status] | |
entry [Menu_manager] | |
enum_item [Cabs] | |
enuminfo [Cil_types] |
Information about an enumeration.
|
enumitem [Cil_types] | |
error [Dynlink_common_interface] | |
event [Log] | |
existsAction [Cil] |
A datatype to be used in conjunction with
existsType
|
exit [Cmdline] | |
exp [Cil_types] |
Expressions (Side-effect free)
|
exp_info [Cil_types] |
Additional information on an expression
|
exp_node [Cil_types] | |
expression [Cabs] | |
ext_decl [Logic_ptree] |
ACSL extension for external spec file *
|
ext_function [Logic_ptree] | |
ext_module [Logic_ptree] | |
ext_spec [Logic_ptree] | |
F | |
fct [Filter.RemoveInfo] |
some type for a function information
|
featureDescr [Cil] |
To be able to add/remove features easily, each feature should be package
as an interface with the following interface.
|
field [Toolbox] |
The expansible attribute of a field.
|
field [Gtk_form] | |
field_group [Cabs] | |
fieldinfo [Cil_types] |
Information about a struct/union field.
|
file [File] | |
file [Cil_types] |
The top-level representation of a CIL source file (and the result of the
parsing and elaboration).
|
file [Cabs] |
the string is a file name, and then the list of toplevel forms.
|
filekind [Toolbox] | |
filetree_node [Filetree] | |
fkind [Cil_types] |
Various kinds of floating-point numbers
|
for_clause [Cabs] | |
formatArg [Cil] |
The type of argument for the interpreter
|
formatter [Pretty_utils] | |
formatter2 [Pretty_utils] | |
from [Cil_types] | |
from_deps [Function_Froms.Deps] | |
froms [Function_Froms] | |
funbehavior [Cil_types] |
behavior of a function.
|
fundec [Cil_types] |
Function definitions.
|
funspec [Cil_types] |
function contract.
|
funspec [Cabs] | |
fuzzy_order [Rangemap] | |
G | |
gen_accessor [Typed_parameter] | |
global [Cil_types] |
The main type for representing global declarations and definitions.
|
global_annotation [Cil_types] |
global annotations, not attached to a statement or a function.
|
guardaction [Dataflow2] |
For if statements
|
guardaction [Dataflow] |
For if statements
|
H | |
history_elt [History] | |
how_to_journalize [Db] |
How to journalize the given function.
|
I | |
i [Int_Base] | |
icon [Toolbox] | |
id [Hook.S_ordered] | |
identified_allocation [Property] | |
identified_assigns [Property] | |
identified_axiom [Property] | |
identified_axiomatic [Property] | |
identified_behavior [Property] | |
identified_code_annotation [Property] |
Only AAssert, AInvariant, or APragma.
|
identified_complete [Property] | |
identified_decrease [Property] |
code_annotation is None for decreases and
Some { AVariant } for
loop variant.
|
identified_disjoint [Property] | |
identified_from [Property] | |
identified_lemma [Property] | |
identified_predicate [Property] | |
identified_predicate [Cil_types] |
predicate with an unique identifier.
|
identified_property [Property] | |
identified_reachable [Property] | None, Kglobal --> global property
None, Some kf --> impossible
Some kf, Kglobal --> property of a function without code
Some kf, Kstmt stmt --> reachability of the given stmt (and the attached
properties)
|
identified_term [Cil_types] |
tsets with an unique identifier.
|
ikind [Cil_types] |
Various kinds of integers
|
impact_pragma [Cil_types] |
Pragmas for the impact plugin of Frama-C.
|
inconsistent [Property_status] | |
info [Type.Heterogeneous_table] | |
info [Cabscond] | |
init [Cil_types] |
Initializers for global variables.
|
init_expression [Cabs] | |
init_name [Cabs] | |
init_name_group [Cabs] | |
initinfo [Cil_types] |
We want to be able to update an initializer in a global variable, so we
define it as a mutable field
|
initwhat [Cabs] | |
instr [Cil_types] |
Instructions.
|
internal_tbl [Emitter.Make_table] | |
itv [Offsetmap_bitwise] | |
itv [Lattice_Interval_Set] | |
K | |
kernel_function [Cil_types] |
Except field
fundec , do not use the other fields directly.
|
key [Type.Heterogeneous_table] | |
key [Rangemap.S] |
The type of the map keys.
|
key [Locations.Location_Bytes.M] | |
key [Hptmap.Make] | |
key [Hook.S_ordered] | |
key [FCMap.S] |
The type of the map keys.
|
key [State_builder.Hashtbl] | |
kf [Description] | |
kind [State_builder.Proxy] | |
kind [Origin] | |
kind [Log] | |
kind [Gtk_helper.Icon] | |
kind [Emitter] | |
kind [Cabscond] | |
kinstr [Cil_types] | |
L | |
l [Lattice_type.Lattice_Base] | |
label [Cil_types] |
Labels
|
lexpr [Logic_ptree] |
logical expression.
|
lexpr_node [Logic_ptree] | |
lhost [Cil_types] |
The host part of an
Cil_types.lval .
|
lineDirectiveStyle [Cil] |
Styles of printing line directives
|
line_directive_style [Printer_api] |
Styles of printing line directives
|
linking_error [Dynlink_common_interface] | |
local_env [Cabs2cil] |
local information needed to typecheck expressions and statements
|
localisation [Cil_types] | |
localizable [Pretty_source] |
The kind of object that can be selected in the source viewer.
|
location [Locations] |
A
Location_Bits.t and a size in bits.
|
location [Errorloc] |
Type for source-file locations
|
location [Cil_types] |
Describes a location in a source file
|
logic_body [Cil_types] | |
logic_constant [Cil_types] | |
logic_ctor_info [Cil_types] |
Description of a constructor of a logic sum-type.
|
logic_dependencies [Value_types] |
Dependencies for the evaluation of a term or a predicate: for each
program point involved, sets of zones that must be read
|
logic_info [Cil_types] |
description of a logic function or predicate.
|
logic_label [Cil_types] |
logic label referring to a particular program point.
|
logic_real [Cil_types] |
Real constants.
|
logic_type [Logic_ptree] |
logic types.
|
logic_type [Cil_types] |
Types of logic terms.
|
logic_type_def [Cil_types] | |
logic_type_info [Cil_types] |
Description of a logic type.
|
logic_var [Cil_types] |
description of a logic variable
|
logic_var_kind [Cil_types] |
origin of a logic variable.
|
loop_invariant [Cabs] | |
loop_pragma [Cil_types] |
Pragmas for the value analysis plugin of Frama-C.
|
lval [Cil_types] | |
M | |
mach [Cil_types] | |
map_t [Map_Lattice.Make_without_cardinal] | |
map_t [Locations.Zone] | |
miscState [Cil] | |
model_annot [Logic_ptree] |
model field.
|
model_info [Cil_types] |
model field.
|
mutex [Task] | |
N | |
name [Cabs] | |
nameKind [Cabsvisit] | |
name_group [Cabs] | |
named [Cil_types] |
object that can be named (in particular predicates).
|
nameform [Rmciltmps] | |
nodeinfo [Callgraph] | |
O | |
offset [Cil_types] |
The offset part of an
Cil_types.lval .
|
offsetmap [Lmap_sig] |
type of the maps associated to a base
|
option_setting [Cmdline] | |
ordered_stmt [Ordered_stmt] |
An
ordered_stmt is an int representing a stmt in a particular
function.
|
ordered_stmt_array [Ordered_stmt] |
As
ordered_stmts are contiguous and start from 0, they are
suitable for use by index in a array.
|
ordered_to_stmt [Ordered_stmt] |
Types of conversion tables between stmt and ordered_stmt.
|
origin [Origin] |
List of possible origins.
|
overflow_kind [Alarms] |
Only signed overflows int are really RTEs.
|
P | |
pack [Structural_descr] |
Structural descriptor used inside structures.
|
param [Hook.S] |
Type of the parameter of the functions registered in the hook.
|
parameter [Typed_parameter] | |
parsed_float [Floating_point] |
If
s is parsed as (n, l, u) , then n is the nearest approximation of
s with the desired precision.
|
path_elt [Logic_ptree] |
kind of expression.
|
pending [Property_status.Consolidation] |
who do the job and, for each of them, who find which issues.
|
plugin [Plugin] |
Only iterable parameters (see
do_iterate and do_not_iterate ) are
registered in the field p_parameters .
|
poly [Type.Polymorphic4] | |
poly [Type.Polymorphic3] | |
poly [Type.Function] | |
poly [Type.Polymorphic2] | |
poly [Type.Polymorphic] |
Type of the polymorphic type (for instance
'a list ).
|
pragma [Cil_types] |
The various kinds of pragmas.
|
precedence [Type] |
Precedences used for generating the minimal number of parenthesis in
combination with function
Type.par below.
|
precision_loss_message [Value_messages] | |
predicate [Cil_types] |
predicates
|
predicate_kind [Property] | |
predicate_result [Hptmap.Make] |
Does the given predicate hold or not.
|
predicate_type [Hptmap.Make] |
Existential (
|| ) or universal (&& ) predicates.
|
prefix [Log] | |
pretty_aborter [Log] | |
pretty_printer [Log] |
Generic type for the various logging channels which are not aborting
Frama-C.
|
private_ops [State] | |
process_result [Command] | |
program_point [Property] | |
proj [Filter.RemoveInfo] |
some type for the whole project information
|
project [Project_skeleton] | |
project [Project] |
Type of a project.
|
Q | |
quantifiers [Logic_ptree] |
quantifier-bound variables
|
quantifiers [Cil_types] |
variables bound by a quantifier.
|
R | |
rangemap [Rangemap.S] |
The type of maps from type
key to type value .
|
raw_statement [Cabs] | |
recursive [Structural_descr] |
Type used for handling (possibly mutually) recursive structural
descriptors.
|
relation [Logic_ptree] |
comparison operators.
|
relation [Cil_types] |
comparison relations
|
result [Hook.S] |
Type of the result of the functions.
|
result [Command] | |
rhs [Reachingdefs] | |
rootsFilter [Rmtmps] | |
rounding_mode [Ival.Float_abstract] | |
running [Task] | |
S | |
server [Task] | |
set [Db.Slicing.Select] |
Set of colored selections.
|
sformat [Pretty_utils] | |
shape [Hptset.S] |
Shape of the set, ie.
|
shared [Task] |
Shareable tasks.
|
single_name [Cabs] | |
single_pack [Structural_descr] | |
slice_pragma [Cil_types] |
Pragmas for the slicing plugin of Frama-C.
|
spec [Logic_ptree] |
specification of a C function.
|
spec [Cil_types] |
Function contract.
|
spec_elem [Cabs] | |
specifier [Cabs] | |
stage [Cmdline] |
The different stages, from the first to be executed to the last one.
|
state [Value_messages] | |
state [Printer_api] | |
state [Pretty_source.Locs] |
To call when the source buffer is about to be discarded
|
state [Logic_lexer] | |
state [Db.Value] |
Internal state of the value analysis.
|
state_on_disk [State] | |
statement [Cabs] | |
status [Task] | |
status [Property_status] |
Type of known precise status of a property.
|
status_accessor [Db.RteGen] | |
stmt [Cil_types] |
Statements.
|
stmt_to_ordered [Ordered_stmt] | |
stmtaction [Dataflow2] | |
stmtaction [Dataflow] | |
stmtkind [Cil_types] | |
storage [Cil_types] |
Storage-class information
|
storage [Cabs] | |
structure [Unmarshal] | |
structure [Structural_descr] |
Description with details.
|
style [Toolbox] | |
subtree [Lmap_sig] | |
sum [Lattice_type.Lattice_Sum] | |
syntactic_context [CilE] | |
T | |
t [Warning_manager] |
Type of the widget containing the warnings.
|
t [Vector] | |
t [Unmarshal] | |
t [Type.Polymorphic4_input] | |
t [Type.Polymorphic3_input] | |
t [Type.Polymorphic2_input] | |
t [Type.Polymorphic_input] |
Static polymorphic type corresponding to its dynamic counterpart to
register.
|
t [Type.Obj_tbl] | |
t [Type.Ty_tbl] | |
t [Type.Heterogeneous_table] |
Type of heterogeneous (hash)tables indexed by values of type Key.t.
|
t [Type.Abstract] | |
t [Type] |
Type of type values.
|
t [Trace] | |
t [Tr_offset] | |
t [Structural_descr] |
Type of internal representations of OCaml type.
|
t [State_topological.G] | |
t [State_selection] |
Type of a state selection.
|
t [State_builder.Proxy] |
Proxy type.
|
t [State.Local] |
Type of the state to register.
|
t [Source_manager] | |
t [Reachingdefs.ReachingDef] | |
t [Qstack.DATA] | |
t [Qstack.Make] | |
t [Property_status.Consolidation_graph] | |
t [Property_status.Feedback] |
Same constructor than Consolidation.t, without argument.
|
t [Project_skeleton] | |
t [Parameter_sig.Indexed_val_input] |
the type to be serialized
|
t [Parameter_sig.S_no_parameter] |
Type of the parameter (an int, a string, etc).
|
t [Logic_typing.Lenv] | |
t [Locations.Location_Bytes.M] | |
t [Lmap_sig.LBase] | |
t [Liveness.LiveFlow] | |
t [Lattice_type.Lattice_Set_Generic.O] | |
t [Lattice_type.Lattice_Set_Generic] | |
t [Lattice_type.Lattice_Base] | |
t [Lattice_type.Lattice_Product] | |
t [Lattice_type.With_Widening] | |
t [Lattice_type.With_Cardinal_One] | |
t [Lattice_type.With_Diff_One] | |
t [Lattice_type.With_Diff] | |
t [Lattice_type.With_Enumeration] | |
t [Lattice_type.With_Intersects] | |
t [Lattice_type.With_Under_Approximation] | |
t [Lattice_type.With_Narrow] | |
t [Lattice_type.With_Top] | |
t [Ival.Float_abstract] | |
t [Ival.F] | |
t [Integer] | |
t [Indexer.Elt] | |
t [Indexer.Make] | |
t [Hptmap.Make] | |
t [Hptmap.Shape] | |
t [Hook.Comparable] | |
t [FCSet.S_Basic_Compare] |
The type of sets.
|
t [FCMap.S] |
The type of maps from type
key to type 'a .
|
t [Dynamic.Parameter.Common] | |
t [Descr] |
Type of a type descriptor.
|
t [Db.INOUTKF] | |
t [Db.Slicing.Slice] |
Abtract data type for function slice.
|
t [Db.Slicing.Select] |
Internal selection.
|
t [Db.Slicing.Mark] |
Abtract data type for mark value.
|
t [Db.Slicing.Project] |
Abstract data type for slicing project.
|
t [Db.Occurrence] | |
t [Db.Pdg] |
PDG type
|
t [Db.Properties.Interp.To_zone] | |
t [Db.Access_path] | |
t [Db.Value] |
Internal representation of a value.
|
t [Datatype.Sub_caml_weak_hashtbl] | |
t [Datatype.Make_input] |
Type for this datatype
|
t [Datatype.Ty] | |
t [Datatype] |
Values associated to each datatype.
|
t [Dataflows.JOIN_SEMILATTICE] | |
t [Dataflow2.BackwardsTransfer] |
The type of the data we compute for each block start.
|
t [Dataflow2.ForwardsTransfer] |
The type of the data we compute for each block start.
|
t [Dataflow.BackwardsTransfer] |
The type of the data we compute for each block start.
|
t [Dataflow.ForwardsTransfer] |
The type of the data we compute for each block start.
|
t [Cmdline.Group] | |
t [Buckx.WeakHashable] | |
t [Buckx.S] | |
t [Bitvector] | |
t [Binary_cache.Result] | |
t [Binary_cache.Cacheable] | |
t [Bag] | |
t [Availexpslv.AvailableExps] | |
t [Abstract_interp.Rel] | |
t1 [Lattice_type.Lattice_Sum] | |
t1 [Lattice_type.Lattice_UProduct] | |
t1 [Lattice_type.Lattice_Product] | |
t2 [Lattice_type.Lattice_Sum] | |
t2 [Lattice_type.Lattice_UProduct] | |
t2 [Lattice_type.Lattice_Product] | |
t_ctx [Db.Properties.Interp.To_zone] | |
t_decl [Db.Properties.Interp.To_zone] | |
t_nodes_and_undef [Db.Pdg] |
type for the return value of many
find_xxx functions when the
answer can be a list of (node, z_part) and an undef zone .
|
t_pragmas [Db.Properties.Interp.To_zone] | |
t_zone_info [Db.Properties.Interp.To_zone] |
list of zones at some program points.
|
t_zones [Db.Scope] | |
tag [Hptmap] | |
task [Task] | |
term [Cil_types] |
Logic terms.
|
term_lhost [Cil_types] |
base address of an lvalue.
|
term_lval [Cil_types] |
lvalue: base address and offset.
|
term_node [Cil_types] |
the various kind of terms.
|
term_offset [Cil_types] |
offset of an lvalue.
|
termination_kind [Cil_types] |
kind of termination a post-condition applies to.
|
theMachine [Cil] | |
timer [Command] | |
token [Logic_parser] | |
token [Cparser] | |
tt [Map_Lattice.Make_without_cardinal] | |
tt [Locations.Zone] | |
tt [Lmap_sig] | |
tt [Lattice_type.Lattice_UProduct] | |
tt [Ival] | |
ty [Type] | |
typ [Cil_types] | |
typeSpecifier [Cabs] | |
type_annot [Logic_ptree] |
type invariant.
|
typed_accessor [Typed_parameter] | |
typedef [Logic_ptree] |
Concrete type definition.
|
typeinfo [Cil_types] |
Information about a defined type.
|
typing_context [Logic_typing] |
Functions that can be called when type-checking an extension of ACSL.
|
U | |
un_t [Cvalue.V_Or_Uninitialized] | |
unary_operator [Cabs] | |
undoAlphaElement [Alpha] |
This is the type of the elements that are recorded by the alpha
conversion functions in order to be able to undo changes to the tables
they modify.
|
unop [Logic_ptree] |
unary operators.
|
unop [Cil_types] |
Unary operators
|
update_term [Logic_ptree] | |
V | |
v [Offsetmap_sig] |
Type of the values stored in the offsetmap
|
v [Lmap_sig] |
type of the values associated to a location
|
validity [Base] | |
value [Rangemap.S] | |
value [Parameter_sig.String_hashtbl] | |
value [Parameter_sig.Indexed_val] |
the real type for the option
|
value_message [Value_messages] | |
variant [Logic_ptree] |
variant for loop or recursive function.
|
variant [Cil_types] |
variant of a loop or a recursive function.
|
varinfo [Cil_types] |
Information about a variable.
|
vertex [Service_graph.Make] | |
visitAction [Cil] |
Different visiting actions.
|
visitor_behavior [Cil] |
Visitor behavior
|
W | |
warn_mode [CilE] |
An argument of type
warn_mode is required by some of the access
functions in Db.Value (the interface to the value analysis).
|
warning [Value_messages] | |
wchar [Escape] | |
where [Menu_manager] |
Where to put a new entry.
|
widen_hint [Offsetmap_sig] | |
widen_hint [Map_Lattice.Make] | |
widen_hint [Lmap_sig] |
Bases that must be widening in priority, plus widening hints for each
base.
|
widen_hint [Lattice_type.With_Widening] |
hints for the widening
|
widen_hint_base [Lmap_sig] |
widening hints for each base
|
wstring [Escape] | |
Y | |
y [Lmap_bitwise.Location_map_bitwise] | |
Z | |
z [Locations.Location_Bytes] |