Wp plugin

Directory plugins

Section Wp (in plugins/wp)


AssignsCompleteness

This module is used to check the assigns specification of a given function so that if it is not precise enough to enable precise memory models hypotheses computation, the assigns specification is considered incomplete.

Auto
Cache
Calculus

Generic WP calculus

CfgAnnot
CfgCalculus
CfgCompiler
CfgDump
CfgGenerator
CfgInfos
CfgInit
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
Filter_axioms
Filtering

Sequent Cleaning

Footprint

Term Footprints

Generator

Compute model setup from command line options.

GuiComposer
GuiConfig
GuiGoal
GuiList
GuiNavigator
GuiPanel
GuiProof
GuiProver
GuiSequent
GuiSource
GuiTactic
Lang
Layout

Region Utilities

Letify
LogicAssigns
LogicBuiltins
LogicCompiler
LogicSemantics
LogicUsage
Matrix
Mcfg
MemEmpty
MemLoader

Compound Loader

MemMemory
MemRegion
MemTyped
MemVar
MemZeroAlias
MemoryContext
Mstate
NormAtLabels
Passive
Pcfg
Pcond
Plang
Proof

Coq Proof Scripts

ProofEngine

Interactive Proof Engine

ProofScript
ProofSession
Prover
ProverCoq
ProverErgo
ProverScript
ProverSearch
ProverTask
ProverWhy3
RefUsage
Region
RegionAccess
RegionAnalysis

Memoized and Projectified Region Analyzis for the given Function.

RegionAnnot
RegionDump
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)

TacBittest

Built-in Bit-Test 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)

TacInduction

Built-in Range 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)

TacSequence

Built-in Sequence 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

Why3Provers
Wp

WP Public API

WpAnnot
WpContext

Model Registration

WpGenerator
WpPropId
WpRTE

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

WpReached

Reachability for Smoke Tests

WpReport

Export Statistics.

WpStrategy
WpTac
WpTarget

This module computes the set of kernel functions that are considered by the command line options transmitted to WP.

Wp_error
Wp_parameters
Wpo
Wprop

Indexed API