Index of types


A
access [Locations]
Kind of memory access.
access [Base]
Access kind: read/write of k bits, or no access.
access_kind [Alarms]
accessor [Typed_parameter]
accessor [Parameter_category]
Type explaining how to manipulate the elements of the category.
acsl_extension [Cil_types]
Extension to standard ACSL clause with an unique identifier.
acsl_extension_kind [Cil_types]
action [Wpane]
Button for dialog options
action [Dataflow2]
action [Hptset.S]
alarm [Alarms]
align [Widget]
align [Pretty_utils]
align [Markdown]
Table columns alignment
allocation [Logic_ptree]
allocates and frees.
allocation [Cil_types]
allocates and frees.
alphaTable [Alpha]
type for alpha conversion table.
alphaTableData [Alpha]
This is the type of the elements of the alpha renaming table.
annot [Logic_ptree]
all kind of annotations
annotation [Interpreted_automata]
array_size [Logic_ptree]
size of logic array.
asm_details [Cabs]
assert_kind [Interpreted_automata]
assertion_kind [Logic_ptree]
assertion_kind [Cil_types]
Kind of an assertion: an assert is both evaluated and used as hypothesis afterwards;, a check is only evaluated, but is not used as an hypothesis: it does not affect the analyses.
assigns [Logic_ptree]
zone assigned with its dependencies.
assigns [Cil_types]
zone assigned with its dependencies.
async [Task]
attr [Dotgraph]
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
automaton [Interpreted_automata]

B
base [Base]
behavior [Logic_ptree]
Behavior in a specification.
behavior [Cil_types]
Behavior of a function or statement.
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 [Markdown]
block [Cil_types]
A block is a sequence of statements with the control falling through from one element to the next.
block [Cabs]
block_ctxt [Printer_api]
context in which a block will be printed.
block_element [Markdown]
bound_kind [Alarms]
box [Wbox]
A packed widget with its layout directives
buffer [Sanitizer]
buffer [Rich_text]
Buffer for creating messages.
buffer [Dotgraph]
A text buffer to compose labels and attributes.
builtin [Db.Value]
Type for an Eva builtin function
builtin_logic_info [Cil_types]
builtin_type [Db.Value]

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 [Oneret]
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.Messages]
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]
all annotations that can be found in the code.
code_annotation [Cil_types]
code annotation with an unique identifier.
code_annotation_node [Cil_types]
all annotations that can be found in the code.
code_transformation_category [File]
type of registered code transformations
coin [Task]
color [Widget]
column [Wtable]
compinfo [Cil_types]
The definition of a structure or union type.
component [Wto]
Each component of the graph is either an individual node of the graph (without) self loop, or a strongly connected component where a node is designed as the head of the component and the remaining nodes are given by a list of components topologically ordered.
configData [Gtk_helper.Configuration]
configData [Cilconfig]
The configuration data can be of several types *
consolidated_status [Property_status.Consolidation]
constant [Logic_ptree]
constant [Cil_types]
Literal constants
constant [Cabs]
constructor_kind [Cil_types]
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
daemon [Db]
Registered daemon on progress.
data [State_builder.Weak_hashtbl]
data [Datatype.Sub_caml_weak_hashtbl]
data [Dataflow2.StmtStartData]
data [State_builder.Ref]
Type of the referenced value.
data [State_builder.Hashtbl]
data_in_list [State_builder.List_ref]
deallocation [Base]
Whether the allocated base has been obtained via calls to malloc/calloc/realloc (Malloc), alloca (Alloca), or is related to a variable-length array (VLA).
decide_fast [Hptmap_sig.S]
decl [Logic_ptree]
global declarations.
decl_node [Logic_ptree]
decl_type [Cabs]
default_contents [Lmap]
Contents of a variable when it is not present in the state.
definition [Cabs]
demon [Gtk_form]
deps [Logic_ptree]
dependencies of an assigned location.
deps [Cil_types]
dependencies of an assigned location.
dot [Dotgraph]
Buffer to a dot file with a graph environment (nodes, edges, etc.)

