A | |
ADT [Lang] | |
ADT [Wp.Lang] | |
Absurd [TacChoice] | |
AinfoComparable [Ctypes] | |
AinfoComparable [Wp.Ctypes] | |
Alpha [Lang] | |
Alpha [Wp.Lang] | |
AltErgo [Wp_parameters] | |
AltErgoFlags [Wp_parameters] | |
AltErgoLibs [Wp_parameters] | |
AltGrErgo [Wp_parameters] | |
Auto |
Registered Strategies
It is always safe to apply strategies to any goal.
|
Auto [Wp] | |
B | |
Behaviors [Wp_parameters] | |
Bits [Wp_parameters] | |
BoundForallUnfolding [Wp_parameters] | |
ByRef [Wp_parameters] | |
ByValue [Wp_parameters] | |
C | |
C_object [Ctypes] | |
C_object [Wp.Ctypes] | |
Calculus |
Generic WP calculus
|
CalleePreCond [Wp_parameters] | |
Cfg [Calculus] | |
CfgDump | |
CfgWP | |
Cfloat |
Floating Arithmetic Model
|
Cfloat [Wp] | |
Check [Lang.F] | |
Check [Wp_parameters] | |
Check [Wp.Lang.F] | |
Choice [TacChoice] | |
Chunk [Memory.Model] | |
Chunk [Wp.Memory.Model] | |
Cil2cfg |
abstract type of a cfg
|
Cint |
Integer Arithmetic Model
|
Cint [Wp] | |
Clabels |
Normalized C-labels
|
Clabels [Wp] | |
Clean [Wp_parameters] | |
Cleaning | |
CodeSemantics |
None means equal to zero/null
|
CodeSemantics [Wp] | |
Computer [CfgWP] | |
Conditions |
Sequent
|
Conditions [Wp] | |
Context |
Current Loc
|
Context [Wp] | |
Contrapose [TacChoice] | |
CoqCompiler [Wp_parameters] | |
CoqIde [Wp_parameters] | |
CoqLibs [Wp_parameters] | |
CoqProject [Wp_parameters] | |
CoqTactic [Wp_parameters] | |
CoqTimeout [Wp_parameters] | |
Core [Wp_parameters] | |
Cstring |
String Literal
|
Cstring [Wp] | |
Ctypes |
C-Types
|
Ctypes [Wp] | |
Cvalues |
Int-As-Booleans
|
D | |
DISK [Wpo] | |
Definitions |
Unique
|
Definitions [Wp] | |
Defs [Letify] | |
Depth [Wp_parameters] | |
Detect [Wp_parameters] | |
Driver |
Memoized loading of drivers according to current
WP options.
|
Drivers [Wp_parameters] | |
DynCall [Wp_parameters] | |
Dyncall |
Returns an property identifier for the precondition.
|
E | |
E [Model.Registry] | |
E [Wp.Model.Registry] | |
Env [Plang] | |
Eset [Cil2cfg] |
set of edges
|
ExtEqual [Wp_parameters] | |
ExternArrays [Wp_parameters] | |
F | |
F [Lang] | |
F [Wp.Lang] | |
Factory | "Var,Typed,Nat,Real" memory model.
|
Factory [Wp] | |
Field [Lang] | |
Field [Wp.Lang] | |
Filter [Wp_parameters] | |
Filtering |
Sequent Cleaning
|
Fmap [Register] | |
Fmap [Tactical] | |
Fmap [Wp.Tactical] | |
Footprint |
Term Footprints
|
Fun [Lang] | |
Fun [Wp.Lang] | |
G | |
GOAL [Wpo] | |
GOALS [Register] | |
Generate [Wp_parameters] | |
Generator | |
Generator [Model] |
projectified, depend on the model, not serialized
|
Generator [Wp.Model] |
projectified, depend on the model, not serialized
|
Gmap [Wpo] | |
Goal [ProverWhy3] | |
Ground [Letify] | |
Ground [Wp_parameters] | |
GuiComposer |
request-for-update event
|
GuiConfig |
Edit enabled provers
|
GuiGoal | |
GuiList | |
GuiNavigator | |
GuiPanel | |
GuiProof | |
GuiProver |
Requires
filter prover .
|
GuiSequent | |
GuiSource | |
GuiTactic | |
H | |
HE [Cil2cfg] | |
Hashtbl [Datatype.S_with_collections] | |
Havoc [TacHavoc] | |
Heap [Memory.Model] | |
Heap [Wp.Memory.Model] | |
Hints [Wp_parameters] | |
I | |
InCtxt [Wp_parameters] | |
InHeap [Wp_parameters] | |
Index [Wpo] | |
Index [Model] |
projectified, depend on the model, not serialized
|
Index [Wp.Model] |
projectified, depend on the model, not serialized
|
Indexed [Wprop] | |
Indexed2 [Wprop] | |
Init [Wp_parameters] | |
InitAlias [Wp_parameters] | |
InitWithForall [Wp_parameters] | |
K | |
Key [Datatype.Hashtbl] |
Datatype for the keys of the hashtbl.
|
Key [Datatype.Map] |
Datatype for the keys of the map.
|
L | |
LabelMap [Clabels] | |
LabelMap [Wp.Clabels] | |
LabelSet [Clabels] | |
LabelSet [Wp.Clabels] | |
Lang |
Logic Language based on Qed
|
Lang [Wp] | |
Let [Wp_parameters] | |
Letify | bind sigma defs xs select definitions in defs
targeting variables xs .
|
Literals [Wp_parameters] | |
Logic [Cvalues] | |
LogicAssigns | |
LogicBuiltins |
integer
|
LogicBuiltins [Wp] | |
LogicCompiler |
Definitions
|
LogicCompiler [Wp] | |
LogicSemantics |
Debug
|
LogicSemantics [Wp] | |
LogicUsage |
Trims the original name
|
LogicUsage [Wp] | |
M | |
MACHINE [Matrix] | |
Make [MemVar] | |
Make [Sigma] | |
Make [LogicAssigns] | |
Make [LogicSemantics] | |
Make [LogicCompiler] | |
Make [CodeSemantics] | |
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 [Warning] | |
Map [Datatype.S_with_collections] | |
Map [Wp.Warning] | |
Matrix |
unique w.r.t
equal
|
Mcfg |
This is what is really needed to propagate something through the CFG.
|
Mcfg [Wp] | |
MemEmpty | |
MemTyped |
describe the content of literal strings
|
MemTyped [Wp] | |
MemVar | |
MemVar [Wp] | |
MemZeroAlias | |
Memory |
Memory Values
|
Memory [Wp] | |
Model |
Model Registration
|
Model [Wp_parameters] | |
Model [Wp] | |
Models [Register] | |
Mstate | |
Mstate [Wp] | |
N | |
N [Lang] | |
N [Wp.Lang] | |
NATURAL [Matrix] | |
NormAtLabels |
push the Tat down to the 'data' operations.
|
NormAtLabels [Wp] | |
P | |
PM [Register] | |
Passive |
Passive Forms
|
Passive [Wp] | |
Pcfg |
current state
|
Pcond |
All-in-one printers
|
Plang |
Lang Pretty-Printer
|
Pmap [VCS] | |
Pmap [Lang.F] | |
Pmap [Wp.VCS] | |
Pmap [Wp.Lang.F] | |
Print [Wp_parameters] | |
Procs [Wp_parameters] | |
Proof |
Proof Script Database
|
ProofEngine |
Interactive Proof Engine
|
ProofScript |
With number of pending goals
|
ProofSession | |
ProofTrace [Wp_parameters] | |
PropId [WpPropId] | |
PropId [Wp.WpPropId] | |
Properties [Wp_parameters] | |
Prover | |
ProverCoq | |
ProverErgo | |
ProverScript |
Play provers with valid result (default: true)
|
ProverSearch | |
ProverTask |
never fails
|
ProverWhy3 |
None if the po is trivial
|
ProverWhy3ide | |
Provers [Wp_parameters] | |
Prune [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] | |
R | |
RTE [Wp_parameters] | |
Range [Auto] | |
Range [Wp.Auto] | |
RefUsage |
Variable accesses from C code and code annotations
|
RefUsage [Wp] | |
Region |
Paths
|
Register |
Do on_server_stop save why3 session
|
Report [Wp_parameters] | |
ReportName [Wp_parameters] | |
Repr |
Term & Predicate Introspection
|
Repr [Wp] | |
Rformat | get_time T t returns k such that T[k-1] <= t <= T[k] ,
T is extended with T[-1]=0 and T[N]=+oo .
|
S | |
S [Wpo] | |
S [Model] | |
S [Wp.Model] | |
Script | |
Script [Wp_parameters] | |
Separated [TacHavoc] | |
Separation |
Elementary regions
|
Separation [Wp_parameters] | |
Separation [Wp] | |
Set [Warning] | |
Set [Datatype.S_with_collections] | |
Set [Wp.Warning] | |
Sigma | |
Sigma [Memory.Model] | |
Sigma [Letify] | |
Sigma [Wp] | |
Sigma [Wp.Memory.Model] | |
Simpl [Wp_parameters] | |
SimplifyForall [Wp_parameters] | |
SimplifyIsCint [Wp_parameters] | |
SimplifyType [Wp_parameters] | |
Split [Letify] |
Pruning strategy ; selects most occurring literals to split cases.
|
Split [Wp_parameters] | |
SplitDepth [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] | |
StatusFalse [Wp_parameters] | |
StatusMaybe [Wp_parameters] | |
StatusTrue [Wp_parameters] | |
Steps [Wp_parameters] | |
Strategy |
Term & Predicate Selection
|
Strategy [Wp] | |
Subst [Lang] | |
Subst [Wp.Lang] | |
T | |
T [Clabels] | |
T [Wp.Clabels] | |
TacArray |
Built-in Array Tactical (auto-registered)
|
TacChoice |
Built-in Choice, Absurd & Contrapose Tactical (auto-registered)
|
TacCompound |
Built-in Compound Tactical (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)
|
TacRange |
Built-in Range Tactical (auto-registered)
|
TacRewrite |
Built-in Range Tactical (auto-registered)
|
TacSplit |
Built-in Split Tactical (auto-registered)
|
TacUnfold |
Built-in Unfold Tactical (auto-registered)
|
Tactical |
Tactical
|
Tactical [Wp] | |
Tau [Lang.F] | |
Tau [Wp.Lang.F] | |
Timeout [Wp_parameters] | |
Tmap [Lang.F] | |
Tmap [Wp.Lang.F] | |
Trigger [Definitions] | |
Trigger [Wp.Definitions] | |
TruncPropIdFileName [Wp_parameters] | |
TryHints [Wp_parameters] | |
Tset [Lang.F] | |
Tset [Wp.Lang.F] | |
U | |
UpdateScript [Wp_parameters] | |
V | |
VC |
Proof Obligations
|
VC [CfgWP] | |
VC [Wp] | |
VCS |
Verification Condition Status
|
VCS [Wp] | |
VC_Annot [Wpo] | |
VC_Check [Wpo] | |
VC_Lemma [Wpo] | |
Var [Lang.F] | |
Var [Wp.Lang.F] | |
Vars [Lang.F] | |
Vars [Wp.Lang.F] | |
Vlist |
VList Theory Builtins
|
Vmap [Lang.F] | |
Vmap [Wp.Lang.F] | |
Vset |
Logical Sets
|
Vset [Wp] | |
W | |
WP [Wp_parameters] | |
Warning |
Contextual Errors
|
Warning [Wp] | |
Why3 [Wp_parameters] | |
Why3_xml |
returns the list of XML elements from the given file.
|
WhyFlags [Wp_parameters] | |
WhyLibs [Wp_parameters] | |
Wp |
C-Types
|
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 |
Beside the property identification, it can be found in different contexts
depending on which part of the computation is involved.
|
WpPropId [Wp] | |
WpRTE |
Returns
true is call pre-conditions have been already
generated by RTE.
|
WpReport |
Export Statistics.
|
WpStrategy |
This file provide all the functions to build a strategy that can then
be used by the main generic calculus.
|
WpTac |
Term manipulation for Tacticals
|
Wp_error |
To be raised a feature of C/ACSL cannot be supported by a memory model
or is not implemented, or ...
|
Wp_parameters |
Goal Selection
|
Wpo |
Proof Obligations
|
Wprop |
Indexed API
|
Z | |
Z [Lang.F] | |
Z [Wp.Lang.F] |