Frama-C API - `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 MemRegion : 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 Region : sig ... end

module Layout : sig ... end

Region Utilities

module RegionAccess : sig ... end

module RegionAnalysis : sig ... end

module RegionAnnot : sig ... end

module RegionDump : sig ... end

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 Filter_axioms : 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

Frama-C API - Wp

High-Level External API

Advanced Usage API

Low-Level Internal API

Model Registration

Memory Models

Other Models

State Model

Model Hypotheses

Region Analysis

Compilers

Core Engine

Proof Engine

Prover Interface

Script Engine

Tactics

Error Management

Printers and Reporting

EVA Proxy

Frama-C API - `Wp`