Index of modules


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 [Lang.F]
Check [Wp_parameters]
Check [Wp.Lang.F]
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
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]

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]
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]
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 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