Module Wp

This the API of the WP plug-in

High-Level External API

The following modules are the recommanded entry points for using WP programmatically. They are meant to be relatively stable over time.

module VC : sig ... end

WP Proof Obligation Generator and Management

module VCS : sig ... end

Provers and Proof Obligations Results

module Wp_parameters : sig ... end

WP Plugin Interface

Advanced Usage API

The following modules entry points for using WP advanced features, such as proof obligation manipulation, tactics and strategies. These modules might expose internal features of WP that are subject to change. Developpers using this API are encouraged to contact us for a roadmap information and further collaboration.

module Repr : sig ... end

High-Level Term Representation

module Lang : sig ... end

Low-Level Logic Terms and Predicates

module Definitions : sig ... end

Generated Logic Definitions

module Conditions : sig ... end

Proof Task and Simplifiers

module Tactical : sig ... end

Tactics Entry Points

module Strategy : sig ... end

Strategies Entry Points

module Generator : sig ... end

WP Proof Obligation Generator

module Register : sig ... end

Command Line Processing

Low-Level Internal API

The following modules are _not_ intended to be used externally. The target audience is WP plug-in developpers. However, developpers interested in such low-level features are encouraged to contact us for more informations.

Model Registration

module Factory : sig ... end
module WpContext : sig ... end

Model Registration

Memory Models

module MemDebug : sig ... end
module MemEmpty : sig ... end
module MemLoader : sig ... end

Compound Loader

module MemMemory : sig ... end
module MemBytes : sig ... end
module MemTyped : sig ... end
module MemVal : sig ... end
module MemVar : sig ... end
module MemZeroAlias : sig ... end

Other Models

module Cint : sig ... end

Integer Arithmetic Model

module Cfloat : sig ... end

Floating Arithmetic Model

module Cmath : sig ... end

Math Operators

module Cstring : sig ... end

State Model

module Sigma : sig ... end
module Passive : sig ... end

Passive Forms

module Mstate : sig ... end

Model Hypotheses

module MemoryContext : sig ... end
module RefUsage : sig ... end
module WpTarget : sig ... end

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

module AssignsCompleteness : sig ... end

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.

Region Analysis

module Layout : sig ... end

Region Utilities

Compilers

module Sigs : sig ... end

Common Types and Signatures

module Driver : sig ... end
module Context : sig ... end

Contextual Values

module Ctypes : sig ... end

C-Types

module Cvalues : sig ... end
module Clabels : sig ... end

Normalized C-labels

module CodeSemantics : sig ... end
module LogicAssigns : sig ... end
module LogicBuiltins : sig ... end
module LogicCompiler : sig ... end
module LogicSemantics : sig ... end
module LogicUsage : sig ... end
module StmtSemantics : sig ... end
module Dyncall = Frama_c_kernel.Dyncall
module Matrix : sig ... end
module NormAtLabels : sig ... end

Core Engine

module CfgAnnot : sig ... end

Normalization of Annotations.

module CfgCalculus : sig ... end
module CfgCompiler : sig ... end
module CfgDump : sig ... end
module CfgGenerator : sig ... end
module CfgInfos : sig ... end
module CfgInit : sig ... end
module CfgWP : sig ... end
module WpReached : sig ... end

Reachability for Smoke Tests

module WpPropId : sig ... end

Beside the property identification, it can be found in different contexts depending on which part of the computation is involved. For instance, properties on loops are split in 2 parts : establishment and preservation.

module WpRTE : sig ... end

Proof Engine

module Wpo : sig ... end
module Auto : sig ... end
module Cache : sig ... end
module Cleaning : sig ... end
module Letify : sig ... end
module Splitter : sig ... end
module Filtering : sig ... end

Sequent Cleaning

Prover Interface

module Why3Provers : sig ... end
module Prover : sig ... end
module ProverTask : sig ... end
module ProverWhy3 : sig ... end

Script Engine

module Script : sig ... end
module Footprint : sig ... end

Term Footprints

module ProofEngine : sig ... end

Interactive Proof Engine

module ProofScript : sig ... end
module ProverScript : sig ... end
module ProverSearch : sig ... end
module ProofSession : sig ... end
module ProofStrategy : sig ... end

Tactics

module WpTac : sig ... end

Term manipulation for Tacticals

module TacArray : sig ... end

Built-in Array Tactical (auto-registered)

module TacBitrange : sig ... end

Built-in Bit Range Tactical (auto-registered)

module TacBittest : sig ... end

Built-in Bit-Test Range Tactical (auto-registered)

module TacBitwised : sig ... end

Built-in Bitwised-Eq Tactical (auto-registered)

module TacChoice : sig ... end

Built-in Choice, Absurd & Contrapose Tactical (auto-registered)

module TacClear : sig ... end

Built-in Range Tactical (auto-registered)

module TacCompound : sig ... end

Built-in Compound Tactical (auto-registered)

module TacCongruence : sig ... end

Built-in Tactical for Product & Division Comparison (auto-registered)

module TacCut : sig ... end

Built-in Cut Tactical (auto-registered)

module TacFilter : sig ... end

Built-in Filtering Tactic (auto-registered)

module TacHavoc : sig ... end

Built-in Havoc Tactical (auto-registered)

module TacInduction : sig ... end

Built-in Range Tactical (auto-registered)

module TacInstance : sig ... end

Built-in Instance Tactical (auto-registered)

module TacLemma : sig ... end

Self registered 'Lemma' Tactical

module TacModMask : sig ... end
module TacNormalForm : sig ... end

Built-in Normal Form Tactical (auto-registered)

module TacOverflow : sig ... end

Auto registered overflow tactic

module TacRange : sig ... end

Built-in Range Tactical (auto-registered)

module TacRewrite : sig ... end

Built-in Range Tactical (auto-registered)

module TacSequence : sig ... end

Built-in Sequence Tactical (auto-registered)

module TacShift : sig ... end

Built-in Shift Tactical (auto-registered)

module TacSplit : sig ... end

Built-in Split Tactical (auto-registered)

module TacUnfold : sig ... end

Built-in Unfold Tactical (auto-registered)

module TacCompute : sig ... end

Built-in Compute Tactical (auto-registered)

Error Management

module Warning : sig ... end

Contextual Errors

module Wp_error : sig ... end

Printers and Reporting

module Plang : sig ... end

Lang Pretty-Printer

module Pcfg : sig ... end
module Pcond : sig ... end
module Ptip : sig ... end
module Rformat : sig ... end
module Stats : sig ... end
module WpReport : sig ... end

Export Statistics.

EVA Proxy

module Wp_eva : sig ... end