Index of types


A
access_kind [Alarms]
accessor [Typed_parameter]
accessor [Parameter_category]
Type explaining how to manipulate the elements of the category.
action [Wpane]
Button for dialog options
action [Dataflow2]
action [Dataflow]
action [Hptset.S]
alarm [Offsetmap_sig]
true indicates that an alarm may have occurred
alarm [Alarms]
align [Widget]
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_component_addition [Annotations]
type for functions adding a part of a behavior inside a contract.
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_alarm [Fval]
Floating-point builtins may produce three kinds of alarms: APosInf when the result may contain +oo;, ANegInf when the result may contain -oo;, ANaN msg when the result is NaN; an explanation of why the argument is invalid is given., AAssume msg is a variant of ANaN for debugging purposes, mostly for internal use. Ignored when printing alarms. Builtins may sometimes raise Non_finite when no part of the result is finite.
builtin_logic_info [Cil_types]
builtin_res [Fval]
Builtins return structured alarms, in the guise of a set of string explaining the problem.
builtin_sig [Db.Value]
Type for a Value builtin function

C
c_rounding_mode [Floating_point]
Rounding modes defined in the C99 standard.
cabsexp [Cabs]
cabsloc [Cabs]
cache_type [Hptmap_sig]
Some functions of this module may optionally use internal caches.
callback_state [Menu_manager]
Callback for the buttons that can be in the menus.
callstack [Db.Value]
catch_binder [Cil_types]
Kind of exceptions that are caught by a given clause.
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 [Wtable]
compinfo [Cil_types]
The definition of a structure or union type.
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]
contract_component_addition [Annotations]
type for functions adding a part of a contract (either for global function or for a given stmt).
cpp_opt_kind [File]
Whether a given preprocessor supports gcc options used in some configurations.
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 [Dataflow2.StmtStartData]
data [Dataflow.StmtStartData]
data [State_builder.Ref]
Type of the referenced value.
data [State_builder.Hashtbl]
data_in_list [State_builder.List_ref]
decide_fast [Hptmap_sig.S]
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]
elt [State_builder.Array]
elt [State_builder.Queue]
elt [Parameter_sig.Collection]
Element in the collection.
elt [Parameter_sig.Collection_category]
Element in the category
elt [Lattice_type.Lattice_Set_Generic.O]
elt [Set.S]
The type of the set elements.
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 [Lattice_messages]
emitter [Emitter]
emitter_with_properties [Property_status]
empty_action [Hptmap_sig.S]
entry [Wtext]
entry [Rgmap]
Entry (a,b,v) maps range a..b (both inclued) to value v in the map.
entry [Menu_manager]
enum_item [Cabs]
enuminfo [Cil_types]
Information about an enumeration.
enumitem [Cil_types]
error [FCDynlink]
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]
extended_asm [Cil_types]
GNU extended-asm information: a list of outputs, each of which is an lvalue with optional names and constraints., a list of input expressions along with constraints, clobbered registers, Possible destinations statements

F
fct [Filter.RemoveInfo]
some type for a function information
field [Wpane]
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 [Wfile]
filetree_node [Filetree]
fkind [Cil_types]
Various kinds of floating-point numbers
float_kind [Fval]
for_clause [Cabs]
formatArg [Cil]
The type of argument for the interpreter
formatter [Pretty_utils]
formatter2 [Pretty_utils]
from [Cil_types]
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]
generic_widen_hint [Offsetmap_lattice_with_isotropy]
generic_widen_hint [Map_Lattice.Make]
generic_widen_hint [Locations.Location_Bytes]
generic_widen_hint [Ival]
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.
graph [Service_graph.S]
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 [Widget]
id [Hook.S_ordered]
identified_allocation [Property]
identified_assigns [Property]
identified_axiom [Property]
identified_axiomatic [Property]
identified_behavior [Property]
for statement contract, the set of parent behavior for which the contract is active is part of its identification.
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_global_invariant [Property]
identified_instance [Property]
Specialization of a property at a given point.
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.
identified_type_invariant [Property]
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]
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]
intervals [Offsetmap_bitwise_sig]
itv [Int_Intervals_sig]

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 [Parameter_sig.Multiple_value_datatype]
key [Parameter_sig.Value_datatype]
key [Parameter_sig.Multiple_map]
key [Parameter_sig.Map]
Type of keys of the map.
key [Locations.Location_Bytes.M]
key [Hptmap_sig.S]
type of the keys
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]
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.
line_directive_style [Printer_api]
Styles of printing line directives
linking_error [FCDynlink]
lmap [Lmap_sig]
lmap [Lmap_bitwise.Location_map_bitwise]
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 [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_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 [Lmap_sig]
Maps from Base.t to Lmap_sig.offsetmap
map [Lmap_bitwise.Location_map_bitwise]
map2_decide [Offsetmap_sig]
map2_decide [Offsetmap_bitwise_sig]
map_t [Map_Lattice.Make_without_cardinal]
map_t [Locations.Zone]
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).
node [Service_graph.S]

