|
Using the BOOP Toolkit
|
After you have installed
the BOOP Toolkit you are ready to use it. We provided
a toy example (which is described in detail in
the thesis).
This example can be found in the example
directory of the BOOP distribution.
|
The executable boop can be called with
following parameters:
|
--reachable or -r |
Used to specify the name of the label
|
--verbose |
Increases the verbosity of BOOP: The report of the erroneous path
contains more details and the theorem prover shows the expressions
that it tries to decide.
|
--prosper-host |
Specifies the name of the host where the HOL98 theorem prover is
running.
|
--prosper-port |
Specifies the number of the port on which the PROSPER Toolkit
is listening.
|
--report |
Specify a file to which the counter example should be reported.
If this parameter is missing, the counter example will be
reported to stdout.
|
--iterations |
Specify a maximal number of interations.
|
|
|
Testing BOOP with an example program
|
You find an example program in the example
directory of the BOOP distribution. The example is
described in detail in the 3rd chapter of the
master's thesis. |
|
The code contains a few functions
of a Linux device driver module. Linux device drivers
are loaded and unloaded dynamically. The driver maintains
a usage count, and it must not be released unless this
count equals to zero. |
|
We modified the interface functions
so that the label ERROR is reachable if the driver
is unloaded though the usage count is greater than zero.
|
Before you call boop, you
must start the HOL98 theorem prover. You
can do this by calling
start_hol &
Then, call boop with following
parameters:
boop -r ERROR example/spec.c example/driver.c
If everything works, BOOP should report that ERROR
is reachable. BOOP writes the intermediate abstractions
to the actual directory, so you should find a number
of files called abs<n>.[bp|exp].
On failure, it is a good idea to inspect these files.
|
BOOP provides a detailed explanation of how ERROR
can be reached. If you edit the file driver.c,
delete the line MOD_INC_USE_COUNT; and add
it again after the instruction locked = TRUE;
then ERROR should be unreachable.
|
|
|
Created by Georg Weißenbacher
|
|