E
edge [Service_graph]
edge [Interpreted_automata]
element [Markdown]
elements [Markdown]
elt [State_builder.Hashcons]
The type of the elements that are hash-consed
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 [Hptset.S_Basic_Compare]
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 included) to value v in the map.
entry [Menu_manager]
enum_item [Cabs]
enuminfo [Cil_types]
Information about an enumeration.
enumitem [Cil_types]
event [Log]
existence [Filepath]
Existence requirement on a file.
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]
expand [Wbox]
Expansion Modes.
expression [Cabs]
ext_category [Cil_types]
Where are we expected to find corresponding extension keyword.
ext_code_annot_context [Cil_types]
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
extended_loc [Property]
extension [Logic_ptree]
extension_preprocessor [Acsl_extension]
Untyped ACSL extensions transformers
extension_printer [Acsl_extension]
extension_typer [Acsl_extension]
Transformers from untyped to typed ACSL extension
extension_visitor [Acsl_extension]
Pretty printers for ACSL extensions

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 type, according to how it will be preprocessed.
file [Cil_types]
The top-level representation of a CIL source file (and the result of the parsing and elaboration).
file [Cabs]
the file name, and then the list of toplevel forms.
filekind [Wfile]
filetree_node [Filetree]
fkind [Cil_types]
Various kinds of floating-point numbers
float [Float_interval_sig.S]
Type of the interval bounds.
for_clause [Cabs]
formatArg [Cil]
The type of argument for the interpreter
formatter [Pretty_utils]
formatter2 [Pretty_utils]
formatter_stag_functions [Transitioning.Format]
from [Logic_ptree]
from [Cil_types]
funbehavior [Cil_types]
behavior of a function.
fundec [Cil_types]
Function definitions.
funspec [Cil_types]
funspec [Cabs]
fuzzy_order [Rangemap]

G
gen_accessor [Typed_parameter]
generic_widen_hint [Int_val]
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.
goto_annot [Oneret]
graph [Service_graph.S]
graph [Interpreted_automata]
guard_kind [Interpreted_automata]
guardaction [Dataflow2]
For if statements

H
history_elt [History]
how_to_journalize [Db]
How to journalize the given function.
href [Markdown]
Local refs and URLs

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_extended [Property]
identified_from [Property]
identified_global_invariant [Property]
identified_instance [Property]
Specialization of a property at a given point, identified by a statement and a function, along with the predicate transposed at this point (if it can be) and the original property.
identified_lemma [Property]
identified_other [Property]
identified_predicate [Property]
identified_predicate [Cil_types]
predicate with an unique identifier.
identified_property [Property]
identified_reachable [Property]
NoneKglobal --> global property NoneSome ki --> 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 [Logic_ptree]
Pragmas for the impact plugin of Frama-C.
impact_pragma [Cil_types]
Pragmas for the impact plugin of Frama-C.
inconsistent [Property_status]
info [Type.Heterogeneous_table]
info [Interpreted_automata]
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]
inline [Markdown]
instr [Cil_types]
Instructions.
internal_tbl [Emitter.Make_table]
intervals [Offsetmap_bitwise_sig]
itv [Int_Intervals_sig]

J
json [Json]
Json Objects

K
kernel_function [Cil_types]
Only field fundec can be used 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 [Map_lattice.MapSet_Lattice]
key [Map_lattice.MapSet_Lattice_with_cardinality]
key [Map_lattice.Map_Lattice_with_cardinality]
key [Locations.Location_Bytes.M]
key [Parameter_sig.Map]
Type of keys of the map.
key [Hptmap_sig.S]
type of the keys
key [Hook.S_ordered]
key [Dotgraph.Map]
key [State_builder.Hashtbl]
kf [Description]
kind [State_builder.Proxy]
kind [Origin]
kind [Log]
kind [Gtk_helper.Icon]
kind [Fval]
kind [Emitter]
kinstr [Cil_types]

