EBA: An effective bug finder for C

EBA is a prototype bug finder for C based on side-effect analysis and model-checking.

For now, you can use it to find double-lock bugs in the Linux kernel. In order to check path/to/file.c do:

make path/to/file.i    # EBA runs on single preprocessed files !
eba -L path/to/file.i

There are some options you can use:

eba --help

In the bin folder there are some scripts to run EBA along with the build process.

Hows does it work?

It combines side-effect analysis and model-checking, check the website for more info: http://www.iagoabal.eu/eba/

Does it really find bugs?

Yes, it really does, check the website for more info: http://www.iagoabal.eu/eba/

Installation

You will need OCaml 4.01 (see cil-project/cil#18), preferrably just install OPAM.

Download the source code.

Install omake if necessary.

sudo apt-get install omake

Install dependencies

opam install batteries cil smart-print cmdliner dolog ocamlgraph

Invoke omake (you build in parallel using -j):

omake

Running the tests

If you want to run the tests you will need to install cram, for instance using pip:

sudo apt-get install python-pip
sudo pip install cram

You should rename eba.opt to eba and move it somewhere in your $PATH, otherwise create a symlink.

Finally,

omake test