CProver Wiki

About

JBMC is a Bounded Model Checker for Java programs. It supports checking for runtime exceptions and user-definde assertions. The verification is performed by unwinding the loops in the program and passing the resulting equation to a decision procedure.

Versions

Get the latest release

• Releases are tested and for production use.

Get the current develop version: git clone https://github.com/diffblue/jbmc.git

• Develop versions are not recommended for production use.

Prerequisites

JBMC compiles CBMC as part of its build process and as such has all the pre-requisites of CBMC. These can be viewed at: diffblue/cbmc:COMPILING

Compilation

To compile you need to run two commands:

make -C src setup-cbmc
make -C src CXXFLAGS="-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare"

The first make command will configure the CBMC submodule (found in lib/cbmc). It can optionally be provided with a list of users forks to retrieve. This is needed if changes depend on a commit that has not yet been merged into diffblue/cbmc.

For example, if you need userA and userB's forks the first command would be:

make -C src USERS="userA userB" setup-cbmc

It is recommend to add your fork in this way.

Output

Compiling produces an executable called symex which by default can be found in src/jbmc/jbmc

Report bugs

If you encounter a problem please file a bug report:

• Create an issue

Contributing to the code base

1. Fork the repository
2. Clone the repository git clone git@github.com:YOURNAME/jbmc.git
3. Create a branch from the develop branch (default branch)
4. Make your changes (follow the coding guidelines)
5. Push your changes to your branch
6. Create a Pull Request targeting the develop branch

License

4-clause BSD license, see LICENSE file.