|
Reporting Problems with BOOP
|
If you use the BOOP Toolkit on other programs
than the example we provided, you will sooner
or later reveal some bugs. Unfortunately,
BOOP is no longer maintained anymore, and we
cannot provide any support for it. There is a
(now inactive) mailing list
boop-info.
|
|
Most problems will result from the fact that BOOP
does only support a subset of the C programming language.
C programs that can be inspected with the BOOP Toolkit
must adhere to following restrictions:
|
|
Expressions |
Expressions must be free of side effects. Furthermore,
we support only a subset of the C operations. Most notably,
all bit manipulation operations except shift left and
shift right are not supported. Furthermore, most of
the type casts are not supported. A detailed enumeration
of the supported operations can be found in the thesis.
|
|
Functions |
BOOP cannot process programs with external functions
(the function assert is an exception,
it must be defined to be external). Furthermore,
function calls must not occur within expressions.
This means that function calls can occur either
on the right hand side of an assignment, or
as an independent statement. Furthermore, functions
with a variable number of parameters are not supported.
|
|
Pointers |
Due to the lack of a pointer analysis we do not
yet support programs with pointers.
|
|
Control constructs |
Some control constructs are not supported:
for-loops, goto,
switch/case, break,
and continue.
|
If you specify more than one source file, the files
will be concatenated with help of the -include
option of the GNU C compiler. This may lead to problems,
so try to compile the program you want to test with
GCC first (using this option). Furthermore, the standard
include files will probably not work, since most of
the functions specified there are located in external libraries.
|
|
|
Internals of BOOP
|
BOOP consists of two modules:
- AST: The sources for the AST module are
located in the
ast directory of the distribution.
It contains the wrapping code for the GNU C compiler.
The functions in astWrapper.c extract the
internal syntax tree of the GNU C
compiler with help of a backend-hook that we added to GCC 3.2.
To insert the backend-hook the sources of GCC must be patched,
the patch is contained in the file astGccPatch.diff.
Basically we reinsert a backend hook that existed in version 3.1 of GCC
and was removed in version 3.2.
The remaining files in the ast
directory are the types for the nodes of the abstract
syntax tree that BOOP uses.
- BOP:The
bop directory contains the files
that contain the abstraction functions, the functions that are
used to call the theorem prover and the functions for the feasibility check.
bopTrans.c contains the functions that translate
a C program to a boolean program.
bopProver.c contains the functions that
translate C expressions to HOL and call the theorem prover via the
PROSPER PII interface.
The functions in bopPath.c are used to call
MOPED and to extract a path from the output of the model checker.
bopFeasable.c (note the typo ;-)) contains the
functions that check the feasibility of this path and calculate
a new set of predicates for the next abstraction.
boop.c contains the main function, which
controls the abstraction/refinement cycle.
|
BOOP is linked agains the libraries libpii.a (the
PROSPER integration interface library), libiberty.a
(the portable GNU library that comes with GCC), and libast.a
(which contains the GNU C compiler library).
|
|
|
Created by Georg Weißenbacher
|
|
