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_logic_info [Cil_types] | |
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 [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 | |
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 [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 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 [Parameter_sig] | |
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] | |
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] | |
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] |
Same as for
Property.identified_behavior .
|
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] | None, Kglobal --> global property
None, Some 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 [Parameter_sig.Map] |
Type of keys of the 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 [Hptmap_sig.S] |
type of the keys
|
key [Hook.S_ordered] | |
key [FCMap.S] |
The type of the map keys.
|
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 int 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] | |
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] | |
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_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_Opt] | |
t [Lattice_type.With_Top] | |
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 [Hptmap.Shape] | |
t [Hook.Comparable] | |
t [Fval.F] | |
t [Float_sig.S] | |
t [Float_interval_sig.S] |
Type of intervals.
|
t [FCSet.S_Basic_Compare] |
The type of sets.
|
t [FCMap.S] |
The type of maps from type
key to type 'a .
|
t [FCBuffer] |
The abstract type of buffers.
|
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] |