L
l [Lattice_type.Lattice_Base]
label [Cil_types]
Labels
labels [Interpreted_automata]
Maps binding the labels from an annotation to the vertices they refer to in the graph.
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
link [Dotgraph]
lmap [Lmap_sig]
lmap [Lmap_bitwise.Location_map_bitwise]
local_env [Cabs2cil]
local information needed to typecheck expressions and statements
local_init [Cil_types]
Initializers for local variables.
localisation [Cil_types]
localizable [Printer_tag]
The kind of object that can be selected in the source viewer.
localizable [Pretty_source]
location [Logic_ptree]
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_builtin_label [Cil_types]
builtin logic labels defined in ACSL.
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 [Logic_ptree]
loop_pragma [Cil_types]
Pragmas for the value analysis plugin of Frama-C.
lval [Cil_types]

M
mach [Cil_types]
Definition of a machine model (architecture + compiler).
map [Map_lattice.MapSet_Lattice]
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 [Locations.Zone]
marger [Pretty_utils]
Margin accumulator (low-level API to pp_items).
message [Rich_text]
Message with tags
model_annot [Logic_ptree]
model field.
model_info [Cil_types]
model field.
mutex [Task]

N
name [Cabs]
nameKind [Cabsvisit]
name_group [Cabs]
node [Service_graph.S]
node [Dotgraph]
numerical_widen_hint [Offsetmap_lattice_with_isotropy]
numerical_widen_hint [Locations.Location_Bytes]
numerical_widen_hint [Ival]

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
ontty [Log]
or_bottom [Bottom.Type]
or_top_bottom [Bottom.Top]
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.
other_loc [Property]
overflow_kind [Alarms]
Only signed overflows and pointer downcasts are really RTEs.

P
pack [Structural_descr]
Structural descriptor used inside structures.
pandoc_markdown [Markdown]
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]
A list of strongly connected components, sorted topologically
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).
pool [Task]
position [Filepath]
Describes a position in a source file.
pragma [Logic_ptree]
The various kinds of pragmas.
pragma [Cil_types]
The various kinds of pragmas.
prec [Float_sig]
Precision of floating-point numbers: the 'single', 'double' and 'long double' C types;, the ACSL 'real' type.
prec [Float_interval_sig]
Precision of the intervals.
precedence [Type]
Precedences used for generating the minimal number of parenthesis in combination with function Type.par below.
predicate [Cil_types]
predicates with a location and an optional list of names
predicate_kind [Property]
predicate_node [Cil_types]
predicates
predicate_result [Hptmap_sig.S]
Does the given predicate hold or not.
predicate_type [Hptmap_sig.S]
Existential (||) or universal (&&) predicates.
pref [Wto.Make]
partial order of preference for the choice of the head of a loop
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]
record [Dotgraph]
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]
returns_clause [Oneret]
round [Float_sig]
Rounding modes defined in the C99 standard.

S
server [Task]
set [Map_lattice.MapSet_Lattice]
set_or_top [Int_set]
Sets whose cardinal exceeds a certain limit must be converted into intervals.
set_or_top_or_bottom [Int_set]
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 [Locations.Location_Bytes]
size_widen_hint [Ival]
size_widen_hint [Int_val]
slice_pragma [Logic_ptree]
Pragmas for the slicing plugin of Frama-C.
slice_pragma [Cil_types]
Pragmas for the slicing plugin of Frama-C.
spec [Logic_ptree]
Function or statement contract.
spec [Cil_types]
Function or statement contract.
spec_elem [Cabs]
specifier [Cabs]
stag [Transitioning.Format]
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]
stmtkind [Cil_types]
storage [Cil_types]
Storage-class information
storage [Cabs]
structure [Unmarshal]
structure [Structural_descr]
Description with details.
style [Widget]
sum [Lattice_type.Lattice_Sum]
syntactic_scope [Cil_types]
Various syntactic scopes through which an identifier might be searched.

