Note: This is the development branch for the EBA bug finder. This is a work in progress with bleeding edge feature branches. Things might break. This repository is based upon the work of Iago Abal.
For an overview of this repository and its branches, see Repositories & Branches.
EBA is a bug finder for C based on side-effect analysis and model-checking.
For now, you can use it to find double-lock and double-unlock bugs in the Linux kernel, by:
git clone --depth=1 https://github.com/torvalds/linux.git
cd linux
make allyesconfig
make $FILENAME.i
./eba {--dunlockaut ; --dlockaut ; --dlock ; --dunlock} $FILENAME.i
See --help for more options.
The --dunlockaut and --dlockaut parameters run Monitor Template-based bug checkers expressed as monitor state machines on the input. The --dlock and --dunlock parameters run pre-existing CTL-based bug checkers on the input.
For an overview of how monitor templates are implemented, see Monitor Templates.
It combines side-effect analysis and model-checking, check http://www.iagoabal.eu/eba/ and Monitor Templates for more details.
Yes, it really does, check the website for more info: http://www.iagoabal.eu/eba/
See the installation instructions.
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 place eba somewhere in your $PATH:
cram test/*.t