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
|