Index of modules

A
A [Sigs.Compiler]
A [Wp.Sigs.Compiler]
ADT [Lang]
ADT [Wp.Lang]
Absurd [TacChoice]
AinfoComparable [Ctypes]
AinfoComparable [Wp.Ctypes]
Alpha [Lang]
Alpha [Wp.Lang]
AltErgo [Wp_parameters]
AltErgo [Wp.Wp_parameters]
AltErgoFlags [Wp_parameters]
AltErgoFlags [Wp.Wp_parameters]
AltErgoLibs [Wp_parameters]
AltErgoLibs [Wp.Wp_parameters]
AltGrErgo [Wp_parameters]
AltGrErgo [Wp.Wp_parameters]
Auto
Auto [Wp_parameters]
Auto [Wp]
Auto [Wp.Wp_parameters]
AutoDepth [Wp_parameters]
AutoDepth [Wp.Wp_parameters]
AutoWidth [Wp_parameters]
AutoWidth [Wp.Wp_parameters]
B
BackTrack [Wp_parameters]
BackTrack [Wp.Wp_parameters]
Behaviors [Wp_parameters]
Behaviors [Wp.Wp_parameters]
Bits [Wp_parameters]
Bits [Wp.Wp_parameters]
BoolRange [Wp_parameters]
BoolRange [Wp.Wp_parameters]
BoundForallUnfolding [Wp_parameters]
BoundForallUnfolding [Wp.Wp_parameters]
ByRef [Wp_parameters]
ByRef [Wp.Wp_parameters]
ByValue [Wp_parameters]
ByValue [Wp.Wp_parameters]
C
C [CfgCompiler.Cfg]

Relocatable condition

C [Sigs.Compiler]
C [Wp.CfgCompiler.Cfg]

Relocatable condition

C [Wp.Sigs.Compiler]
C_object [Ctypes]
C_object [Wp.Ctypes]
Calculus

Generic WP calculus

CalleePreCond [Wp_parameters]
CalleePreCond [Wp.Wp_parameters]
Cfg [Calculus]
Cfg [StmtSemantics.Make]
Cfg [CfgCompiler]
Cfg [Wp.StmtSemantics.Make]
Cfg [Wp.CfgCompiler]
CfgCompiler
CfgCompiler [Wp]
CfgDump
CfgWP
Cfloat

Floating Arithmetic Model

Cfloat [Wp]
Check [Lang.F]
Check [Wp_parameters]
Check [Wp.Lang.F]
Check [Wp.Wp_parameters]
Choice [TacChoice]
Chunk [Sigs.Model]

Memory model chunks.

Chunk [Sigs.Sigma]
Chunk [Wp.Sigs.Model]

Memory model chunks.

Chunk [Wp.Sigs.Sigma]
Cil2cfg

Build a CFG of a function keeping some information of the initial structure.

Cint

Integer Arithmetic Model

Cint [Wp]
Clabels

Normalized C-labels

Clabels [Wp]
Clean [Wp_parameters]
Clean [Wp.Wp_parameters]
Cleaning
Cmath

Math Operators

CodeSemantics
CodeSemantics [Wp]
Computer [CfgWP]
Conditions
Conditions [Wp]
Context

Current Loc

Context [Wp]
Contrapose [TacChoice]
CoqCompiler [Wp_parameters]
CoqCompiler [Wp.Wp_parameters]
CoqIde [Wp_parameters]
CoqIde [Wp.Wp_parameters]
CoqLibs [Wp_parameters]
CoqLibs [Wp.Wp_parameters]
CoqProject [Wp_parameters]
CoqProject [Wp.Wp_parameters]
CoqTactic [Wp_parameters]
CoqTactic [Wp.Wp_parameters]
CoqTimeout [Wp_parameters]
CoqTimeout [Wp.Wp_parameters]
Core [Wp_parameters]
Core [Wp.Wp_parameters]
Cstring
Cstring [Wp]
Ctypes

C-Types

Ctypes [Wp]
Cvalues
D
DISK [Wpo]
DISK [Wp.Wpo]
Definitions
Definitions [Wp]
Defs [Letify]
Depth [Wp_parameters]
Depth [Wp.Wp_parameters]
Detect [Wp_parameters]
Detect [Wp.Wp_parameters]
Driver
Driver [Wp]
Drivers [Wp_parameters]
Drivers [Wp.Wp_parameters]
DynCall [Wp_parameters]
DynCall [Wp.Wp_parameters]
Dyncall
E
E [CfgCompiler.Cfg]

