eba

EBA: un bogue efficace pour C

L'EBA est un prototype de bogue pour C basé sur l'analyse à effets secondaires et la vérification du modèle.

Pour l'instant, vous pouvez l'utiliser pour trouver des bugs doubles dans le noyau Linux, par exemple:

 git clone --depth=1 https://github.com/torvalds/linux.git
cd linux
make allyesconfig
scripts/eba-linux.sh drivers/net

Le script trouvera tous les fichiers source C sous drivers/ , appelez CPP sur eux et appelez EBA pour trouver des doubles verrouillables potentiels. Soyez patient, cela peut prendre plusieurs heures.

Si l'EBA trouve un bug potentiel dans path/to/file.c , il écrira les traces de bogue dans _eba/path/to/file.warn :

 find _eba/ -iname '*.warn'

Comment ça marche?

Il combine l'analyse et la vérification du modèle, consultez le site Web pour plus d'informations: http://www.iagoabal.eu/eba/

Est-ce que cela trouve vraiment des bugs?

Oui, c'est vraiment le cas, consultez le site Web pour plus d'informations: http://www.iagoabal.eu/eba/

Installation

Voir les instructions d'installation.

Exécuter les tests

Si vous souhaitez exécuter les tests, vous devrez installer Cram , par exemple en utilisant PIP :

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

Vous devez placer l'EBA quelque part dans votre $ PATH :

 cram test/*.t