Index of modules

A
A [Sigs.Compiler]
A [Wp.Sigs.Compiler]
ADT [Lang]
ADT [Wp.Lang]
Absurd [TacChoice]
AinfoComparable [Ctypes]
AinfoComparable [Wp.Ctypes]
Alias [Layout]
AliasInit [Wp_parameters]
AliasInit [Wp.Wp_parameters]
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]
AssignsCompleteness

This module is used to check the assigns specification of a given function so that if it is not precise enough to enable precise memory models hypotheses computation, the assigns specification is considered incomplete.

AssignsCompleteness [Wp]
Auto
Auto [Wp_parameters]
Auto [Wp]
Auto [Wp.Wp_parameters]
AutoDepth [Wp_parameters]
AutoDepth [Wp.Wp_parameters]
AutoWidth [Wp_parameters]
AutoWidth [Wp.Wp_parameters]
Automaton [Interpreted_automata]

Datatype for automata

B
BackTrack [Wp_parameters]
BackTrack [Wp.Wp_parameters]
Behaviors [Wp_parameters]
Behaviors [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]
Cache
Cache [Wp_parameters]
Cache [Wp.Wp_parameters]
CacheDir [Wp_parameters]
CacheDir [Wp.Wp_parameters]
CacheEnv [Wp_parameters]
CacheEnv [Wp.Wp_parameters]
CachePrint [Wp_parameters]
CachePrint [Wp.Wp_parameters]
Calculus

Generic WP calculus

CalleePreCond [Wp_parameters]
CalleePreCond [Wp.Wp_parameters]
Cfg [Calculus]
Cfg [CfgInfos]
Cfg [StmtSemantics.Make]
Cfg [CfgCompiler]
Cfg [Wp.StmtSemantics.Make]
Cfg [Wp.CfgCompiler]
CfgAnnot
CfgCalculus
CfgCompiler
CfgCompiler [Wp]
CfgDump
CfgGenerator
CfgInfos
CfgInit
CfgWP
Cfloat

Floating Arithmetic Model

Cfloat [Wp]
CheckMemoryContext [Wp_parameters]
CheckMemoryContext [Wp.Wp_parameters]
Choice [TacChoice]
Chunk [MemLoader.Model]
Chunk [Sigs.Model]

Memory model chunks.

Chunk [Sigs.Sigma]
Chunk [Layout]
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
Cluster [Layout]
Cmath

Math Operators

CodeSemantics
CodeSemantics [Wp]
Compound [Layout]
Compute [Interpreted_automata]

This module defines the previous functions without memoization

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]
Dataflow [Interpreted_automata]

Builds a simple dataflow analysis over an input domain.

Definitions
Definitions [Wp]
Defs [Letify]
Deref [Layout]
Detect [Wp_parameters]
Detect [Wp.Wp_parameters]
Driver
Driver [Wp]
Drivers [Wp_parameters]
Drivers [Wp.Wp_parameters]
Dump [Cil2cfg]
Dump [Wp_parameters]
Dump [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 [WpContext.Registry]
E [Wp.CfgCompiler.Cfg]

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

E [Wp.WpContext.Registry]
Edge [Interpreted_automata]
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]
FilterInit [Wp_parameters]
FilterInit [Wp.Wp_parameters]
Filter_axioms
Filtering

Sequent Cleaning

Filtering [Wp]
Flat [Layout]

Flatten arrays

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

Term Footprints

For_export [Lang]

For why3_api but circular dependency

For_export [Wp.Lang]

For why3_api but circular dependency

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

Compute model setup from command line options.

Generator [WpContext]

projectified, depend on the model, not serialized

Generator [Wp.WpContext]

projectified, depend on the model, not serialized

GeneratorID [WpContext]

projectified, depend on the model, not serialized

GeneratorID [Wp.WpContext]

projectified, depend on the model, not serialized