Relocatable effect (a predicate that depend on two states).

E [Model.Registry]
E [Wp.CfgCompiler.Cfg]

Relocatable effect (a predicate that depend on two states).

E [Wp.Model.Registry]
Env [Plang]
Env [Wp.Plang]
Eset [Cil2cfg]

set of edges

ExtEqual [Wp_parameters]
ExtEqual [Wp.Wp_parameters]
ExternArrays [Wp_parameters]
ExternArrays [Wp.Wp_parameters]
F
F [Lang]
F [Wp.Lang]
Factory
Factory [Wp]
Field [Lang]
Field [Wp.Lang]
Filter [Wp_parameters]
Filter [Wp.Wp_parameters]
Filtering

Sequent Cleaning

Filtering [Wp]
Fmap [Register]
Fmap [Tactical]
Fmap [Wp.Tactical]
Footprint

Term Footprints

Fun [Lang]
Fun [Wp.Lang]
G
GOAL [Wpo]
GOAL [Wp.Wpo]
GOALS [Register]
Generate [Wp_parameters]
Generate [Wp.Wp_parameters]
Generator
Generator [Model]

projectified, depend on the model, not serialized

Generator [Wp.Model]

projectified, depend on the model, not serialized

Gmap [Wpo]
Gmap [Wp.Wpo]
Goal [ProverWhy3]
Ground [Letify]
Ground [Wp_parameters]
Ground [Wp.Wp_parameters]
GuiComposer
GuiConfig
GuiGoal
GuiList
GuiNavigator
GuiPanel
GuiProof
GuiProver
GuiSequent
GuiSource
GuiTactic
H
HE [Cil2cfg]
Hashtbl [CfgCompiler.Cfg.Node]
Hashtbl [Wp.CfgCompiler.Cfg.Node]
Hashtbl [Datatype.S_with_collections]
Havoc [TacHavoc]
Heap [Sigs.Model]

Chunks Sets and Maps.

Heap [Wp.Sigs.Model]

Chunks Sets and Maps.

Hints [Wp_parameters]
Hints [Wp.Wp_parameters]
I
InCtxt [Wp_parameters]
InCtxt [Wp.Wp_parameters]
InHeap [Wp_parameters]
InHeap [Wp.Wp_parameters]
Index [Wpo]
Index [Model]

projectified, depend on the model, not serialized

Index [Wp.Wpo]
Index [Wp.Model]

projectified, depend on the model, not serialized

Indexed [Wprop]
Indexed2 [Wprop]
Init [Wp_parameters]
Init [Wp.Wp_parameters]
InitAlias [Wp_parameters]
InitAlias [Wp.Wp_parameters]
InitWithForall [Wp_parameters]
InitWithForall [Wp.Wp_parameters]
K
Key [Datatype.Hashtbl]

Datatype for the keys of the hashtbl.

Key [Datatype.Map]

Datatype for the keys of the map.

L
L [Sigs.Compiler]
L [Sigs.LogicAssigns]
L [Wp.Sigs.Compiler]
L [Wp.Sigs.LogicAssigns]
LabelMap [Clabels]
LabelMap [Wp.Clabels]
LabelSet [Clabels]
LabelSet [Wp.Clabels]
Lang
Lang [Wp]
Let [Wp_parameters]
Let [Wp.Wp_parameters]
Letify
Literals [Wp_parameters]
Literals [Wp.Wp_parameters]
Logic [Cvalues]
LogicAssigns
LogicBuiltins
LogicBuiltins [Wp]
LogicCompiler
LogicCompiler [Wp]
LogicSemantics
LogicSemantics [Wp]
LogicUsage
LogicUsage [Wp]
M
M [Sigs.Compiler]
M [Sigs.LogicAssigns]
M [Sigs.LogicSemantics]

Underlying memory model

M [Sigs.CodeSemantics]

The underlying memory model

M [Wp.Sigs.Compiler]
M [Wp.Sigs.LogicAssigns]
M [Wp.Sigs.LogicSemantics]

Underlying memory model