O
offset [Cil_types]
The offset part of an Cil_types.lval.
offset_match [Bit_utils]
We want to find a symbolic offset that corresponds to a numeric one, with one additional criterion:
offsetmap [Lmap_sig]
type of the maps associated to a base
offsetmap_top_bottom [Lmap_sig]
ontty [Log]
or_bottom [Bottom.Type]
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]
parse [Logic_lexer]
parsed_float [Floating_point]
If s is parsed as (n, l, u), then n is the nearest approximation of s with the desired precision.
partition [Wto]
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.
predicate [Cil_types]
predicates
predicate_kind [Property]
predicate_result [Hptmap_sig.S]
Does the given predicate hold or not.
predicate_type [Hptmap_sig.S]
Existential (||) or universal (&&) predicates.
prefix [Log]
prefix [Hptmap_sig.S]
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
range_validity [Base]
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]
result [Abstract_interp.Comp]
rootsFilter [Rmtmps]
rounding_mode [Fval]

S
server [Task]
set [Db.Slicing.Select]
Set of colored selections.
sformat [Pretty_utils]
shape [Hptmap_sig.S]
shape [Hptset.S]
Shape of the set, ie.
shared [Task]
Shareable tasks.
sign [Floating_point]
single_name [Cabs]
single_pack [Structural_descr]
size_widen_hint [Offsetmap_lattice_with_isotropy]
size_widen_hint [Map_Lattice.Make]
size_widen_hint [Locations.Location_Bytes]
size_widen_hint [Ival]
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 [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 the local 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 [Widget]
subtree [Lmap_sig]
succ [Wto]
sum [Lattice_type.Lattice_Sum]

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]
Type of traces.
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 [Rgmap]
The type of range maps, containing of collection of 'a entry.
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.Collection_category]
t [Parameter_sig.S_no_parameter]
Type of the parameter (an int, a string, etc).
t [Parameter_category]
\tau t is the type of a category for the type \tau.
t [Map_Lattice.Make_without_cardinal]
t [Logic_typing.Lenv]
t [Locations.Zone]
This type should be considered private
t [Locations.Location_Bytes.M]
Mapping from bases to bytes-expressed offsets
t [Locations.Location_Bytes]
This type should be considered private
t [Lattice_type.Lattice_Set_Generic.O]
t [Lattice_type.Lattice_Set_Generic]
t [Lattice_type.Lattice_Base]
t [Lattice_type.Lattice_UProduct]
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 [Lattice_messages]
t [Json]
Json Objects
t [Ival]
t [Integer]
t [Indexer.Elt]
t [Indexer.Make]
t [Hptmap.Shape]
t [Hook.Comparable]
t [Set.S]
The type of sets.
t [Fval.F]
t [Fval]
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.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 [Bitvector]
t [Binary_cache.Result]
t [Binary_cache.Cacheable]
t [Bag]
t [Abstract_interp.Bool]
t [Abstract_interp.Rel]
t [Abstract_interp.Comp]
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_bottom [Offsetmap_sig]
Datatype for the offsetmaps
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_top_bottom [Offsetmap_sig]
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]
thread [Task]
timer [Command]
token [Logic_parser]
token [Cparser]
ty [Type]
typ [Cil_types]
typeSpecifier [Cabs]
type_annot [Logic_ptree]
type invariant.
type_namespace [Logic_typing]
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
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 [Offsetmap_bitwise_sig]
Type of the values stored in the offsetmap
v [Lmap_sig]
type of the values associated to a location
v [Lmap_bitwise.Location_map_bitwise]
v [Hptmap_sig.S]
type of the values
validity [Base]
value [Rangemap.S]
value [Parameter_sig.Multiple_map]
value [Parameter_sig.Map]
Type of the values associated to the keys.
variable_validity [Base]
Validity for variables that might change size.
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]
visitAction [Cil]
Different visiting actions.
visitor_behavior [Cil]
Visitor behavior

W
wchar [Escape]
where [Menu_manager]
Where to put a new entry.
widen_hint [Offsetmap_sig]
widen_hint [Map_Lattice.Make]
widen_hint [Locations.Location_Bytes]
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]
wto [Wto_statement]
This type represents a list; Nil is the empty list, Node conses a single element, while Component conses a whole component.