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.
|
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] |
|
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] |
|
axiom_info [WpPropId] |
|
axiom_info [Wp.WpPropId] |
|
axiomatic [LogicUsage] |
|
axiomatic [Wp.LogicUsage] |
|
axioms [Definitions] |
|
axioms [Wp.Definitions] |
|
B |
balance [Lang] |
|
balance [Wp.Lang] |
|
binder [Sigs] |
|
binder [Wp.Sigs] |
|
binding [Passive] |
|
binding [Wp.Passive] |
|
bindings [TacInstance] |
|
binop [Lang.F] |
|
binop [Wp.Lang.F] |
|
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 [LogicCompiler.Make] |
|
call [Sigs.LogicSemantics] |
Internal call data.
|
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.Model] |
|
chunk [Sigs.Sigma] |
The type of memory chunks.
|
chunk [Layout] |
|
chunk [Wp.LogicCompiler.Make] |
|
chunk [Wp.Sigs.Model] |
|
chunk [Wp.Sigs.Sigma] |
The type of memory chunks.
|
chunks [Layout] |
|
clause [Tactical] |
|
clause [MemoryContext] |
|
clause [Wp.Tactical] |
|
clause [Wp.MemoryContext] |
|
cluster [Definitions] |
|
cluster [Layout] |
|
cluster [Wp.Definitions] |
|
cmp [Lang.F] |
|
cmp [Wp.Lang.F] |
|
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] |
|
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] |
|
decl [Mcfg.Export] |
|
decl [Wp.Mcfg.Export] |
|
definition [Definitions] |
|
definition [Wp.Definitions] |
|
denv [Matrix] |
|
deref [Layout] |
|
dfun [Definitions] |
|
dfun [Wp.Definitions] |
|
dim [Matrix] |
|
dim [Layout] |
|
dir [TacRewrite] |
|
dlemma [Definitions] |
|
dlemma [Wp.Definitions] |
|
domain [Sigs.Model] |
|
domain [Sigs.Sigma] |
Memory footprint.
|
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 [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 [LogicCompiler.Make] |
|
env [Pcond] |
|
env [Pcfg] |
|
env [Sigs.LogicSemantics] |
Compilation environment for terms and predicates.
|
env [Letify.Ground] |
|
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 |
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 [LogicCompiler.Make] |
|
frame [Sigs.LogicSemantics] |
|
frame [Sigs] |
Frame Conditions.
|
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] |
|
H |
hypotheses [WpContext] |
|
hypotheses [Wp.WpContext] |
|
I |
iformat [Plang] |
|
iformat [Wp.Plang] |
|
index [Wpo] |
|
index [Wp.Wpo] |
|
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 [Map.S] |
The type of the map keys.
|
key [Hashtbl.S] |
|
key [Wp.WpContext.IData] |
|
key [Wp.WpContext.Data] |
|
key [Wp.WpContext.Generator] |
|
key [Wp.WpContext.Entries] |
|
key [Wp.WpContext.Registry] |
|
key [FCMap.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] |
|
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.CodeSemantics] |
|
loc [Sigs.Model] |
Representation of the memory location in the model.
|
loc [Wp.Sigs.LogicSemantics] |
|
loc [Wp.Sigs.CodeSemantics] |
|
loc [Wp.Sigs.Model] |
Representation of the memory location in the model.
|
logic [LogicCompiler.Make] |
|
logic [Sigs.LogicSemantics] |
|
logic [Sigs] |
Logical values, locations, or sets of
|
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] |
|
lpath [RegionAnnot] |
|
lrange [RegionAnnot] |
|
lvalue [Layout] |
|
M |
map [Region] |
|
marks [Lang.F] |
|
marks [Wp.Lang.F] |
|
matrix [Matrix] |
|
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 [Register] |
|
mode [ProverWhy3] |
|
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 [LogicCompiler] |
|
polarity [Sigs] |
Polarity of predicate compilation
|
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 [Repr] |
|
pred [Lang.F] |
|
pred [Mcfg.Splitter] |
|
pred [Mcfg.Export] |
|
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 [WpAnnot] |
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] |
|
prover [VCS] |
|
prover [Wp.VCS] |
|
pstat [Register] |
|
R |
range [Tactical] |
|
range [Layout] |
|
range [Wp.Tactical] |
|
record [Lang.F] |
|
record [Wp.Lang.F] |
|
recursion [Definitions] |
|
recursion [Wp.Definitions] |
|
region [Sigs.LogicSemantics] |
|
region [Sigs] |
Typed set of locations
|
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 [VCS] |
|
result [LogicCompiler.Make] |
|
result [Sigs.LogicSemantics] |
|
result [Sigs.CodeSemantics] |
|
result [Sigs] |
Container for the returned value of a function
|
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
|
root [Layout] |
|
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 [Plang] |
|
scope [Sigs] |
Scope management for locals and formals
|
scope [Mcfg] |
|
scope [WpContext] |
|
scope [Wp.Plang] |
|
scope [Wp.Sigs] |
Scope management for locals and formals
|
scope [Wp.WpContext] |
|
scope [Wp.Mcfg] |
|
segment [Sigs.Model] |
|
segment [Cvalues.Logic] |
|
segment [Wp.Sigs.Model] |
|
selection [GuiSource] |
|
selection [Tactical] |
|
selection [Wp.Tactical] |
|
sequence [Conditions] |
List of steps
|
sequence [Sigs] |
|
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 [LogicCompiler.Make] |
|
sigma [Sigs.LogicSemantics] |
|
sigma [Sigs.CodeSemantics] |
|
sigma [Sigs.Model] |
|
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 [ProofEngine] |
|
state [Mstate] |
|
state [Sigs.Model] |
Internal (private) memory state description for later reversing the model.
|
state [Wp.Mstate] |
|
state [Wp.Sigs.Model] |
Internal (private) memory state description for later reversing the model.
|
status [ProofEngine] |
|
status [ProofSession] |
|
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 [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 [Sigs.Sigma] |
Environment assigning logic variables to chunk.
|
t [Sigs.Chunk] |
|
t [Letify.Defs] |
|
t [Letify.Sigma] |
|
t [Splitter] |
|
t [Passive] |
|
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 [Warning] |
|
t [Why3Provers] |
|
t [Clabels.T] |
|
t [Ctypes.AinfoComparable] |
|
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 [Map.S] |
The type of maps from type key to type 'a .
|
t [Set.S] |
The type of sets.
|
t [Wp.CfgCompiler.Cfg.E] |
|
t [Wp.CfgCompiler.Cfg.T] |
|
t [Wp.CfgCompiler.Cfg.P] |
|
t [Wp.CfgCompiler.Cfg.C] |
|
t [Hashtbl.S] |
|
t [Wp.CfgCompiler.Cfg.Node] |
|
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 [Wp.WpContext.SCOPE] |
|
t [Wp.WpContext.MODEL] |
|
t [Wp.WpContext.S] |
|
t [Wp.WpContext] |
|
t [Wp.Warning] |
|
t [FCMap.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_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] |
|
tree [ProofEngine] |
A proof tree
|
trigger [Definitions] |
|
trigger [Wp.Definitions] |
|
tuning [WpContext] |
|
tuning [Wp.WpContext] |
|
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 |
value [LogicCompiler.Make] |
|
value [Pcfg] |
|
value [Sigs.LogicSemantics] |
|
value [Sigs.CodeSemantics] |
|
value [Sigs] |
Abstract location or concrete value
|
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] |
|
verdict [VCS] |
|
verdict [Wp.VCS] |
|
vset [Vset] |
|
vset [Wp.Vset] |
|
W |
warned_hyp [Sigs.CodeSemantics] |
|
warned_hyp [Wp.Sigs.CodeSemantics] |
|
Z |
zone [MemoryContext] |
|
zone [Wp.MemoryContext] |
|