Index of types

A
a_kind [WpPropId]
a_kind [Wp.WpPropId]
access [RefUsage]

By lattice order of usage

access [Wp.RefUsage]

By lattice order of usage

acs [Sigs]

Access conditions

acs [Wp.Sigs]

Access conditions

adt [Lang]
adt [Wp.Lang]
alias [Layout]
alternative [ProofScript]
annot_kind [WpStrategy]

An annotation can be used for different purpose.

annotation [Interpreted_automata]
annots_tbl [WpStrategy]
argument [Strategy]
argument [Wp.Strategy]
arrayflat [Ctypes]

Array objects, with both the head view and the flatten view.

arrayflat [Wp.Ctypes]

Array objects, with both the head view and the flatten view.

arrayinfo [Ctypes]
arrayinfo [Wp.Ctypes]
asked_assigns [WpAnnot]
assert_kind [Interpreted_automata]
assigns_desc [WpPropId]
assigns_desc [Wp.WpPropId]
assigns_full_info [WpPropId]
assigns_full_info [Wp.WpPropId]
assigns_info [WpPropId]
assigns_info [Wp.WpPropId]
attributed [Conditions]
attributed [Wp.Conditions]
automaton [Interpreted_automata]
axiom_info [WpPropId]
axiom_info [Wp.WpPropId]
axiomatic [LogicUsage]
axiomatic [Wp.LogicUsage]
axioms [Definitions]
axioms [Wp.Definitions]
B
balance [Lang]
balance [Wp.Lang]
behavior [CfgAnnot]
binder [Sigs]
binder [Wp.Sigs]
binding [Passive]
binding [Wp.Passive]
bindings [TacInstance]
binop [Lang.F]
binop [Wp.Lang.F]
block_scope [Cil2cfg]
block_type [Cil2cfg]

Be careful that only Bstmt are real Block statements

browser [Tactical]
browser [Wp.Tactical]
builtin [LogicBuiltins]
builtin [Wp.LogicBuiltins]
bundle [Conditions]
bundle [Wp.Conditions]
C
c_float [Ctypes]

Runtime floats.

c_float [Wp.Ctypes]

Runtime floats.

c_int [Ctypes]

Runtime integers.

c_int [Wp.Ctypes]

Runtime integers.

c_label [Clabels]
c_label [Wp.Clabels]
c_object [Ctypes]

Type of variable, inits, field or assignable values.

c_object [Wp.Ctypes]

Type of variable, inits, field or assignable values.

cache [Layout.Offset]
call [GuiSource]
call [Sigs.LogicSemantics]

Internal call data.

call [LogicCompiler.Make]
call [Wp.LogicCompiler.Make]
call [Wp.Sigs.LogicSemantics]

Internal call data.

call_type [Cil2cfg]
callback [GuiTactic]
category [LogicBuiltins]
category [Wp.LogicBuiltins]
cfg [StmtSemantics.Make]
cfg [CfgCompiler.Cfg]

Structured collection of traces.

cfg [Wp.StmtSemantics.Make]
cfg [Wp.CfgCompiler.Cfg]

Structured collection of traces.

chunk [LogicCompiler.Make]
chunk [Sigs.Sigma]

The type of memory chunks.

chunk [Sigs.Model]
chunk [Layout]
chunk [Wp.LogicCompiler.Make]
chunk [Wp.Sigs.Model]
chunk [Wp.Sigs.Sigma]

The type of memory chunks.

chunks [Layout]
clause [Tactical]
clause [Wp.Tactical]
cluster [Definitions]
cluster [Layout]
cluster [Wp.Definitions]
cmp [Lang.F]
cmp [Wp.Lang.F]
code_assertions [CfgAnnot]
command [Rformat]
compose [Tactical]
compose [Wp.Tactical]
condition [Conditions]
condition [Wp.Conditions]
config [VCS]
config [Wp.VCS]
context [WpContext]
context [Warning]
context [Wp.WpContext]
context [Wp.Warning]
contract [CfgAnnot]
control [Interpreted_automata]

Control flow informations for outgoing edges, if any.

