Frama C snapshot

Frama-C es una plataforma dedicada al análisis del código fuente escrito en C.

Nota: ¡El repositorio oficial de Frama-C está ahora en nuestro Gitlab!

Frama-C ha trasladado su repositorio oficial a nuestra instancia de Gitlab autohospedada.

Los lanzamientos oficiales (a partir de Frama-C 21) ya no se actualizarán aquí.

¡Las instantáneas nocturnas también están disponibles en nuestro gitlab! Ahora puede obtener acceso a la última versión de desarrollo en: https://git.frama-c.com/pub/frama-c/-/tree/master

El rastreador oficial de problemas de Frama-C ahora está en nuestro Gitlab: https://git.frama-c.com/pub/frama-c/-/issues

Puede enviar problemas y extraer solicitudes utilizando su inicio de sesión de GitHub (elija "Iniciar sesión con GitHub" cuando se le solicite).

¡Nos vemos allí!

Una plataforma de colaboración

Frama-C reúne varias técnicas de análisis en una sola plataforma de colaboración, que consiste en un núcleo que proporciona un conjunto central de características (por ejemplo, un AST para programas C normalizado) más un conjunto de analizadores, llamado complementos . Los complementos pueden basarse en resultados calculados por otros complementos en la plataforma.

Gracias a este enfoque, Frama-C proporciona herramientas sofisticadas, que incluyen:

• un analizador basado en la interpretación abstracta, dirigido a verificar la ausencia de errores de tiempo de ejecución ( EVA );
• un marco a prueba de programa basado en el cálculo de condición previa más débil ( WP );
• una cortadora de programa ( corte );
• una herramienta para la verificación de propiedades temporales (LTL) ( Aorain );
• una herramienta de verificación de tiempo de ejecución ( E-ACSL );
• Varias herramientas para el análisis de exploración y dependencia de la base de código ( de , impacto , métricas , ocurrencia , alcance , etc.).

Estos complementos comparten un lenguaje común y pueden intercambiar información a través de propiedades ACSL ( lenguaje de especificación ANSI/ISO C ). Los complementos también pueden colaborar a través de sus API.

Instalación

Para obtener información más detallada sobre la instalación de OPAM/FRAMA-C, consulte Install.md.

Frama-C está disponible a través de OPAM, el Manager de paquetes OCAML. Este es el método de instalación preferido. Asegúrese de instalar OPAM v2.0 o superior. Luego, la siguiente secuencia de comandos debe instalar Frama-C y su GUI:

 opam init
opam install depext
opam depext frama-c
opam install frama-c

Frama-C se desarrolla principalmente en Linux, a menudo probado en macOS (a través de Homebrew), y ocasionalmente se prueba en Windows (a través del subsistema de Windows para Linux).

Uso

Frama-C se puede ejecutar desde la línea de comandos o a través de su interfaz gráfica.

Uso simple

El uso recomendado para archivos simples es una de las siguientes líneas:

 frama-c file.c -<plugin> [options]
frama-c-gui file.c

Donde -<plugin> es uno de los varios complementos Frama -C, EG -eva , o -wp , o -metrics , etc. Los complementos también se pueden ejecutar directamente desde la GUI.

Para enumerar todos los complementos, ejecute:

 frama-c -plugins

Cada complemento tiene un comando de ayuda ( -<plugin>-help o- -<plugin>-h ) que describe sus varias opciones.

Finalmente, la lista de opciones que rigen el comportamiento del kernel de Frama-C está disponible a través de

 frama-c -kernel-help

Escenarios complejos

Para escenarios de uso más complejos (muchos archivos y directorios, con varias directivas de preprocesamiento), recomendamos dividir el uso de Frama-C en dos partes:

1. Analizar los archivos de entrada y guardar el resultado en un archivo;
2. Cargando los resultados del análisis y luego ejecutando los análisis o la GUI.

El análisis generalmente implica dar argumentos adicionales al preprocesador C, por lo que la opción -cpp-extra-args es a menudo útil, como en el ejemplo a continuación:

 frama-c *.c *.h -cpp-extra-args="-D<define> -I<include>" -save parsed.sav

Los resultados se cargan en Frama-C para análisis adicionales o para inspección a través de la GUI:

 frama-c -load parsed.sav -<plugin> [options]
frama-c-gui -load parsed.sav -<plugin> [options]

Referencia adicional

• Los enlaces a los manuales de usuarios y desarrolladores, los archivos frama-C y los manuales de complemento están disponibles en
  http://frama-c.com/download.html

• Stackoverflow tiene varias preguntas con la etiqueta frama-c , que es monitoreada por varios miembros de la comunidad Frama-C.

• La lista de correo de frama-c-discuss se utiliza para anuncios y discusiones generales.

• El sistema oficial de seguimiento de errores se puede utilizar para informes de errores.

• El Wiki Frama-C tiene información útil, aunque no está completamente actualizado.

• El blog de Frama-C tiene varias publicaciones sobre nuevos desarrollos de Frama-C, así como discusiones generales sobre el lenguaje C, el comportamiento indefinido, los cálculos de punto flotante, etc.

• El repositorio de instantáneas de GitHub contiene los archivos .tar.gz de lanzamientos de frama-C estables, listos para ser clonados. También se puede utilizar para informar problemas y enviar solicitudes de extracción.