ECLAIR es una herramienta comercial de análisis de código estático desarrollada por BUGSENG, LLC para el análisis, verificación, prueba y transformación automáticos de programas C y C++ .
ECLAIR es una reingeniería completa de una serie de prototipos [2] desarrollados en el Laboratorio de Métodos Formales Aplicados de la Universidad de Parma . Utiliza técnicas de análisis de código estático basadas en métodos formales , como la interpretación abstracta y la verificación de modelos, combinadas con técnicas de satisfacción de restricciones para detectar o probar la ausencia de ciertos errores de tiempo de ejecución en el código fuente , y brinda soporte para el análisis y verificación de programas, generación de pruebas de programas y transformación del programa.
Con respecto al análisis y la verificación de programas, ECLAIR puede detectar estáticamente o probar la ausencia de anomalías en el tiempo de ejecución, así como verificar automáticamente la conformidad con respecto a varios estándares de codificación, como MISRA C , MISRA C ++, CERT C Secure Coding Standard, CERT C ++ Secure Estándar de codificación, [3] C++ de alta integridad, NASA / JPL C, ESA /BSSC C/C++, JSF C++, EC--, [4] Netrino Embedded C, [5] The Power of Ten (C), [6 ] Fuerza Industrial C++. [7]
Para la prueba del programa, ECLAIR puede sintetizar automáticamente conjuntos de entradas de prueba de unidad que alcanzan un criterio de cobertura especificado por el usuario, advirtiendo al usuario cuando, debido a condiciones inviables en el programa, no se puede lograr esta cobertura.
En cuanto a la transformación de programas, ECLAIR puede utilizarse para realizar transformaciones de programas complejas: estas se especifican mediante criterios sintácticos y semánticos; las regiones del programa en la fuente que coinciden con estos criterios se pueden reemplazar opcionalmente por una sustitución parametrizada.