cst [Cstring]
cst [Wp.Cstring]
current [ProofEngine]
D
data [WpContext.IData]
data [WpContext.Data]
data [WpContext.Generator]
data [WpContext.Entries]
data [WpContext.Registry]
data [Wp.WpContext.IData]
data [Wp.WpContext.Data]
data [Wp.WpContext.Generator]
data [Wp.WpContext.Entries]
data [Wp.WpContext.Registry]
datakind [Lang]
datakind [Wp.Lang]
decl [Mcfg.Export]
decl [Wp.Mcfg.Export]
definition [Definitions]
definition [Wp.Definitions]
deref [Layout]
dfun [Definitions]
dfun [Wp.Definitions]
digest [Cache]
dim [Layout]
dir [TacRewrite]
dlemma [Definitions]
dlemma [Wp.Definitions]
domain [Sigs.Sigma]

Memory footprint.

domain [Sigs.Model]
domain [Wp.Sigs.Model]
domain [Wp.Sigs.Sigma]

Memory footprint.

doption [LogicBuiltins]
doption [Wp.LogicBuiltins]
driver [Factory]
driver [LogicBuiltins]
driver [Wp.Factory]
driver [Wp.LogicBuiltins]
E
edge [Interpreted_automata]
edge [Cil2cfg]

abstract type of the cfg edges

effect_source [WpPropId]
effect_source [Wp.WpPropId]
elt [Set.S]

The type of the set elements.

env [GuiSequent]
env [StmtSemantics.Make]
env [Sigs.LogicSemantics]

Compilation environment for terms and predicates.

env [LogicCompiler.Make]
env [Pcond]
env [Pcfg]
env [Letify.Ground]
env [Matrix]
env [Lang.F]
env [Wp.StmtSemantics.Make]
env [Wp.LogicCompiler.Make]
env [Wp.Pcond]
env [Wp.Pcfg]
env [Wp.Sigs.LogicSemantics]

Compilation environment for terms and predicates.

env [Wp.Lang.F]
equation [Sigs]

Oriented equality or arbitrary relation

equation [Wp.Sigs]

Oriented equality or arbitrary relation

extern [Lang]
extern [Wp.Lang]
F
fallback [Why3Provers]
fcstat [WpReport]
field [Tactical]
field [Repr]
field [Lang]
field [Wp.Tactical]
field [Wp.Repr]
field [Wp.Lang]
fields [Lang]
fields [Wp.Lang]
fork [ProofEngine]
formatter [Tactical]
formatter [Wp.Tactical]
formula [Wpo]
formula [Wp.Wpo]
frame [Sigs]

Frame Conditions.

frame [Sigs.LogicSemantics]
frame [LogicCompiler.Make]
frame [Wp.LogicCompiler.Make]
frame [Wp.Sigs.LogicSemantics]
frame [Wp.Sigs]

Frame Conditions.

from [Layout]
functions [Wp_parameters]
functions [Wp.Wp_parameters]
G
gamma [Lang]
gamma [Wp.Lang]
goal [StmtSemantics.Make]
goal [Wp.StmtSemantics.Make]
graph [Interpreted_automata]
guard_kind [Interpreted_automata]
H
hypotheses [WpContext]
hypotheses [Wp.WpContext]
I
iformat [Plang]
iformat [Wp.Plang]
index [Wpo]
index [Wp.Wpo]
info [Interpreted_automata]
infoprover [Lang]

Name for external prover.

infoprover [Wp.Lang]

Name for external prover.

input [Script]
J
jscript [ProofScript]
jtactic [ProofScript]
K
key [WpContext.IData]
key [WpContext.Data]
key [WpContext.Generator]
key [WpContext.Entries]
key [WpContext.Registry]
key [Wprop.Info]
key [Wprop.Indexed]
key [Wp.WpContext.IData]
key [Wp.WpContext.Data]
key [Wp.WpContext.Generator]
key [Wp.WpContext.Entries]
key [Wp.WpContext.Registry]
key [Hashtbl.S]
key [Map.S]

The type of the map keys.

key1 [Wprop.Indexed2]
key2 [Wprop.Indexed2]
kind [LogicBuiltins]
kind [Wp.LogicBuiltins]
L
label [Pcfg]
label [Wp.Pcfg]
label_mapping [NormAtLabels]
label_mapping [Wp.NormAtLabels]
labeling [Interpreted_automata]
labels [Interpreted_automata]

Maps binding the labels from an annotation to the vertices they refer to in the graph.

layout [Layout]
lemma [TacLemma]
lfun [Repr]
lfun [Lang]
lfun [Wp.Repr]
lfun [Wp.Lang]
library [Lang]
library [Wp.Lang]
lnode [RegionAnnot]
loc [MemLoader.Model]
loc [Sigs.LogicSemantics]
loc [Sigs.Model]

