Index of modules


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