Download WP manual - Frama-C

CHAPTER 2.
Coq:
Alt-Ergo:
Why3:
USING WP PLUG-IN
Option
Format
coq.file
altergo.file
why3.file
why3.import
[dir:]path.v
path.mlw
path.why[:name][:as]
theory[:as]
Precise meaning of formats is given by the following examples (all lenames are relatives to
the driver le's directory):
coq.file="mydir/bar.v"
Imports module
coq.file="mydir/foo:Foo.v"
why3.file="mydir/foo.why"
Imports theory
foo.Foo
foo.Bar
Imports theory
See also the default WP driver le, in
from le
mydir/foo/Foo.vo.
from directory
foo.Bar
Imports theory
Imports theory
mydir/bar.vo.
foo.Foo
Imports theory
why3.file="mydir/foo.why:Bar:T"
why3.import="foo.Bar:T"
from le
Loads coq library
why3.file="mydir/foo.why:Bar"
why3.import="foo.Bar"
Bar
mydir.
from directory
foo.Bar as T
mydir.
from directory
mydir.
with no additional includes.
foo.Bar as T
with no additional includes.
[wp-share]/wp.driver.
Optional property-tags can be given to
logic "link "
additional simplications (See section 4).
symbols to allow the WP to performs
Tags consists of an identier with column (`:'),
sometimes followed by a link (`"link ";'). The available tags are depicted on gure 2.3.
2.4 Plug-in Developer Interface
The WP plug-in has several entry points registered in the
Dynamic3
module of Frama-C.
All the entry points are documented in the Frama-C html documentation, in the Wp API
page of the plug-in section.
2.5 Proof Obligation Reports
The WP plug-in can export statistics on generated proof obligations.
These statistics are
called WP reports and are distinct from those property reports generated by the Report plugin. Actually, WP reports are statistics on proof obligations generated by WP, whereas property
reports are consolidated status of properties, generated by Frama-C kernel from various analyzers. We only discuss WP reports in this section.
Reports are generated with the following command-line options:
-wp-report <Rspec1 ,...,Rspecn >
species the list of reports to export. Each value
Rspeci
is a WP report specication le (described below).
-wp-report-basename <name>
3
See the plug-in
set the basename for exported reports (described below).
development guide
26