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