A |
A [Sigs.Compiler] |
|
A [Wp.Sigs.Compiler] |
|
ADT [Lang] |
|
ADT [Wp.Lang] |
|
Absurd [TacChoice] |
|
AinfoComparable [Ctypes] |
|
AinfoComparable [Wp.Ctypes] |
|
Alpha [Lang] |
|
Alpha [Wp.Lang] |
|
AltErgo [Wp_parameters] |
|
AltErgo [Wp.Wp_parameters] |
|
AltErgoFlags [Wp_parameters] |
|
AltErgoFlags [Wp.Wp_parameters] |
|
AltErgoLibs [Wp_parameters] |
|
AltErgoLibs [Wp.Wp_parameters] |
|
AltGrErgo [Wp_parameters] |
|
AltGrErgo [Wp.Wp_parameters] |
|
Auto |
|
Auto [Wp_parameters] |
|
Auto [Wp] |
|
Auto [Wp.Wp_parameters] |
|
AutoDepth [Wp_parameters] |
|
AutoDepth [Wp.Wp_parameters] |
|
AutoWidth [Wp_parameters] |
|
AutoWidth [Wp.Wp_parameters] |
|
B |
BackTrack [Wp_parameters] |
|
BackTrack [Wp.Wp_parameters] |
|
Behaviors [Wp_parameters] |
|
Behaviors [Wp.Wp_parameters] |
|
Bits [Wp_parameters] |
|
Bits [Wp.Wp_parameters] |
|
BoundForallUnfolding [Wp_parameters] |
|
BoundForallUnfolding [Wp.Wp_parameters] |
|
ByRef [Wp_parameters] |
|
ByRef [Wp.Wp_parameters] |
|
ByValue [Wp_parameters] |
|
ByValue [Wp.Wp_parameters] |
|
C |
C [CfgCompiler.Cfg] |
|
C [Sigs.Compiler] |
|
C [Wp.CfgCompiler.Cfg] |
|
C [Wp.Sigs.Compiler] |
|
C_object [Ctypes] |
|
C_object [Wp.Ctypes] |
|
Calculus |
|
CalleePreCond [Wp_parameters] |
|
CalleePreCond [Wp.Wp_parameters] |
|
Cfg [Calculus] |
|
Cfg [StmtSemantics.Make] |
|
Cfg [CfgCompiler] |
|
Cfg [Wp.StmtSemantics.Make] |
|
Cfg [Wp.CfgCompiler] |
|
CfgCompiler |
|
CfgCompiler [Wp] |
|
CfgDump |
|
CfgWP |
|
Cfloat |
Floating Arithmetic Model
|
Cfloat [Wp] |
|
Check [Lang.F] |
|
Check [Wp_parameters] |
|
Check [Wp.Lang.F] |
|
Check [Wp.Wp_parameters] |
|
Choice [TacChoice] |
|
Chunk [Sigs.Model] |
|
Chunk [Sigs.Sigma] |
|
Chunk [Wp.Sigs.Model] |
|
Chunk [Wp.Sigs.Sigma] |
|
Cil2cfg |
Build a CFG of a function keeping some information of the initial structure.
|
Cint |
|
Cint [Wp] |
|
Clabels |
|
Clabels [Wp] |
|
Clean [Wp_parameters] |
|
Clean [Wp.Wp_parameters] |
|
Cleaning |
|
Cmath |
|
CodeSemantics |
|
CodeSemantics [Wp] |
|
Computer [CfgWP] |
|
Conditions |
|
Conditions [Wp] |
|
Context |
|
Context [Wp] |
|
Contrapose [TacChoice] |
|
CoqCompiler [Wp_parameters] |
|
CoqCompiler [Wp.Wp_parameters] |
|
CoqIde [Wp_parameters] |
|
CoqIde [Wp.Wp_parameters] |
|
CoqLibs [Wp_parameters] |
|
CoqLibs [Wp.Wp_parameters] |
|
CoqProject [Wp_parameters] |
|
CoqProject [Wp.Wp_parameters] |
|
CoqTactic [Wp_parameters] |
|
CoqTactic [Wp.Wp_parameters] |
|
CoqTimeout [Wp_parameters] |
|
CoqTimeout [Wp.Wp_parameters] |
|
Core [Wp_parameters] |
|
Core [Wp.Wp_parameters] |
|
Cstring |
|
Cstring [Wp] |
|
Ctypes |
|
Ctypes [Wp] |
|
Cvalues |
|
D |
DISK [Wpo] |
|
DISK [Wp.Wpo] |
|
Definitions |
|
Definitions [Wp] |
|
Defs [Letify] |
|
Depth [Wp_parameters] |
|
Depth [Wp.Wp_parameters] |
|
Detect [Wp_parameters] |
|
Detect [Wp.Wp_parameters] |
|
Driver |
|
Driver [Wp] |
|
Drivers [Wp_parameters] |
|
Drivers [Wp.Wp_parameters] |
|
DynCall [Wp_parameters] |
|
DynCall [Wp.Wp_parameters] |
|
Dyncall |
|
E |
E [CfgCompiler.Cfg] |
Relocatable effect (a predicate that depend on two states).
|
E [Model.Registry] |
|
E [Wp.CfgCompiler.Cfg] |
Relocatable effect (a predicate that depend on two states).
|
E [Wp.Model.Registry] |
|
Env [Plang] |
|
Env [Wp.Plang] |
|
Eset [Cil2cfg] |
|
ExtEqual [Wp_parameters] |
|
ExtEqual [Wp.Wp_parameters] |
|
ExternArrays [Wp_parameters] |
|
ExternArrays [Wp.Wp_parameters] |
|
F |
F [Lang] |
|
F [Wp.Lang] |
|
Factory |
|
Factory [Wp] |
|
Field [Lang] |
|
Field [Wp.Lang] |
|
Filter [Wp_parameters] |
|
Filter [Wp.Wp_parameters] |
|
Filtering |
|
Filtering [Wp] |
|
Fmap [Register] |
|
Fmap [Tactical] |
|
Fmap [Wp.Tactical] |
|
Footprint |
|
Fun [Lang] |
|
Fun [Wp.Lang] |
|
G |
GOAL [Wpo] |
|
GOAL [Wp.Wpo] |
|
GOALS [Register] |
|
Generate [Wp_parameters] |
|
Generate [Wp.Wp_parameters] |
|
Generator |
|
Generator [Model] |
projectified, depend on the model, not serialized
|
Generator [Wp.Model] |
projectified, depend on the model, not serialized
|
Gmap [Wpo] |
|
Gmap [Wp.Wpo] |
|
Goal [ProverWhy3] |
|
Ground [Letify] |
|
Ground [Wp_parameters] |
|
Ground [Wp.Wp_parameters] |
|
GuiComposer |
|
GuiConfig |
|
GuiGoal |
|
GuiList |
|
GuiNavigator |
|
GuiPanel |
|
GuiProof |
|
GuiProver |
|
GuiSequent |
|
GuiSource |
|
GuiTactic |
|
H |
HE [Cil2cfg] |
|
Hashtbl [CfgCompiler.Cfg.Node] |
|
Hashtbl [Wp.CfgCompiler.Cfg.Node] |
|
Hashtbl [Datatype.S_with_collections] |
|
Havoc [TacHavoc] |
|
Heap [Sigs.Model] |
|
Heap [Wp.Sigs.Model] |
|
Hints [Wp_parameters] |
|
Hints [Wp.Wp_parameters] |
|
I |
InCtxt [Wp_parameters] |
|
InCtxt [Wp.Wp_parameters] |
|
InHeap [Wp_parameters] |
|
InHeap [Wp.Wp_parameters] |
|
Index [Wpo] |
|
Index [Model] |
projectified, depend on the model, not serialized
|
Index [Wp.Wpo] |
|
Index [Wp.Model] |
projectified, depend on the model, not serialized
|
Indexed [Wprop] |
|
Indexed2 [Wprop] |
|
Init [Wp_parameters] |
|
Init [Wp.Wp_parameters] |
|
InitAlias [Wp_parameters] |
|
InitAlias [Wp.Wp_parameters] |
|
InitWithForall [Wp_parameters] |
|
InitWithForall [Wp.Wp_parameters] |
|
K |
Key [Datatype.Hashtbl] |
Datatype for the keys of the hashtbl.
|
Key [Datatype.Map] |
Datatype for the keys of the map.
|
L |
L [Sigs.Compiler] |
|
L [Sigs.LogicAssigns] |
|
L [Wp.Sigs.Compiler] |
|
L [Wp.Sigs.LogicAssigns] |
|
LabelMap [Clabels] |
|
LabelMap [Wp.Clabels] |
|
LabelSet [Clabels] |
|
LabelSet [Wp.Clabels] |
|
Lang |
|
Lang [Wp] |
|
Let [Wp_parameters] |
|
Let [Wp.Wp_parameters] |
|
Letify |
|
Literals [Wp_parameters] |
|
Literals [Wp.Wp_parameters] |
|
Logic [Cvalues] |
|
LogicAssigns |
|
LogicBuiltins |
|
LogicBuiltins [Wp] |
|
LogicCompiler |
|
LogicCompiler [Wp] |
|
LogicSemantics |
|
LogicSemantics [Wp] |
|
LogicUsage |
|
LogicUsage [Wp] |
|
M |
M [Sigs.Compiler] |
|
M [Sigs.LogicAssigns] |
|
M [Sigs.LogicSemantics] |
|
M [Sigs.CodeSemantics] |
The underlying memory model
|
M [Wp.Sigs.Compiler] |
|
M [Wp.Sigs.LogicAssigns] |
|
M [Wp.Sigs.LogicSemantics] |
|
M [Wp.Sigs.CodeSemantics] |
The underlying memory model
|
MACHINE [Matrix] |
|
Make [StmtSemantics] |
|
Make [MemVar] |
|
Make [Sigma] |
|
Make [LogicAssigns] |
|
Make [LogicSemantics] |
|
Make [LogicCompiler] |
|
Make [CodeSemantics] |
|
Make [Wp.StmtSemantics] |
|
Make [Wp.MemVar] |
|
Make [Wp.Sigma] |
|
Make [Wp.LogicSemantics] |
|
Make [Wp.LogicCompiler] |
|
Make [Wp.CodeSemantics] |
|
Make [Datatype.Hashtbl] |
Build a datatype of the hashtbl according to the datatype of values in the
hashtbl.
|
Make [Datatype.Map] |
Build a datatype of the map according to the datatype of values in the
map.
|
Map [CfgCompiler.Cfg.Node] |
|
Map [Warning] |
|
Map [Wp.CfgCompiler.Cfg.Node] |
|
Map [Datatype.S_with_collections] |
|
Map [Wp.Warning] |
|
Matrix |
|
Mcfg |
|
Mcfg [Wp] |
|
MemEmpty |
|
MemTyped |
|
MemTyped [Wp] |
|
MemVar |
|
MemVar [Wp] |
|
MemZeroAlias |
|
MemoryContext |
|
MemoryContext [Wp_parameters] |
|
MemoryContext [Wp] |
|
MemoryContext [Wp.Wp_parameters] |
|
Model |
|
Model [Wp_parameters] |
|
Model [Wp] |
|
Model [Wp.Wp_parameters] |
|
Models [Register] |
|
Mstate |
|
Mstate [Wp] |
|
N |
N [Lang] |
|
N [Wp.Lang] |
|
NATURAL [Matrix] |
|
Node [CfgCompiler.Cfg] |
Program point along a trace.
|
Node [Wp.CfgCompiler.Cfg] |
Program point along a trace.
|
NormAtLabels |
|
NormAtLabels [Wp] |
|
P |
P [CfgCompiler.Cfg] |
|
P [Wp.CfgCompiler.Cfg] |
|
PM [Register] |
|
Parasite [Wp_parameters] |
|
Parasite [Wp.Wp_parameters] |
|
Passive |
|
Passive [Wp] |
|
Pcfg |
|
Pcfg [Wp] |
|
Pcond |
|
Pcond [Wp] |
|
Plang |
|
Plang [Wp] |
|
Pmap [VCS] |
|
Pmap [Lang.F] |
|
Pmap [Wp.VCS] |
|
Pmap [Wp.Lang.F] |
|
PrecondWeakening [Wp_parameters] |
|
PrecondWeakening [Wp.Wp_parameters] |
|
Prenex [Wp_parameters] |
|
Prenex [Wp.Wp_parameters] |
|
Print [Wp_parameters] |
|
Print [Wp.Wp_parameters] |
|
Procs [Wp_parameters] |
|
Procs [Wp.Wp_parameters] |
|
Proof |
|
ProofEngine |
|
ProofScript |
|
ProofSession |
|
ProofTrace [Wp_parameters] |
|
ProofTrace [Wp.Wp_parameters] |
|
PropId [WpPropId] |
|
PropId [Wp.WpPropId] |
|
Properties [Wp_parameters] |
|
Properties [Wp.Wp_parameters] |
|
Prover |
|
Prover [Wp] |
|
ProverCoq |
|
ProverDetect |
|
ProverErgo |
|
ProverScript |
|
ProverSearch |
|
ProverTask |
|
ProverTask [Wp] |
|
ProverWhy3 |
|
ProverWhy3ide |
|
Provers [Wp_parameters] |
|
Provers [Wp.Wp_parameters] |
|
Prune [Wp_parameters] |
|
Prune [Wp.Wp_parameters] |
|
Pset [VCS] |
|
Pset [Lang.F] |
|
Pset [Wp.VCS] |
|
Pset [Wp.Lang.F] |
|
Q |
QED [Lang.F] |
|
QED [Wp.Lang.F] |
|
QedChecks [Wp_parameters] |
|
QedChecks [Wp.Wp_parameters] |
|
R |
RTE [Wp_parameters] |
|
RTE [Wp.Wp_parameters] |
|
Range [Auto] |
|
Range [Wp.Auto] |
|
Reduce [Wp_parameters] |
|
Reduce [Wp.Wp_parameters] |
|
RefUsage |
|
RefUsage [Wp] |
|
Region |
|
Register |
|
Report [Wp_parameters] |
|
Report [Wp.Wp_parameters] |
|
ReportJson [Wp_parameters] |
|
ReportJson [Wp.Wp_parameters] |
|
ReportName [Wp_parameters] |
|
ReportName [Wp.Wp_parameters] |
|
Repr |
Term & Predicate Introspection
|
Repr [Wp] |
|
Rformat |
|
S |
S [Wpo] |
|
S [CfgCompiler.Cfg] |
|
S [Model] |
|
S [Wp.Wpo] |
|
S [Wp.CfgCompiler.Cfg] |
|
S [Wp.Model] |
|
Script |
|
Script [Wp_parameters] |
|
Script [Wp.Wp_parameters] |
|
Separated [TacHavoc] |
|
Set [CfgCompiler.Cfg.Node] |
|
Set [Warning] |
|
Set [Wp.CfgCompiler.Cfg.Node] |
|
Set [Datatype.S_with_collections] |
|
Set [Wp.Warning] |
|
Sigma |
|
Sigma [Sigs.Model] |
|
Sigma [Letify] |
|
Sigma [Wp] |
|
Sigma [Wp.Sigs.Model] |
|
Sigs |
Common Types and Signatures
|
Sigs [Wp] |
|
Simpl [Wp_parameters] |
|
Simpl [Wp.Wp_parameters] |
|
SimplifyForall [Wp_parameters] |
|
SimplifyForall [Wp.Wp_parameters] |
|
SimplifyIsCint [Wp_parameters] |
|
SimplifyIsCint [Wp.Wp_parameters] |
|
SimplifyLandMask [Wp_parameters] |
|
SimplifyLandMask [Wp.Wp_parameters] |
|
SimplifyType [Wp_parameters] |
|
SimplifyType [Wp.Wp_parameters] |
|
Split [Letify] |
Pruning strategy ; selects most occurring literals to split cases.
|
Split [Wp_parameters] |
|
Split [Wp.Wp_parameters] |
|
SplitDepth [Wp_parameters] |
|
SplitDepth [Wp.Wp_parameters] |
|
Splitter |
|
Splitter [Wp] |
|
Static [Model] |
projectified, independent from the model, not serialized
|
Static [Wp.Model] |
projectified, independent from the model, not serialized
|
StaticGenerator [Model] |
projectified, independent from the model, not serialized
|
StaticGenerator [Wp.Model] |
projectified, independent from the model, not serialized
|
StatusAll [Wp_parameters] |
|
StatusAll [Wp.Wp_parameters] |
|
StatusFalse [Wp_parameters] |
|
StatusFalse [Wp.Wp_parameters] |
|
StatusMaybe [Wp_parameters] |
|
StatusMaybe [Wp.Wp_parameters] |
|
StatusTrue [Wp_parameters] |
|
StatusTrue [Wp.Wp_parameters] |
|
Steps [Wp_parameters] |
|
Steps [Wp.Wp_parameters] |
|
StmtSemantics |
|
StmtSemantics [Wp] |
|
Strategy |
Term & Predicate Selection
|
Strategy [Wp] |
|
Subst [Lang] |
|
Subst [Wp.Lang] |
|
T |
T [CfgCompiler.Cfg] |
|
T [Clabels] |
|
T [Wp.CfgCompiler.Cfg] |
|
T [Wp.Clabels] |
|
TacArray |
Built-in Array Tactical (auto-registered)
|
TacBitrange |
Built-in Bit Range Tactical (auto-registered)
|
TacBitwised |
Built-in Bitwised-Eq Tactical (auto-registered)
|
TacChoice |
Built-in Choice, Absurd & Contrapose Tactical (auto-registered)
|
TacCompound |
Built-in Compound Tactical (auto-registered)
|
TacCongruence |
Built-in Tactical for Product & Division Comparison (auto-registered)
|
TacCut |
Built-in Cut Tactical (auto-registered)
|
TacFilter |
Built-in Filtering Tactic (auto-registered)
|
TacHavoc |
Built-in Havoc Tactical (auto-registered)
|
TacInstance |
Built-in Instance Tactical (auto-registered)
|
TacLemma |
Self registered 'Lemma' Tactical
|
TacNormalForm |
Built-in Normal Form Tactical (auto-registered)
|
TacOverflow |
Auto registered overflow tactic
|
TacRange |
Built-in Range Tactical (auto-registered)
|
TacRewrite |
Built-in Range Tactical (auto-registered)
|
TacShift |
Built-in Shift Tactical (auto-registered)
|
TacSplit |
Built-in Split Tactical (auto-registered)
|
TacUnfold |
Built-in Unfold Tactical (auto-registered)
|
Tactical |
|
Tactical [Wp] |
|
Tau [Lang.F] |
|
Tau [Wp.Lang.F] |
|
TimeExtra [Wp_parameters] |
|
TimeExtra [Wp.Wp_parameters] |
|
TimeMargin [Wp_parameters] |
|
TimeMargin [Wp.Wp_parameters] |
|
Timeout [Wp_parameters] |
|
Timeout [Wp.Wp_parameters] |
|
Tmap [Lang.F] |
|
Tmap [Wp.Lang.F] |
|
Trigger [Definitions] |
|
Trigger [Wp.Definitions] |
|
TruncPropIdFileName [Wp_parameters] |
|
TruncPropIdFileName [Wp.Wp_parameters] |
|
TryHints [Wp_parameters] |
|
TryHints [Wp.Wp_parameters] |
|
Tset [Lang.F] |
|
Tset [Wp.Lang.F] |
|
U |
UnfoldAssigns [Wp_parameters] |
|
UnfoldAssigns [Wp.Wp_parameters] |
|
UpdateScript [Wp_parameters] |
|
UpdateScript [Wp.Wp_parameters] |
|
V |
VC |
|
VC [CfgWP] |
|
VC [Wp] |
|
VCS |
Verification Condition Status
|
VCS [Wp] |
|
VC_Annot [Wpo] |
|
VC_Annot [Wp.Wpo] |
|
VC_Check [Wpo] |
|
VC_Check [Wp.Wpo] |
|
VC_Lemma [Wpo] |
|
VC_Lemma [Wp.Wpo] |
|
Validity [TacHavoc] |
|
Var [Lang.F] |
|
Var [Wp.Lang.F] |
|
Vars [Lang.F] |
|
Vars [Wp.Lang.F] |
|
Vlist |
|
Vmap [Lang.F] |
|
Vmap [Wp.Lang.F] |
|
Volatile [Wp_parameters] |
|
Volatile [Wp.Wp_parameters] |
|
Vset |
|
Vset [Wp] |
|
W |
WP [Wp_parameters] |
|
WP [Wp.Wp_parameters] |
|
Warning |
|
Warning [Wp] |
|
Why3 [Wp_parameters] |
|
Why3 [Wp.Wp_parameters] |
|
Why3_xml |
|
WhyFlags [Wp_parameters] |
|
WhyFlags [Wp.Wp_parameters] |
|
WhyLibs [Wp_parameters] |
|
WhyLibs [Wp.Wp_parameters] |
|
Wp |
|
WpAnnot |
Every access to annotations have to go through here,
so this is the place where we decide what the computation
is allowed to use.
|
WpPropId |
|
WpPropId [Wp] |
|
WpRTE |
Invoke RTE to generate missing annotations
for the given function and model.
|
WpReport |
|
WpStrategy |
|
WpTac |
|
Wp_error |
|
Wp_parameters |
|
Wp_parameters [Wp] |
|
Wpo |
|
Wpo [Wp] |
|
Wprop |
|