eba

EBA: un buscador de errores efectivo para C

EBA es un buscador de errores prototipo para C basado en el análisis de efectos secundarios y la verificación del modelo.

Por ahora, puede usarlo para encontrar errores de doble bloqueo en el núcleo de Linux, por ejemplo:

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

El script encontrará todos los archivos de origen C en drivers/ , llame a CPP en ellos y llame a EBA para encontrar posibles bolos dobles. Sea paciente, esto puede llevar varias horas.

Si EBA encuentra algún error potencial en path/to/file.c , escribirá las trazas de errores en _eba/path/to/file.warn :

 find _eba/ -iname '*.warn'

¿Cómo funciona?

Combina análisis de efectos secundarios y verificación de modelos, consulte el sitio web para obtener más información: http://www.iagoabal.eu/eba/

¿Realmente encuentra errores?

Sí, realmente lo hace, consulte el sitio web para obtener más información: http://www.iagoabal.eu/eba/

Instalación

Consulte las instrucciones de instalación.

Ejecutando las pruebas

Si desea ejecutar las pruebas, deberá instalar Cram , por ejemplo, usando PIP :

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

Debe colocar a EBA en algún lugar de su ruta $ :

 cram test/*.t