M [Wp.Sigs.CodeSemantics]

The underlying memory model

MACHINE [Matrix]
Make [StmtSemantics]
Make [MemVar]
Make [Sigma]
Make [LogicAssigns]
Make [LogicSemantics]
Make [LogicCompiler]
Make [CodeSemantics]
Make [Wp.StmtSemantics]
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 [CfgCompiler.Cfg.Node]
Map [Warning]
Map [Wp.CfgCompiler.Cfg.Node]
Map [Datatype.S_with_collections]
Map [Wp.Warning]
Matrix
Mcfg
Mcfg [Wp]
MemEmpty
MemTyped
MemTyped [Wp]
MemVar
MemVar [Wp]
MemZeroAlias
Model

Model Registration

Model [Wp_parameters]
Model [Wp]
Model [Wp.Wp_parameters]
Models [Register]
Mstate
Mstate [Wp]
N
N [Lang]
N [Wp.Lang]
NATURAL [Matrix]
Node [CfgCompiler.Cfg]

Program point along a trace.

Node [Wp.CfgCompiler.Cfg]

Program point along a trace.

NormAtLabels
NormAtLabels [Wp]
O
Overflows [Wp_parameters]
Overflows [Wp.Wp_parameters]
P
P [CfgCompiler.Cfg]

Relocatable predicate

P [Wp.CfgCompiler.Cfg]

Relocatable predicate

PM [Register]
Parasite [Wp_parameters]
Parasite [Wp.Wp_parameters]
Passive
Passive [Wp]
Pcfg
Pcfg [Wp]
Pcond
Pcond [Wp]
Plang
Plang [Wp]
Pmap [VCS]
Pmap [Lang.F]
Pmap [Wp.VCS]
Pmap [Wp.Lang.F]
Prenex [Wp_parameters]
Prenex [Wp.Wp_parameters]
Print [Wp_parameters]
Print [Wp.Wp_parameters]
Procs [Wp_parameters]
Procs [Wp.Wp_parameters]
Proof

Proof Script Database

ProofEngine

Interactive Proof Engine

ProofScript
ProofSession
ProofTrace [Wp_parameters]
ProofTrace [Wp.Wp_parameters]
PropId [WpPropId]
PropId [Wp.WpPropId]
Properties [Wp_parameters]
Properties [Wp.Wp_parameters]
Prover
Prover [Wp]
ProverCoq
ProverErgo
ProverScript
ProverSearch
ProverTask
ProverTask [Wp]
ProverWhy3
ProverWhy3ide
Provers [Wp_parameters]
Provers [Wp.Wp_parameters]
Prune [Wp_parameters]
Prune [Wp.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]
QedChecks [Wp.Wp_parameters]
R
RTE [Wp_parameters]
RTE [Wp.Wp_parameters]
Range [Auto]
Range [Wp.Auto]
Reduce [Wp_parameters]
Reduce [Wp.Wp_parameters]
RefUsage
RefUsage [Wp]
Region
Register
Report [Wp_parameters]
Report [Wp.Wp_parameters]
ReportJson [Wp_parameters]
ReportJson [Wp.Wp_parameters]
ReportName [Wp_parameters]
ReportName [Wp.Wp_parameters]
Repr

Term & Predicate Introspection

Repr [Wp]
Rformat
S
S [Wpo]
S [CfgCompiler.Cfg]

The memory model used.

S [Model]
S [Wp.Wpo]
S [Wp.CfgCompiler.Cfg]

The memory model used.

S [Wp.Model]
Script
Script [Wp_parameters]
Script [Wp.Wp_parameters]
Separated [TacHavoc]
Separation
Separation [Wp_parameters]
Separation [Wp]
Separation [Wp.Wp_parameters]
Set [CfgCompiler.Cfg.Node]
Set [Warning]
Set [Wp.CfgCompiler.Cfg.Node]
Set [Datatype.S_with_collections]
Set [Wp.Warning]
Sigma
Sigma [Sigs.Model]

Model Environments.

Sigma [Letify]
Sigma [Wp]
Sigma [Wp.Sigs.Model]

Model Environments.

Sigs

Common Types and Signatures

