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