T
t [Warning_manager]
Type of the widget containing the warnings.
t [Visitor_behavior]
How the visitor should behave in front of mutable fields: in place modification or copy of the structure.
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 [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.MapSet_Lattice]
t [Logic_typing.Lenv]
t [Locations.Zone]
t [Locations.Location_Bytes.M]
Mapping from bases to bytes-expressed offsets
t [Locations.Location_Bytes]
t [Lattice_type.Lattice_Base]
t [Lattice_type.Lattice_UProduct]
t [Lattice_type.Lattice_Product]
t [Lattice_type.With_Diff_One]
t [Lattice_type.With_Diff]
t [Lattice_type.With_Under_Approximation]
t [Lattice_type.With_Narrow]
t [Lattice_type.With_Top_Opt]
t [Lattice_messages]
t [Json]
t [Ival]
t [Interpreted_automata.Domain]
States propagated by the dataflow analysis.
t [Integer]
t [Indexer.Elt]
t [Indexer.Make]
t [Hptset.S_Basic_Compare]
t [Hptmap.Shape]
t [Hook.Comparable]
t [Fval.F]
t [Float_sig.S]
t [Float_interval_sig.S]
Type of intervals.
t [Eva_lattice_type.With_Diff_One]
t [Eva_lattice_type.With_Diff]
t [Eva_lattice_type.With_Under_Approximation]
t [Eva_lattice_type.With_Narrow]
t [Lattice_type.With_Widening]
t [Lattice_type.With_Cardinal_One]
t [Lattice_type.With_Enumeration]
t [Lattice_type.With_Intersects]
t [Lattice_type.With_Top]
t [Dynamic.Parameter.Common]
t [Dotgraph.Map]
t [Dotgraph.Node]
t [Descr]
Type of a type descriptor.
t [Db.INOUTKF]
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 [Cmdline.Group]
t [Filepath.Normalized]
The normalized (absolute) path.
t [Bitvector]
t [Binary_cache.Result]
t [Binary_cache.Cacheable]
t [Bag]
t [Lattice_type.Lattice_Set]
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_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.
table [Markdown]
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.
text [Markdown]
Inline elements separated by spaces
theMachine [Cil]
thread [Task]
timer [Command]
token [Logic_parser]
token [Cparser]
transition [Interpreted_automata]
Each transition can either be a skip (do nothing), a return, a guard represented by a Cil expression, a Cil instruction, an ACSL annotation or entering/leaving a block.
truth [Abstract_interp]
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 [Map_lattice.MapSet_Lattice]
v [Map_lattice.MapSet_Lattice_with_cardinality]
v [Map_lattice.Map_Lattice_with_cardinality]
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 of a loop or a recursive function.
variant [Cil_types]
variant of a loop or a recursive function.
varinfo [Cil_types]
Information about a variable.
vertex [Service_graph]
vertex [Interpreted_automata]
visitAction [Cil]
Different visiting actions.

W
warn_category [Log.Messages]
Same as above, but for warnings
warn_status [Log]
status of a warning category
wchar [Escape]
where [Menu_manager]
Where to put a new entry.
widen_hint [Offsetmap_sig]
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
widen_hints [Float_sig.S]
widen_hints [Float_interval_sig.S]
Type of the widen hints.
wstring [Escape]
wto [Wto_statement]
A weak topological ordering where nodes are Cil statements
wto [Interpreted_automata]
Weak Topological Order is given by a list (in topological order) of components of the graph, which are themselves WTOs
wto_index [Wto_statement]
the position of a statement in a wto given as the list of component heads
wto_index [Interpreted_automata]
the position of a statement in a wto given as the list of component heads
wto_index_table [Interpreted_automata.Compute]