Sigs [Wp]
Simpl [Wp_parameters]
Simpl [Wp.Wp_parameters]
SimplifyForall [Wp_parameters]
SimplifyForall [Wp.Wp_parameters]
SimplifyIsCint [Wp_parameters]
SimplifyIsCint [Wp.Wp_parameters]
SimplifyLandMask [Wp_parameters]
SimplifyLandMask [Wp.Wp_parameters]
SimplifyType [Wp_parameters]
SimplifyType [Wp.Wp_parameters]
Split [Letify]

Pruning strategy ; selects most occurring literals to split cases.

Split [Wp_parameters]
Split [Wp.Wp_parameters]
SplitDepth [Wp_parameters]
SplitDepth [Wp.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]
StatusAll [Wp.Wp_parameters]
StatusFalse [Wp_parameters]
StatusFalse [Wp.Wp_parameters]
StatusMaybe [Wp_parameters]
StatusMaybe [Wp.Wp_parameters]
StatusTrue [Wp_parameters]
StatusTrue [Wp.Wp_parameters]
Steps [Wp_parameters]
Steps [Wp.Wp_parameters]
StmtSemantics
StmtSemantics [Wp]
Strategy

Term & Predicate Selection

Strategy [Wp]
Subst [Lang]
Subst [Wp.Lang]
T
T [CfgCompiler.Cfg]

Relocatable term

T [Clabels]
T [Wp.CfgCompiler.Cfg]

Relocatable term

T [Wp.Clabels]
TacArray

Built-in Array Tactical (auto-registered)

TacBitrange

Built-in Bit Range Tactical (auto-registered)

TacBitwised

Built-in Bitwised-Eq Tactical (auto-registered)

TacChoice

Built-in Choice, Absurd & Contrapose Tactical (auto-registered)

TacCompound

Built-in Compound Tactical (auto-registered)

TacCongruence

Built-in Tactical for Product & Division Comparison (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)

TacOverflow

Auto registered overflow tactic

TacRange

Built-in Range Tactical (auto-registered)

TacRewrite

Built-in Range Tactical (auto-registered)

TacShift

Built-in Shift 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]
TimeExtra [Wp_parameters]
TimeExtra [Wp.Wp_parameters]
TimeMargin [Wp_parameters]
TimeMargin [Wp.Wp_parameters]
Timeout [Wp_parameters]
Timeout [Wp.Wp_parameters]
Tmap [Lang.F]
Tmap [Wp.Lang.F]
Trigger [Definitions]
Trigger [Wp.Definitions]
TruncPropIdFileName [Wp_parameters]
TruncPropIdFileName [Wp.Wp_parameters]
TryHints [Wp_parameters]
TryHints [Wp.Wp_parameters]
Tset [Lang.F]
Tset [Wp.Lang.F]
U
UnfoldAssigns [Wp_parameters]
UnfoldAssigns [Wp.Wp_parameters]
UpdateScript [Wp_parameters]
UpdateScript [Wp.Wp_parameters]
V
VC
VC [CfgWP]
VC [Wp]
VCS

Verification Condition Status

VCS [Wp]
VC_Annot [Wpo]
VC_Annot [Wp.Wpo]
VC_Check [Wpo]
VC_Check [Wp.Wpo]
VC_Lemma [Wpo]
VC_Lemma [Wp.Wpo]
Validity [TacHavoc]
Var [Lang.F]
Var [Wp.Lang.F]
Vars [Lang.F]
Vars [Wp.Lang.F]
Vlist
Vmap [Lang.F]
Vmap [Wp.Lang.F]
Volatile [Wp_parameters]
Volatile [Wp.Wp_parameters]
Vset
Vset [Wp]
W
WP [Wp_parameters]
WP [Wp.Wp_parameters]
Warning

Contextual Errors

Warning [Wp]
Why3 [Wp_parameters]
Why3 [Wp.Wp_parameters]
Why3_xml
WhyFlags [Wp_parameters]
WhyFlags [Wp.Wp_parameters]
WhyLibs [Wp_parameters]
WhyLibs [Wp.Wp_parameters]
Wp

WP Public API

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
WpPropId [Wp]
WpRTE

Returns true is call pre-conditions have been already generated by RTE.

WpReport

Export Statistics.

WpStrategy
WpTac
Wp_error
Wp_parameters
Wp_parameters [Wp]
Wpo
Wpo [Wp]
Wprop

Indexed API