Wp plugin


Directory plugins

Section Wp (in plugins/wp)


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