A |
ADT [Lang] |
|
ADT [Wp.Lang] |
|
AinfoComparable [Ctypes] |
|
AinfoComparable [Wp.Ctypes] |
|
Alpha [Lang] |
|
Alpha [Wp.Lang] |
|
AltErgo [Wp_parameters] |
|
AltErgoFlags [Wp_parameters] |
|
AltErgoLibs [Wp_parameters] |
|
AltGrErgo [Wp_parameters] |
|
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 |
Floatting Arithmetic Model
|
Cfloat [Wp] |
|
Check [Wp_parameters] |
|
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] |
|
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-Boolans
|
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] |
|
Fmap [Register] |
|
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] |
|
GuiConfig |
Edit enabled provers
|
GuiGoal |
|
GuiList |
|
GuiNavigator |
|
GuiPanel |
|
GuiSource |
|
H |
HE [Cil2cfg] |
|
Hashtbl [Datatype.S_with_collections] |
|
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] |
|
InitWithForall [Wp_parameters] |
|
Invariants [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.LogicSemantics] |
|
Make [Wp.LogicCompiler] |
|
Make [Wp.CodeSemantics] |
|
Make [Wp.Sigma] |
|
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 |
|
MemTyped [Wp] |
|
MemVar |
|
MemVar [Wp] |
|
MemZeroAlias |
|
Memory |
Memory Values
|
Memory [Wp] |
|
Model |
Model Registration
|
Model [Wp_parameters] |
|
Model [Wp] |
|
Models [Register] |
|
N |
NATURAL [Matrix] |
|
NormAtLabels |
push the Tat down to the 'data' operations.
|
NormAtLabels [Wp] |
|
P |
PM [Register] |
|
Passive |
Passive Forms
|
Passive [Wp] |
|
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
|
ProofTrace [Wp_parameters] |
|
PropId [WpPropId] |
|
PropId [Wp.WpPropId] |
|
Properties [Wp_parameters] |
|
Prover |
|
ProverCoq |
|
ProverErgo |
|
ProverTask |
never fails
|
ProverWhy3 |
None if the po is trivial
|
ProverWhy3ide |
|
Provers [Wp_parameters] |
|
Prune [Wp_parameters] |
|
Pset [Lang.F] |
|
Pset [Wp.Lang.F] |
|
Q |
QedChecks [Wp_parameters] |
|
R |
RTE [Wp_parameters] |
|
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] |
|
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] |
|
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 occuring literals to split cases.
|
Split [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] |
|
T |
T [Clabels] |
|
T [Wp.Clabels] |
|
Timeout [Wp_parameters] |
|
Trigger [Definitions] |
|
Trigger [Wp.Definitions] |
|
TruncPropIdFileName [Wp_parameters] |
|
TryHints [Wp_parameters] |
|
U |
UpdateScript [Wp_parameters] |
|
V |
VC |
Proof Obligations
|
VC [CfgWP] |
|
VC [Wp] |
|
VCS |
Verification Conditions Database
|
VCS [Wp] |
|
VC_Annot [Wpo] |
|
VC_Check [Wpo] |
|
VC_Lemma [Wpo] |
|
VarUsage |
Usage Variable Analysis
|
VarUsageRef |
Usage Variable Analysis
|
Variables_analysis |
This analysis performs a classification of the variables of the input
program.
|
Vlist |
VList Theory Builtins
|
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] |
|
WpReport |
Export Statistics.
|
WpStrategy |
This file provide all the functions to build a stategy that can then
be used by the main generic calculus.
|
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
|