Wp plugin


Directory plugins

Section Wp (in plugins/wp)


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