Index of types

A
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 [Dataflow]
action [Hptset.S]
alarm [Offsetmap_sig]

true indicates that an alarm may have occurred

alarm [Alarms]
alarm [Abstract_interp]
align [Widget]
align [Pretty_utils]
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

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.

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 [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.

bound_kind [Alarms]
box [Wbox]

A packed widget with its layout directives

buffer [Rich_text]

Buffer for creating messages.

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

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 [Dataflow.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.

E
edge [Service_graph]
edge [Interpreted_automata]
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]
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_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

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 [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

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 [Offsetmap_lattice_with_isotropy]
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.

goto_annot [Oneret]
graph [Service_graph.S]
graph [Interpreted_automata]
guard_kind [Interpreted_automata]
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_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_predicate [Property]
identified_predicate [Cil_types]

predicate with an unique identifier.

identified_property [Property]
identified_reachable [Property]

NoneKglobal --> global property NoneSome 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 [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]
instr [Cil_types]

Instructions.

internal_tbl [Emitter.Make_table]
intervals [Offsetmap_bitwise_sig]
itv [Int_Intervals_sig]
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 [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]
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

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 [Pretty_source]

The kind of object that can be selected in the source viewer.

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]
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.

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]

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]
pragma [Logic_ptree]

The various kinds of pragmas.

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 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]
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]
rootsFilter [Rmtmps]
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]
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]
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 [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 [Leftistheap.Make]
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]

Json Objects

t [Ival]
t [Integer]
t [Indexer.Elt]
t [Indexer.Make]
t [Hptmap.Shape]
t [Hook.Comparable]
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 [FCBuffer]

The abstract type of buffers.

t [Dynamic.Parameter.Common]
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 [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 [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.

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]
transition [Interpreted_automata]
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.

visitor_behavior [Cil]

Visitor behavior

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

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]