A | |
ADT [Lang] | |
AinfoComparable [Ctypes] | |
Alpha [Lang] | |
AltErgoFlags [Wp_parameters] | |
AltErgoLibs [Wp_parameters] | |
B | |
Behaviors [Wp_parameters] | |
Bits [Wp_parameters] | |
BoundForallUnfolding [Wp_parameters] | |
ByRef [Wp_parameters] | |
ByValue [Wp_parameters] | |
C | |
C_object [Ctypes] | |
Calculus |
Generic WP calculus
|
CalleePreCond [Wp_parameters] | |
Cfg [Calculus] | |
CfgDump | |
CfgWP | |
Cfloat |
Floatting Arithmetic Model
|
Check [Wp_parameters] | |
Chunk [Memory.Model] | |
Cil2cfg |
abstract type of a cfg
|
Cint |
Integer Arithmetic Model
|
Clabels |
Normalized C-labels
|
Clean [Wp_parameters] | |
Cleaning | |
CodeSemantics |
None means equal to zero/null
|
Computer [CfgWP] | |
Conditions |
Bundles
|
Context |
Current Loc
|
CoqLibs [Wp_parameters] | |
CoqTactic [Wp_parameters] | |
CoqTimeout [Wp_parameters] | |
Core [Wp_parameters] | |
Cstring |
String Literal
|
Ctypes |
C-Types
|
Cvalues |
Int-As-Boolans
|
D | |
DISK [Wpo] | |
Definitions |
Unique
|
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] | |
Eset [Cil2cfg] |
set of edges
|
ExtEqual [Wp_parameters] | |
ExternArrays [Wp_parameters] | |
F | |
F [Lang] | |
Factory | |
Field [Lang] | |
Filter [Wp_parameters] | |
Fun [Lang] | |
G | |
GOAL [Wpo] | |
GOALS [Register] | |
Generate [Wp_parameters] | |
Generator | |
Generator [Model] |
projectified, depend on the model, not serialized
|
Gmap [Wpo] | |
GuiConfig |
Edit enabled provers
|
GuiGoal | |
GuiList | |
GuiNavigator | |
GuiPanel | |
GuiSource | |
H | |
HE [Cil2cfg] | |
Hashtbl [Datatype.S_with_collections] | |
Heap [Memory.Model] | |
Hints [Wp_parameters] | |
I | |
InCtxt [Wp_parameters] | |
InHeap [Wp_parameters] | |
Index [Wpo] | |
Index [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] | |
LabelSet [Clabels] | |
Lang |
Logic Language based on Qed
|
Let [Wp_parameters] | |
Letify | bind sigma defs xs select definitions in defs
targeting variables xs .
|
Literals [Wp_parameters] | |
Logic [Cvalues] | |
LogicAssigns | |
LogicBuiltins |
integer
|
LogicCompiler |
Definitions
|
LogicSemantics |
Debug
|
LogicUsage |
Trims the original name
|
M | |
MACHINE [Matrix] | |
Make [MemVar] | |
Make [Sigma] | |
Make [LogicAssigns] | |
Make [LogicSemantics] | |
Make [LogicCompiler] | |
Make [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 [Datatype.S_with_collections] | |
Map [Warning] | |
Matrix |
unique w.r.t
equal
|
Mcfg |
This is what is really needed to propagate something through the CFG.
|
MemEmpty | |
MemTyped | |
MemVar | |
Memory |
Memory Values
|
Model |
Model Registration
|
Model [Wp_parameters] | |
N | |
NATURAL [Matrix] | |
NormAtLabels |
push the Tat down to the 'data' operations.
|
P | |
PM [Register] | |
Passive |
Passive Forms
|
Pmap [VCS] | |
Pmap [Lang.F] | |
Print [Wp_parameters] | |
Procs [Wp_parameters] | |
Proof |
Proof Script Database
|
ProofTrace [Wp_parameters] | |
PropId [WpPropId] | |
Properties [Wp_parameters] | |
Prover |
Different instance of why3ide can't be run simultanely
|
ProverCoq | |
ProverErgo | |
ProverTask |
never fails
|
ProverWhy3 |
None if the po is trivial
|
Provers [Wp_parameters] | |
Prune [Wp_parameters] | |
Pset [Lang.F] | |
Q | |
QedChecks [Wp_parameters] | |
R | |
RTE [Wp_parameters] | |
RefUsage |
Variable accesses from C code and code annotations
|
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] | |
Script | |
Script [Wp_parameters] | |
Set [Datatype.S_with_collections] | |
Set [Warning] | |
Sigma [Memory.Model] | |
Sigma | |
Sigma [Letify] | |
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 | |
Static [Model] |
projectified, independent from the model, not serialized
|
StaticGenerator [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] | |
Timeout [Wp_parameters] | |
Trigger [Definitions] | |
TruncPropIdFileName [Wp_parameters] | |
TryHints [Wp_parameters] | |
U | |
UpdateScript [Wp_parameters] | |
V | |
VC [CfgWP] | |
VCS |
Verification Conditions Database
|
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.
|
Vset |
Logical Sets
|
W | |
WP [Wp_parameters] | |
Warning |
Contextual Errors
|
Why3_session |
From the original file we kept only the reading of a session.
|
Why3_xml |
returns the list of XML elements from the given file.
|
WhyFlags [Wp_parameters] | |
WhyLibs [Wp_parameters] | |
Wp |
Weakest preconditions.
|
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.
|
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
|