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] | |
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_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] | |
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 |
control [Interpreted_automata] | Control flow informations for outgoing edges, if any. |
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.Hashtbl] | |
data [State_builder.Ref] | Type of the referenced value. |
data_in_list [State_builder.List_ref] | |
deallocation [Base] | Whether the allocated base has been obtained via calls to
malloc/calloc/realloc ( |
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 |
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 |
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 |
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_decl [Logic_ptree] | |
extended_loc [Property] | |
extension [Logic_ptree] | |
extension_preprocessor [Acsl_extension] | Untyped ACSL extensions transformers |
extension_preprocessor_block [Acsl_extension] | |
extension_printer [Acsl_extension] | |
extension_typer [Acsl_extension] | Transformers from untyped to typed ACSL extension |
extension_typer_block [Acsl_extension] | Pretty printers for ACSL extensions |
extension_visitor [Acsl_extension] | |
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] | |
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. |
global_extension [Logic_ptree] | |
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_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 |
identified_decrease [Property] | code_annotation is None for decreases and |
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] |
|
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 |
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 |
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 [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 |
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 |
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 |
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_array [Ordered_stmt] | As |
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 |
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] | |
poly [Type.Polymorphic4] | |
poly [Type.Polymorphic3] | |
poly [Type.Function] | |
poly [Type.Polymorphic2] | |
poly [Type.Polymorphic] | Type of the polymorphic type (for instance |
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 |
predicate [Cil_types] | predicates with a location and an optional list of names |
predicate_kind [Property] | |
predicate_kind [Cil_types] | |
predicate_node [Cil_types] | predicates |
predicate_result [Hptmap_sig.S] | Does the given predicate hold or not. |
predicate_type [Hptmap_sig.S] | Existential ( |
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 |
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 [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] | |
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] | |
substitution [Base] | Type used for the substitution between bases. |
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 |
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] |
|
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 |
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] | |
toplevel_predicate [Logic_ptree] | |
toplevel_predicate [Cil_types] | main statement of an annotation. |
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] |