Wp plugin

Directory plugins

Section Wp (in plugins/wp)


Auto
Calculus

Generic WP calculus

CfgCompiler
CfgDump
CfgWP
Cfloat

Floating Arithmetic Model

Cil2cfg

Build a CFG of a function keeping some information of the initial structure.

Cint

Integer Arithmetic Model

Clabels

Normalized C-labels

Cleaning
Cmath

Math Operators

CodeSemantics
Conditions
Context

Current Loc

Cstring
Ctypes

C-Types

Cvalues
Definitions
Driver
Dyncall
Factory
Filtering

Sequent Cleaning

Footprint

Term Footprints

Generator
GuiComposer
GuiConfig
GuiGoal
GuiList
GuiNavigator
GuiPanel
GuiProof
GuiProver
GuiSequent
GuiSource
GuiTactic
Lang
Letify
LogicAssigns
LogicBuiltins
LogicCompiler
LogicSemantics
LogicUsage
Matrix
Mcfg
MemEmpty
MemTyped
MemVar
MemZeroAlias
MemoryContext
Model

Model Registration

Mstate
NormAtLabels
Passive
Pcfg
Pcond
Plang
Proof

Coq Proof Scripts

ProofEngine

Interactive Proof Engine

ProofScript
ProofSession
Prover
ProverCoq
ProverDetect

Why3 Prover Detection

ProverErgo
ProverScript
ProverSearch
ProverTask
ProverWhy3
ProverWhy3ide
RefUsage
Region
Register
Repr

Term & Predicate Introspection

Rformat
Script
Sigma
Sigs

Common Types and Signatures

Splitter
StmtSemantics
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
VCS

Verification Condition Status

Vlist
Vset
Warning

Contextual Errors

Why3_xml
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.

WpPropId
WpRTE

Invoke RTE to generate missing annotations for the given function and model.

WpReport

Export Statistics.

WpStrategy
WpTac
Wp_error
Wp_parameters
Wpo
Wprop

Indexed API