Auto |
Basic Strategies
It is always safe to apply strategies to any goal.
|
Calculus |
Generic WP calculus
|
CfgCompiler |
Control Flow Graphs
|
CfgDump | |
CfgWP | |
Cfloat |
Floating Arithmetic Model
|
Cil2cfg |
abstract type of a cfg
|
Cint |
Integer Arithmetic Model
|
Clabels |
Normalized C-labels
|
Cleaning | |
Cmath |
Math Operators
|
CodeSemantics | |
Conditions |
Predicate Introduction
|
Context |
Current Loc
|
Cstring |
String Literal
|
Ctypes |
C-Types
|
Cvalues |
Pretty Printing
|
Definitions |
Unique
|
Driver |
Memoized loading of drivers according to current
WP options.
|
Dyncall |
Returns
None if there is no specified dynamic call.
|
Factory | "Var,Typed,Nat,Real" memory model.
|
Filter_axioms |
inlining
|
Filtering |
Sequent Cleaning
|
Footprint |
Term Footprints
|
Generator | |
GuiComposer |
request-for-update event
|
GuiConfig |
Edit enabled provers
|
GuiGoal | |
GuiList | |
GuiNavigator | |
GuiPanel | |
GuiProof | |
GuiProver |
Requires
filter prover .
|
GuiSequent | |
GuiSource | |
GuiTactic | |
Lang |
Logic Language based on Qed
|
Layout |
Region Utilities
|
Letify | bind sigma defs xs select definitions in defs
targeting variables xs .
|
LogicAssigns | |
LogicBuiltins |
integer
|
LogicCompiler |
Definitions
|
LogicSemantics |
cast to a C type
|
LogicUsage |
Trims the original name
|
Matrix |
unique w.r.t
equal
|
Mcfg |
This is what is really needed to propagate something through the CFG.
|
MemEmpty | |
MemLoader |
Compound Loader
|
MemMemory |
Theory
|
MemRegion | |
MemTyped |
describe the content of literal strings
|
MemVar |
Memory Model Hypotheses
|
MemZeroAlias | |
MemoryContext | &x the cell x
|
Mstate | |
NormAtLabels |
push the Tat down to the 'data' operations.
|
Passive |
Passive Forms
|
Pcfg |
current state
|
Pcond |
All-in-one printers
|
Plang |
Lang Pretty-Printer
|
Proof |
Coq Proof Scripts
|
ProofEngine |
Interactive Proof Engine
|
ProofScript |
With number of pending goals
|
ProofSession | |
Prover | |
ProverCoq | |
ProverErgo | |
ProverScript |
Play provers with valid result (default: true)
|
ProverSearch | |
ProverTask |
never fails
|
ProverWhy3 |
Equality used in the goal, simpler to prove than polymorphic equality
|
RefUsage |
By lattice order of usage
|
Region | |
RegionAccess | |
RegionAnalysis |
Memoized and Projectified Region Analyzis for the given Function.
|
RegionAnnot |
Auto when `-wp-region`
|
RegionDump | |
Register |
Do on_server_stop save why3 session
|
Repr |
Term & Predicate Introspection
|
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 .
|
Script | |
Sigma |
Get a map of the chunks (the data is not important)
|
Sigs |
Common Types and Signatures
|
Splitter |
erase all tags
|
StmtSemantics |
Compilation environment
|
Strategy |
Term & Predicate Selection
|
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
|
VC |
Proof Obligations
|
VCS |
Verification Condition Status
|
Vlist |
VList Theory Builtins
|
Vset |
Logical Sets
|
Warning |
Contextual Errors
|
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
|
WpPropId |
Beside the property identification, it can be found in different contexts
depending on which part of the computation is involved.
|
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
|
Wpo |
Proof Obligations
|
Wprop |
Indexed API
|