Index of modules


A
ADT [Lang]
ADT [Wp.Lang]
Absurd [TacChoice]
AinfoComparable [Ctypes]
AinfoComparable [Wp.Ctypes]
Alpha [Lang]
Alpha [Wp.Lang]
AltErgo [Wp_parameters]
AltErgoFlags [Wp_parameters]
AltErgoLibs [Wp_parameters]
AltGrErgo [Wp_parameters]
Auto
Registered Strategies It is always safe to apply strategies to any goal.
Auto [Wp]

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
Floating Arithmetic Model
Cfloat [Wp]
Check [Lang.F]
Check [Wp_parameters]
Check [Wp.Lang.F]
Choice [TacChoice]
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]
Contrapose [TacChoice]
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-Booleans

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]
Filtering
Sequent Cleaning
Fmap [Register]
Fmap [Tactical]
Fmap [Wp.Tactical]
Footprint
Term Footprints
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]
Ground [Letify]
Ground [Wp_parameters]
GuiComposer
request-for-update event
GuiConfig
Edit enabled provers
GuiGoal
GuiList
GuiNavigator
GuiPanel
GuiProof
GuiProver
Requires filter prover.
GuiSequent
GuiSource
GuiTactic

H
HE [Cil2cfg]
Hashtbl [Datatype.S_with_collections]
Havoc [TacHavoc]
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]
InitAlias [Wp_parameters]
InitWithForall [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.Sigma]
Make [Wp.LogicSemantics]
Make [Wp.LogicCompiler]
Make [Wp.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 [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]
Mstate
Mstate [Wp]

N
N [Lang]
N [Wp.Lang]
NATURAL [Matrix]
NormAtLabels
push the Tat down to the 'data' operations.
NormAtLabels [Wp]

P
PM [Register]
Passive
Passive Forms
Passive [Wp]
Pcfg
current state
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
ProofEngine
Interactive Proof Engine
ProofScript
With number of pending goals
ProofSession
ProofTrace [Wp_parameters]
PropId [WpPropId]
PropId [Wp.WpPropId]
Properties [Wp_parameters]
Prover
ProverCoq
ProverErgo
ProverScript
Play provers with valid result (default: true)
ProverSearch
ProverTask
never fails
ProverWhy3
None if the po is trivial
ProverWhy3ide
Provers [Wp_parameters]
Prune [Wp_parameters]
Pset [VCS]
Pset [Lang.F]
Pset [Wp.VCS]
Pset [Wp.Lang.F]

Q
QED [Lang.F]
QED [Wp.Lang.F]
QedChecks [Wp_parameters]

R
RTE [Wp_parameters]
Range [Auto]
Range [Wp.Auto]
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]
Repr
Term & Predicate Introspection
Repr [Wp]
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]
Separated [TacHavoc]
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 occurring literals to split cases.
Split [Wp_parameters]
SplitDepth [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]
Strategy
Term & Predicate Selection
Strategy [Wp]
Subst [Lang]
Subst [Wp.Lang]

T
T [Clabels]
T [Wp.Clabels]
TacArray
Built-in Array Tactical (auto-registered)
TacChoice
Built-in Choice, Absurd & Contrapose Tactical (auto-registered)
TacCompound
Built-in Compound Tactical (auto-registered)
TacCut
Built-in Cut Tactical (auto-registered)
TacFilter
Built-in Filtering Tactic (auto-registered)
TacHavoc
Built-in Havoc Tactical (auto-registered)
TacInstance
Built-in Instance Tactical (auto-registered)
TacLemma
Self registered 'Lemma' Tactical
TacNormalForm
Built-in Normal Form Tactical (auto-registered)
TacRange
Built-in Range Tactical (auto-registered)
TacRewrite
Built-in Range Tactical (auto-registered)
TacSplit
Built-in Split Tactical (auto-registered)
TacUnfold
Built-in Unfold Tactical (auto-registered)
Tactical
Tactical
Tactical [Wp]
Tau [Lang.F]
Tau [Wp.Lang.F]
Timeout [Wp_parameters]
Tmap [Lang.F]
Tmap [Wp.Lang.F]
Trigger [Definitions]
Trigger [Wp.Definitions]
TruncPropIdFileName [Wp_parameters]
TryHints [Wp_parameters]
Tset [Lang.F]
Tset [Wp.Lang.F]

U
UpdateScript [Wp_parameters]

V
VC
Proof Obligations
VC [CfgWP]
VC [Wp]
VCS
Verification Condition Status
VCS [Wp]
VC_Annot [Wpo]
VC_Check [Wpo]
VC_Lemma [Wpo]
Var [Lang.F]
Var [Wp.Lang.F]
Vars [Lang.F]
Vars [Wp.Lang.F]
Vlist
VList Theory Builtins
Vmap [Lang.F]
Vmap [Wp.Lang.F]
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 strategy that can then be used by the main generic calculus.
WpTac
Term manipulation for Tacticals
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

Z
Z [Lang.F]
Z [Wp.Lang.F]