Auto |
Registered Strategies
It is always safe to apply strategies to any goal.
|
Calculus |
Generic WP calculus
|
CfgDump | |
CfgWP | |
Cfloat |
Floating Arithmetic Model
|
Cil2cfg |
abstract type of a cfg
|
Cint |
Integer Arithmetic Model
|
Clabels |
Normalized C-labels
|
Cleaning | |
CodeSemantics |
None means equal to zero/null
|
Conditions |
Sequent
|
Context |
Current Loc
|
Cstring |
String Literal
|
Ctypes |
C-Types
|
Cvalues |
Int-As-Booleans
|
Definitions |
Unique
|
Driver |
Memoized loading of drivers according to current
WP options.
|
Dyncall |
Returns an property identifier for the precondition.
|
Factory | "Var,Typed,Nat,Real" memory model.
|
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
|
Letify | bind sigma defs xs select definitions in defs
targeting variables xs .
|
LogicAssigns | |
LogicBuiltins |
integer
|
LogicCompiler |
Definitions
|
LogicSemantics |
Debug
|
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 | |
MemTyped |
describe the content of literal strings
|
MemVar | |
MemZeroAlias | |
Memory |
Memory Values
|
Model |
Model Registration
|
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 |
Proof Script Database
|
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 |
None if the po is trivial
|
ProverWhy3ide | |
RefUsage |
Variable accesses from C code and code annotations
|
Region |
Paths
|
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 | |
Separation |
Elementary regions
|
Sigma | |
Splitter | |
Strategy |
Term & Predicate Selection
|
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
|
VC |
Proof Obligations
|
VCS |
Verification Condition Status
|
Vlist |
VList Theory Builtins
|
Vset |
Logical Sets
|
Warning |
Contextual Errors
|
Why3_xml |
returns the list of XML elements from the given file.
|
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.
|
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
|