|
Installing the BOOP Toolkit (2)
|
|
Make sure that you have already installed HOL98, the
PROSPER Toolkit and the MOPED model checker! The
instructions for installing these tools can be
found here.
|
|
|
Installing GCC 3.2 and the BOOP Toolkit v0.42
|
|
The BOOP source tarball contains three directories:
|
ast |
The source code that wraps the GNU C compiler 3.2.
It contains the "Abstract Syntax Tree" module.
|
bop |
The source files for abstraction and refinment,
and the sources for interfacing to HOL98 and MOPED.
This is the main package.
|
example |
A simple example that can be used to test BOOP
after it has been installed. The example is
described in detail in the
thesis.
|
|
Unpack the BOOP source tarball into a subdirectory in
your home directory:
tar xzvf boop-0.42.tar.gz
Before you can compile the BOOP Toolkit, you need
to unpack the sources of the GNU C compiler, too.
During the build of the BOOP Toolkit a symbolic link
to the ast directory will be added to
the source tree of GCC 3.2 (in the subdirectory
gcc). The
installation guide for GCC 3.2 recommends that GCC
should not be built in its source directory!
|
|
|
Configuring the BOOP sources
|
After you have unpacked the BOOP source tarball
and the GCC 3.2 sources, you have to configure
the BOOP Makefile. Enter the bop
directory and call
configure --bindir=<binary directory>
GCCSRCDIR=<GCC sources>
GCCOBJDIR=<GCC build dir>
The paths that you specify must be absolute paths!
The binary directory is the directory where the binaries
will be installed after you have built BOOP. The GCC
sources path specifies the directory to which you have
unpacked the GCC sources. The GCC build dir specifies the
directory where GCC will be built; This directory is
created during the build if it does not exist.
|
|
|
Building the BOOP Toolkit
|
After you have configured the BOOP sources,
there should be a file called Makefile
in the bop directory. You can now
call
make
to start building the BOOP Toolkit. The build
will take a while, since the GCC sources are rather
large. If the build is successful, there should
be a file called boop in the
bop directory.
|
|
|
Installing the BOOP Toolkit
|
You can now install the BOOP binaries in
the directory you have specified by calling
make install
This installs the executables boop,
bopCallMoped.pl, and start_hol.
Add the directory where these binaries reside
to your path, since boop calls
bopCallMoped.pl and can only find
it if it is in the search path.
|
|
|
Testing and Using the BOOP Toolkit
|
|
After you have installed the BOOP Toolkit
you should test it with the toy example
that we provided. You find an explanation
of how this can be accomplished
here.
|
|
Created by Georg Weißenbacher
|
|