Gmap [Wpo]
Gmap [Wp.Wpo]
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 [Datatype.S_with_collections]
Hashtbl [Wp.CfgCompiler.Cfg.Node]
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 [WpContext]

projectified, depend on the model, not serialized

Index [Wp.Wpo]
Index [Wp.WpContext]

projectified, depend on the model, not serialized

Indexed [Wprop]
Indexed2 [Wprop]
Init [Wp_parameters]
Init [Wp.Wp_parameters]
InitWithForall [Wp_parameters]
InitWithForall [Wp.Wp_parameters]
Interactive [Wp_parameters]
Interactive [Wp.Wp_parameters]
InteractiveTimeout [Wp_parameters]
InteractiveTimeout [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]
Layout

Region Utilities

Legacy [Wp_parameters]
Legacy [Wp.Wp_parameters]
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]
Lpath [RegionAnnot]
Lvalue [Layout]
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

MINDEX [WpContext]
MINDEX [Wp.WpContext]
MODEL [WpContext]
MODEL [Wp.WpContext]
Make [CfgCalculus]
Make [CfgInit]
Make [StmtSemantics]
Make [MemVar]
Make [MemLoader]

Generates Loader for Compound Values

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.

Make [Wp.StmtSemantics]
Make [Wp.MemVar]
Make [Wp.Sigma]
Make [Wp.LogicSemantics]
Make [Wp.LogicCompiler]
Make [Wp.CodeSemantics]
Map [CfgCompiler.Cfg.Node]
Map [Region]
Map [Warning]
Map [Datatype.S_with_collections]
Map [Wp.CfgCompiler.Cfg.Node]
Map [Wp.Warning]
Matrix
Matrix [Layout]
Mcfg
Mcfg [Wp]
MemEmpty
MemLoader

Compound Loader

MemMemory
MemRegion
MemTyped
MemTyped [Wp]
MemVar
MemVar [Wp]
MemZeroAlias
MemoryContext
MemoryContext [Wp_parameters]
MemoryContext [Wp]
MemoryContext [Wp.Wp_parameters]
Model [Wp_parameters]
Model [Wp.Wp_parameters]
Models [Register]
Mstate
Mstate [Wp]
N
N [Lang]
N [Wp.Lang]
Node [CfgCompiler.Cfg]

Program point along a trace.

Node [Wp.CfgCompiler.Cfg]

Program point along a trace.

NormAtLabels
NormAtLabels [Wp]
O
Offset [Layout]
Overlay [Layout]
P
P [CfgCompiler.Cfg]

Relocatable predicate

P [Wp.CfgCompiler.Cfg]

Relocatable predicate

PM [Register]
Pack [Layout]

Pack fields

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]
PrecondWeakening [Wp_parameters]
PrecondWeakening [Wp.Wp_parameters]
Prenex [Wp_parameters]
Prenex [Wp.Wp_parameters]
Print [Wp_parameters]
Print [Wp.Wp_parameters]
Procs [Wp_parameters]
Procs [Wp.Wp_parameters]
Proof

Coq Proof Scripts

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
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]
R
R [Region]
RTE [Wp_parameters]
RTE [Wp.Wp_parameters]
RW [Layout]

Read-Write access

Range [Auto]
Range [Layout]
Range [Wp.Auto]
Reduce [Wp_parameters]
Reduce [Wp.Wp_parameters]
RefUsage
RefUsage [Wp]
Region
Region [Wp_parameters]
Region [Wp.Wp_parameters]
RegionAccess
RegionAnalysis

Memoized and Projectified Region Analyzis for the given Function.

