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]
Auto
Basic Strategies It is always safe to apply strategies to any goal.
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]
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 [Wp_parameters]
Cache [Wp.Wp_parameters]
CacheEnv [Wp_parameters]
CacheEnv [Wp.Wp_parameters]
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
Control Flow Graphs
CfgCompiler [Wp]
CfgDump
CfgWP
Cfloat
Floating Arithmetic Model
Cfloat [Wp]
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
abstract type of a cfg
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]
Computer [CfgWP]
Conditions
Predicate Introduction
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
String Literal
Cstring [Wp]
Ctypes
C-Types
Ctypes [Wp]
Cvalues
Pretty Printing

D
DISK [Wpo]
DISK [Wp.Wpo]
Definitions
Unique
Definitions [Wp]
Defs [Letify]
Deref [Layout]
Detect [Wp_parameters]
Detect [Wp.Wp_parameters]
Driver
Memoized loading of drivers according to current WP options.
Driver [Wp]
Drivers [Wp_parameters]
Drivers [Wp.Wp_parameters]
DynCall [Wp_parameters]
DynCall [Wp.Wp_parameters]
Dyncall
Returns None if there is no specified dynamic call.

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]
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
"Var,Typed,Nat,Real" memory model.
Factory [Wp]
Field [Lang]
Field [Wp.Lang]
Filter [Wp_parameters]
Filter [Wp.Wp_parameters]
Filter_axioms
inlining
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
GOAL [Wpo]
GOAL [Wp.Wpo]
GOALS [Register]
Generate [Wp_parameters]
Generate [Wp.Wp_parameters]
Generator
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
request-for-update event
GuiConfig
Edit enabled provers
GuiGoal
GuiList
GuiNavigator
GuiPanel
GuiProof
GuiProver
Requires filter prover.
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]

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
Logic Language based on Qed
Lang [Wp]
Layout
Region Utilities
Let [Wp_parameters]
Let [Wp.Wp_parameters]
Letify
bind sigma defs xs select definitions in defs targeting variables xs.
Literals [Wp_parameters]
Literals [Wp.Wp_parameters]
Logic [Cvalues]
LogicAssigns
LogicBuiltins
integer
LogicBuiltins [Wp]
LogicCompiler
Definitions
LogicCompiler [Wp]
LogicSemantics
cast to a C type
LogicSemantics [Wp]
LogicUsage
Trims the original name
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
MACHINE [Matrix]
MODEL [WpContext]
MODEL [Wp.WpContext]
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
unique w.r.t equal
Matrix [Layout]
Mcfg
This is what is really needed to propagate something through the CFG.
Mcfg [Wp]
MemEmpty
MemLoader
Compound Loader
MemMemory
Theory
MemRegion
MemTyped
describe the content of literal strings
MemTyped [Wp]
MemVar
Memory Model Hypotheses
MemVar [Wp]
MemZeroAlias
MemoryContext
&x the cell x
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]
NATURAL [Matrix]
Node [CfgCompiler.Cfg]
Program point along a trace.
Node [Wp.CfgCompiler.Cfg]
Program point along a trace.
NormAtLabels
push the Tat down to the 'data' operations.
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 Forms
Passive [Wp]
Pcfg
current state
Pcfg [Wp]
Pcond
All-in-one printers
Pcond [Wp]
Plang
Lang Pretty-Printer
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
With number of pending goals
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
Play provers with valid result (default: true)
ProverSearch
ProverTask
never fails
ProverTask [Wp]
ProverWhy3
Equality used in the goal, simpler to prove than polymorphic equality
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
By lattice order of usage
RefUsage [Wp]
Region
Region [Wp_parameters]
Region [Wp.Wp_parameters]
RegionAccess
RegionAnalysis
Memoized and Projectified Region Analyzis for the given Function.
RegionAnnot
Auto when `-wp-region`
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
Do on_server_stop save why3 session
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
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.
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
Get a map of the chunks (the data is not important)
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
erase all tags
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
Compilation environment
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)
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]
Usage [Layout]

V
VC
Proof Obligations
VC [CfgWP]
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]
Vlist
VList Theory Builtins
Vmap [Lang.F]
Vmap [Wp.Lang.F]
Volatile [Wp_parameters]
Volatile [Wp.Wp_parameters]
Vset
Logical Sets
Vset [Wp]

W
WP [Wp_parameters]
WP [Wp.Wp_parameters]
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
Every access to annotations have to go through here, so this is the place where we decide what the computation is allowed to use.
WpContext
Model Registration
WpContext [Wp]
WpPropId
Beside the property identification, it can be found in different contexts depending on which part of the computation is involved.
WpPropId [Wp]
WpRTE
Invoke RTE to generate missing annotations for the given function and model.
WpReached
Reachability for Smoke Tests
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
Function Selection
Wp_parameters [Wp]
Wpo
Proof Obligations
Wpo [Wp]
Wprop
Indexed API