Representation of the memory location in the model.

loc [Sigs.CodeSemantics]
loc [Wp.Sigs.LogicSemantics]
loc [Wp.Sigs.CodeSemantics]
loc [Wp.Sigs.Model]

Representation of the memory location in the model.

logic [Sigs]

Logical values, locations, or sets of

logic [Sigs.LogicSemantics]
logic [LogicCompiler.Make]
logic [Cvalues.Logic]
logic [Wp.LogicCompiler.Make]
logic [Wp.Sigs.LogicSemantics]
logic [Wp.Sigs]

Logical values, locations, or sets of

logic_lemma [LogicUsage]
logic_lemma [Wp.LogicUsage]
logic_section [LogicUsage]
logic_section [Wp.LogicUsage]
logs [ProverTask]
logs [Wp.ProverTask]
loop_contract [CfgAnnot]
lpath [RegionAnnot]
lrange [RegionAnnot]
lvalue [Layout]
M
map [Region]
marks [Lang.F]
marks [Wp.Lang.F]
matrixinfo [Cvalues]
mdt [Lang]

name to print to the provers

mdt [Wp.Lang]

name to print to the provers

merger [Layout]
mheap [Factory]
mheap [Wp.Factory]
mode [CfgCalculus]
mode [Cache]
mode [TacCut]
mode [VCS]
mode [CfgCompiler]
mode [Wp.VCS]
mode [Wp.CfgCompiler]
model [Mstate]
model [Cfloat]
model [Cint]
model [Lang]
model [WpContext]
model [Wp.Mstate]
model [Wp.Cfloat]
model [Wp.Cint]
model [Wp.Lang]
model [Wp.WpContext]
mval [Sigs]

Reversed abstract value

mval [Wp.Sigs]

Reversed abstract value

mvar [Factory]
mvar [Wp.Factory]
N
named [Tactical]
named [Wp.Tactical]
node [ProofEngine]

A proof node

node [StmtSemantics.Make]
node [CfgCompiler.Cfg]
node [Cil2cfg]

abstract type of the cfg nodes

node [Wp.StmtSemantics.Make]
node [Wp.CfgCompiler.Cfg]
node_type [Cil2cfg]
O
occur [Letify.Split]
occurrence [Footprint]

k-th occurrence of the footprint in a term

offset [Layout]
op [Cfloat]
op [Wp.Cfloat]
operator [Lang.F]
operator [Wp.Lang.F]
outcome [Warning]
outcome [Wp.Warning]
overlay [Layout]
P
param [MemoryContext]
param [Wp.MemoryContext]
parameter [Tactical]
parameter [Wp.Tactical]
partition [MemoryContext]
partition [Wp.MemoryContext]
paths [StmtSemantics.Make]
paths [Wp.StmtSemantics.Make]
po [Wpo]
po [Wp.Wpo]
pointer [MemTyped]
pointer [Wp.MemTyped]
polarity [Sigs]

Polarity of predicate compilation

polarity [LogicCompiler]
polarity [Cvalues]

positive goal negative hypothesis

polarity [Wp.LogicCompiler]
polarity [Wp.Sigs]

Polarity of predicate compilation

pool [Plang]
pool [Lang.F]
pool [Wp.Plang]
pool [Wp.Lang.F]
position [ProofEngine]
pred [Mcfg.Splitter]
pred [Mcfg.Export]
pred [Repr]
pred [Lang.F]
pred [Wp.Repr]
pred [Wp.Lang.F]
pred [Wp.Mcfg.Splitter]
pred [Wp.Mcfg.Export]
pred_info [WpPropId]
pred_info [Wp.WpPropId]
printer [GuiSequent]
printer [Cvalues]
process [ProverScript]
process [Tactical]
process [Wp.Tactical]
proof [WpPropId]

A proof accumulator for a set of related prop_id

proof [Wp.WpPropId]

A proof accumulator for a set of related prop_id

prop_id [WpPropId]

Property.t information and kind of PO (establishment, preservation, etc)

prop_id [Wp.WpPropId]

Property.t information and kind of PO (establishment, preservation, etc)

prop_kind [WpPropId]
prop_kind [Wp.WpPropId]
property [Wprop]
props [CfgCalculus]
prover [VCS]
prover [Wp.VCS]
R
range [Tactical]
range [Layout]
range [Wp.Tactical]
reachability [WpReached]