RegionAnnot
RegionDump
Region_annot [Wp_parameters]
Region_annot [Wp.Wp_parameters]
Region_cluster [Wp_parameters]
Region_cluster [Wp.Wp_parameters]
Region_fixpoint [Wp_parameters]
Region_fixpoint [Wp.Wp_parameters]
Region_flat [Wp_parameters]
Region_flat [Wp.Wp_parameters]
Region_inline [Wp_parameters]
Region_inline [Wp.Wp_parameters]
Region_pack [Wp_parameters]
Region_pack [Wp.Wp_parameters]
Region_rw [Wp_parameters]
Region_rw [Wp.Wp_parameters]
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
Root [Layout]
RunAllProvers [Wp_parameters]
RunAllProvers [Wp.Wp_parameters]
S
S [Wpo]
S [CfgCompiler.Cfg]

The memory model used.

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

The memory model used.

S [Wp.WpContext]
SCOPE [WpContext]
SCOPE [Wp.WpContext]
Script
Script [Wp_parameters]
Script [Wp.Wp_parameters]
Separated [TacHavoc]
Set [CfgCompiler.Cfg.Node]
Set [Region]
Set [Warning]
Set [Datatype.S_with_collections]
Set [Wp.CfgCompiler.Cfg.Node]
Set [Wp.Warning]
Sigma [MemLoader.Model]
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]
SmokeDeadcall [Wp_parameters]
SmokeDeadcall [Wp.Wp_parameters]
SmokeDeadcode [Wp_parameters]
SmokeDeadcode [Wp.Wp_parameters]
SmokeDeadloop [Wp_parameters]
SmokeDeadloop [Wp.Wp_parameters]
SmokeTests [Wp_parameters]
SmokeTests [Wp.Wp_parameters]
SmokeTimeout [Wp_parameters]
SmokeTimeout [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]
SplitMax [Wp_parameters]
SplitMax [Wp.Wp_parameters]
Splitter
Splitter [Wp]
Static [WpContext]

projectified, independent from the model, not serialized

Static [Wp.WpContext]

projectified, independent from the model, not serialized

StaticGenerator [WpContext]

projectified, independent from the model, not serialized

StaticGenerator [Wp.WpContext]

projectified, independent from the model, not serialized

StaticGeneratorID [WpContext]

projectified, independent from the model, not serialized

StaticGeneratorID [Wp.WpContext]

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.F]
Subst [Wp.Lang.F]
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)

TacBittest

Built-in Bit-Test 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)

TacInduction

Built-in Range 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)

TacSequence

Built-in Sequence 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]
UnrollUnnatural [Interpreted_automata]
UpdateScript [Wp_parameters]
UpdateScript [Wp.Wp_parameters]
Usage [Layout]
V
VC
VC [Wp]
VCS

Verification Condition Status

VCS [Wp]
VC_Annot [Wpo]
VC_Annot [Wp.Wpo]
VC_Lemma [Wpo]
VC_Lemma [Wp.Wpo]
Validity [TacHavoc]
Value [Layout]
Var [Lang.F]
Var [Wp.Lang.F]
Vars [Lang.F]
Vars [Wp.Lang.F]
Version [Interpreted_automata.UnrollUnnatural]
Vertex [Interpreted_automata]

Datatype for vertices

Vertex_Set [Interpreted_automata.UnrollUnnatural]
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]
WTO [Interpreted_automata.UnrollUnnatural]
WTO [Interpreted_automata]
WTOIndex [Interpreted_automata]

Datatype for wto_index

Warning

Contextual Errors

Warning [Wp]
WeakIntModel [Wp_parameters]
WeakIntModel [Wp.Wp_parameters]
Why3Flags [Wp_parameters]
Why3Flags [Wp.Wp_parameters]
Why3Provers
Wp

WP Public API

WpAnnot
WpContext

Model Registration

WpContext [Wp]
WpGenerator
WpPropId
WpPropId [Wp]
WpRTE

Invoke RTE to generate missing annotations for the given function and model.

WpReached

Reachability for Smoke Tests

WpReport

Export Statistics.

WpStrategy
WpTac
WpTarget

This module computes the set of kernel functions that are considered by the command line options transmitted to WP.

Wp_error
Wp_parameters
Wp_parameters [Wp]
Wpo
Wpo [Wp]
Wprop

Indexed API