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.
It combines side-effect analysis and model-checking, check the website for more info: http://www.iagoabal.eu/eba/
Yes, it really does, check the website for more info: http://www.iagoabal.eu/eba/
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
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