package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-wp.core/Wp/index.html

Module `Wp`Source

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

Contextual Values

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

On This Page

High-Level External API
Advanced Usage API
Low-Level Internal API

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/index.html

Module WpSource

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

Module `Wp`Source