The BOOP Toolkit

Developed at the
Institute for Software Technology

The BOOP Toolkit
This page contains all information that you need for downloading, installing and using the BOOP Toolkit.
About BOOP
Downloading BOOP
Installing BOOP
Using BOOP
Documentation (Thesis)
Reporting problems

Links
The BOOP Toolkit was not implemented from the scratch. We utilized the tools of several other research groups. Please visit the homepages of the following projects, too:
HOL98 Theorem Prover
Moscow ML 2.0
The PROSPER Toolkit
MOPED
GCC 3.2
Microsoft SLAM project

Download tarballs
Download the tarballs that are necessary to install the BOOP Toolkit!
HOL98 Taupo 6
Moscow ML 2.01
PROSPER v1.4
MOPED
CUDD Library
SPIN model checker
GCC 3.2 sources
BOOP v0.42

SourceForge.net Logo

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