Module WpSource

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.

Sourcemodule VC : sig ... end

WP Proof Obligation Generator and Management

Sourcemodule VCS : sig ... end

Provers and Proof Obligations Results

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

Sourcemodule Repr : sig ... end

High-Level Term Representation

Sourcemodule Lang : sig ... end

Low-Level Logic Terms and Predicates

Sourcemodule Definitions : sig ... end

Generated Logic Definitions

Sourcemodule Conditions : sig ... end

Proof Task and Simplifiers

Sourcemodule Tactical : sig ... end

Tactics Entry Points

Sourcemodule Strategy : sig ... end

Strategies Entry Points

Sourcemodule Generator : sig ... end

WP Proof Obligation Generator

Sourcemodule 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

Sourcemodule Factory : sig ... end
Sourcemodule WpContext : sig ... end

Model Registration

Memory Models

Sourcemodule MemDebug : sig ... end
Sourcemodule MemEmpty : sig ... end
Sourcemodule MemLoader : sig ... end

Compound Loader

Sourcemodule MemMemory : sig ... end
Sourcemodule MemRegion : sig ... end
Sourcemodule MemTyped : sig ... end
Sourcemodule MemVal : sig ... end
Sourcemodule MemVar : sig ... end
Sourcemodule MemZeroAlias : sig ... end

Other Models

Sourcemodule Cint : sig ... end

Integer Arithmetic Model

Sourcemodule Cfloat : sig ... end

Floating Arithmetic Model

Sourcemodule Cmath : sig ... end

Math Operators

Sourcemodule Cstring : sig ... end

State Model

Sourcemodule Sigma : sig ... end
Sourcemodule Passive : sig ... end

Passive Forms

Sourcemodule Mstate : sig ... end

Model Hypotheses

Sourcemodule MemoryContext : sig ... end
Sourcemodule RefUsage : sig ... end
Sourcemodule WpTarget : sig ... end

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

Sourcemodule 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

Sourcemodule Region : sig ... end
Sourcemodule Layout : sig ... end

Region Utilities

Sourcemodule RegionAccess : sig ... end
Sourcemodule RegionAnalysis : sig ... end
Sourcemodule RegionAnnot : sig ... end
Sourcemodule RegionDump : sig ... end

Compilers

Sourcemodule Sigs : sig ... end

Common Types and Signatures

Sourcemodule Driver : sig ... end
Sourcemodule Context : sig ... end

Current Loc

Sourcemodule Ctypes : sig ... end

C-Types

Sourcemodule Cvalues : sig ... end
Sourcemodule Clabels : sig ... end

Normalized C-labels

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

Core Engine

Sourcemodule CfgAnnot : sig ... end

Normalization of Annotations.

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

Reachability for Smoke Tests

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

Sourcemodule WpRTE : sig ... end

Proof Engine

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

Sequent Cleaning

Prover Interface

Sourcemodule Why3Provers : sig ... end
Sourcemodule Filter_axioms : sig ... end
Sourcemodule Prover : sig ... end
Sourcemodule ProverTask : sig ... end
Sourcemodule ProverWhy3 : sig ... end

Script Engine

Sourcemodule Script : sig ... end
Sourcemodule Footprint : sig ... end

Term Footprints

Sourcemodule ProofEngine : sig ... end

Interactive Proof Engine

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

Tactics

Sourcemodule WpTac : sig ... end

Term manipulation for Tacticals

Sourcemodule TacArray : sig ... end

Built-in Array Tactical (auto-registered)

Sourcemodule TacBitrange : sig ... end

Built-in Bit Range Tactical (auto-registered)

Sourcemodule TacBittest : sig ... end

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

Sourcemodule TacBitwised : sig ... end

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

Sourcemodule TacChoice : sig ... end

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

Sourcemodule TacClear : sig ... end

Built-in Range Tactical (auto-registered)

Sourcemodule TacCompound : sig ... end

Built-in Compound Tactical (auto-registered)

Sourcemodule TacCongruence : sig ... end

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

Sourcemodule TacCut : sig ... end

Built-in Cut Tactical (auto-registered)

Sourcemodule TacFilter : sig ... end

Built-in Filtering Tactic (auto-registered)

Sourcemodule TacHavoc : sig ... end

Built-in Havoc Tactical (auto-registered)

Sourcemodule TacInduction : sig ... end

Built-in Range Tactical (auto-registered)

Sourcemodule TacInstance : sig ... end

Built-in Instance Tactical (auto-registered)

Sourcemodule TacLemma : sig ... end

Self registered 'Lemma' Tactical

Sourcemodule TacModMask : sig ... end
Sourcemodule TacNormalForm : sig ... end

Built-in Normal Form Tactical (auto-registered)

Sourcemodule TacOverflow : sig ... end

Auto registered overflow tactic

Sourcemodule TacRange : sig ... end

Built-in Range Tactical (auto-registered)

Sourcemodule TacRewrite : sig ... end

Built-in Range Tactical (auto-registered)

Sourcemodule TacSequence : sig ... end

Built-in Sequence Tactical (auto-registered)

Sourcemodule TacShift : sig ... end

Built-in Shift Tactical (auto-registered)

Sourcemodule TacSplit : sig ... end

Built-in Split Tactical (auto-registered)

Sourcemodule TacUnfold : sig ... end

Built-in Unfold Tactical (auto-registered)

Sourcemodule TacCompute : sig ... end

Built-in Compute Tactical (auto-registered)

Error Management

Sourcemodule Warning : sig ... end

Contextual Errors

Sourcemodule Wp_error : sig ... end

Printers and Reporting

Sourcemodule Plang : sig ... end

Lang Pretty-Printer

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

Export Statistics.

EVA Proxy

Sourcemodule Wp_eva : sig ... end