control flow graph dedicated to smoke tests

record [Lang.F]
record [Wp.Lang.F]
recursion [Definitions]
recursion [Wp.Definitions]
region [Sigs]

Typed set of locations

region [Sigs.LogicSemantics]
region [Cvalues.Logic]
region [Region]
region [Wp.Sigs.LogicSemantics]
region [Wp.Sigs]

Typed set of locations

region_pattern [RegionAnnot]
region_spec [RegionAnnot]
repr [Repr]
repr [Wp.Repr]
result [Sigs]

Container for the returned value of a function

result [Interpreted_automata.DataflowAnalysis]
result [VCS]
result [Sigs.LogicSemantics]
result [LogicCompiler.Make]
result [Sigs.CodeSemantics]
result [Wp.VCS]
result [Wp.LogicCompiler.Make]
result [Wp.Sigs.LogicSemantics]
result [Wp.Sigs.CodeSemantics]
result [Wp.Sigs]

Container for the returned value of a function

rformat [Plang]
rformat [Wp.Plang]
rg [Auto.Range]
rg [Wp.Auto.Range]
rloc [Sigs]

Contiguous set of locations

rloc [Wp.Sigs]

Contiguous set of locations

rollback [WpContext]
rollback [Wp.WpContext]
root [Layout]
runner [Cache]
S
s_host [Sigs]
s_host [Wp.Sigs]
s_lval [Sigs]

Reversed ACSL left-value

s_lval [Wp.Sigs]

Reversed ACSL left-value

s_offset [Sigs]
s_offset [Wp.Sigs]
sanitizer [LogicBuiltins]
sanitizer [Wp.LogicBuiltins]
scope [Mcfg]
scope [Sigs]

Scope management for locals and formals

scope [Plang]
scope [WpContext]
scope [Wp.Plang]
scope [Wp.Sigs]

Scope management for locals and formals

scope [Wp.WpContext]
scope [Wp.Mcfg]
script [ProofSession]
segment [Sigs.Model]
segment [Cvalues.Logic]
segment [Wp.Sigs.Model]
selection [GuiSource]
selection [Tactical]
selection [Wp.Tactical]
sequence [Sigs]
sequence [Conditions]

List of steps

sequence [Wp.Conditions]

List of steps

sequence [Wp.Sigs]
sequent [Conditions]
sequent [Wp.Conditions]
set [Vset]
set [Wp.Vset]
setup [Factory]
setup [Wp.Factory]
sigma [Sigs.LogicSemantics]
sigma [LogicCompiler.Make]
sigma [Sigs.Model]
sigma [Sigs.CodeSemantics]
sigma [Lang.F]
sigma [Wp.LogicCompiler.Make]
sigma [Wp.Sigs.LogicSemantics]
sigma [Wp.Sigs.CodeSemantics]
sigma [Wp.Sigs.Model]
sigma [Wp.Lang.F]
sloc [Sigs]

Structured set of locations

sloc [Wp.Sigs]

Structured set of locations

source [Lang]
source [Wp.Lang]
specific_equality [Lang.For_export]
specific_equality [Wp.Lang.For_export]
state [Interpreted_automata.DataflowAnalysis]
state [MemVal.Value]
state [Sigs.Model]

Internal (private) memory state description for later reversing the model.

state [Mstate]
state [Wp.MemVal.Value]
state [Wp.Mstate]
state [Wp.Sigs.Model]

Internal (private) memory state description for later reversing the model.

status [ProofEngine]
status [Tactical]
status [Wp.Tactical]
step [Conditions]
step [Wp.Conditions]
strategy [Strategy]
strategy [WpStrategy]
strategy [Wp.Strategy]
strategy_for_froms [WpStrategy]
strategy_kind [WpStrategy]
subst [Letify.Ground]
T
t [VC]

elementary proof obligation

t [Interpreted_automata.Domain]

States propagated by the dataflow analysis.

t [CfgInfos]
t [Strategy]
t [Tactical.Fmap]
t [Tactical]
t [Wpo.VC_Annot]
t [Wpo.VC_Lemma]
t [Wpo.GOAL]
t [Wpo]
t [CfgCompiler.Cfg.E]
t [CfgCompiler.Cfg.T]
t [CfgCompiler.Cfg.P]
t [CfgCompiler.Cfg.C]
t [CfgCompiler.Cfg.Node]
t [MemVal.State]

