Skip to content
This repository has been archived by the owner on Oct 22, 2021. It is now read-only.

wasowski/eba-development

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

EBA: An Effective Bug Finder for C

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.

Hows does it work?

It combines side-effect analysis and model-checking, check http://www.iagoabal.eu/eba/ and Monitor Templates for more details.

Does it really find bugs?

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

Installation

See the installation instructions.

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 place eba somewhere in your $PATH:

cram test/*.t

About

EBA is a static bug finder for C.

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • SWIG 98.5%
  • OCaml 1.3%
  • C 0.2%
  • Shell 0.0%
  • Perl 0.0%
  • Python 0.0%