abstract state *

t [MemVal.Value]

abstract value *

t [Sigs.Sigma]

Environment assigning logic variables to chunk.

t [Sigs.Chunk]
t [Letify.Defs]
t [Letify.Sigma]
t [Splitter]
t [Passive]
t [Matrix]

Matrix dimensions.

t [Cil2cfg.HEsig]
t [Cil2cfg]

abstract type of a cfg

t [RegionAnnot.Lpath]
t [Layout.Data]
t [WpContext.Key]
t [WpContext.SCOPE]
t [WpContext.MODEL]
t [WpContext.S]
t [WpContext]
t [Clabels.T]
t [Ctypes.AinfoComparable]
t [Warning]
t [Why3Provers]
t [Map.OrderedType]

The type of the map keys.

t [Wp.Wpo.VC_Annot]
t [Wp.Wpo.VC_Lemma]
t [Wp.Wpo.GOAL]
t [Wp.Wpo]
t [Wp.VC]

elementary proof obligation

t [Wp.Strategy]
t [Wp.Tactical.Fmap]
t [Wp.Tactical]
t [Wp.CfgCompiler.Cfg.E]
t [Wp.CfgCompiler.Cfg.T]
t [Wp.CfgCompiler.Cfg.P]
t [Wp.CfgCompiler.Cfg.C]
t [Wp.CfgCompiler.Cfg.Node]
t [Wp.MemVal.State]

abstract state *

t [Wp.MemVal.Value]

abstract value *

t [Wp.Sigs.Sigma]

Environment assigning logic variables to chunk.

t [Wp.Sigs.Chunk]
t [Wp.Splitter]
t [Wp.Passive]
t [Wp.WpContext.Key]
t [Hashtbl.S]
t [Wp.WpContext.SCOPE]
t [Wp.WpContext.MODEL]
t [Wp.WpContext.S]
t [Wp.WpContext]
t [Wp.Warning]
t [Set.S]

The type of sets.

t [Map.S]

The type of maps from type key to type 'a.

t [Wp.Clabels.T]
t [Wp.Ctypes.AinfoComparable]
t_annots [WpStrategy]

a set of annotations to be added to a program point.

t_builtin [Lang]
t_builtin [Wp.Lang]
t_env [Mcfg.S]
t_env [Wp.Mcfg.S]
t_prop [Mcfg.S]
t_prop [Wp.Mcfg.S]
tag [Splitter]
tag [Wp.Splitter]
target [GuiSequent]
tau [Repr]
tau [Lang.F]
tau [Lang]
tau [Wp.Repr]
tau [Wp.Lang.F]
tau [Wp.Lang]
term [Repr]
term [Lang.F]
term [Wp.Repr]
term [Wp.Lang.F]
ti [Cil2cfg.HEsig]
token [Script]
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.

tree [ProofEngine]

A proof tree

trigger [Definitions]
trigger [Wp.Definitions]
typedef [Definitions]
typedef [Wp.Definitions]
U
unop [Lang.F]
unop [Wp.Lang.F]
update [Sigs]

Reversed update

update [Wp.Sigs]

Reversed update

usage [Cleaning]
usage [Layout]
V
validity [MemoryContext]
validity [Wp.MemoryContext]
value [Sigs]

Abstract location or concrete value

value [Sigs.LogicSemantics]
value [LogicCompiler.Make]
value [Sigs.CodeSemantics]
value [Pcfg]
value [Layout]
value [Context]
value [Wp.LogicCompiler.Make]
value [Wp.Pcfg]
value [Wp.Sigs.LogicSemantics]
value [Wp.Sigs.CodeSemantics]
value [Wp.Sigs]

Abstract location or concrete value

value [Wp.Context]
var [Repr]
var [Lang.F]
var [Wp.Repr]
var [Wp.Lang.F]
variant_info [WpPropId]
variant_info [Wp.WpPropId]
verdict [VCS]
verdict [Wp.VCS]
vertex [Interpreted_automata]
vset [Vset]
vset [Wp.Vset]
W
warned_hyp [Sigs.CodeSemantics]
warned_hyp [Wp.Sigs.CodeSemantics]
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 [Interpreted_automata]

the position of a statement in a wto given as the list of component heads

wto_index_table [Interpreted_automata.Compute]