Download List

Descripción del Proyecto

Frama-C is a suite of tools dedicated to the analysis of the source code of software written in C. Frama-C gathers several static analysis techniques in a single collaborative framework. The collaborative approach allows static analyzers to build upon the results already computed by other analyzers in the framework. It provides sophisticated tools, such as a slicer and dependency analysis.

System Requirements

System requirement is not defined
Information regarding Project Releases and Project Resources. Note that the information here is a quote from Freecode.com page, and the downloads themselves may not be hosted on OSDN.

2012-10-05 06:45
20120901 Oxygen

Esta versión trae mejoras en el front-end C y en el análisis de valor (análisis de flujo de datos contextuales automáticos), WP (verificación de propiedades funcionales utilizando la lógica de Hoare), corte (generación de programas C compilable simplificados) y plug-ins.
This release brings improvements in the C front-end and in the value analysis (automatic context-sensitive data flow analysis), WP (verification of functional properties using Hoare logic), slicing (generation of simplified, compilable C programs), and plug-ins.

2011-10-11 06:02
Nitrogen 20111001

Esta nueva versión incluye muchas mejoras y correcciones de errores. Mejoras de rendimiento beneficiarán el análisis de valor y consumo plug-ins, el plug-in para la verificación de programas c contra las fórmulas lineal Temporal Logic Aoraï, GUI y estatus de propiedad del núcleo de colaboración plug-in.
This new major version includes many bugfixes and improvements. Performance improvements benefit the Value Analysis and Slicing plug-ins, the Aoraï plug-in for verification of C programs against Linear Temporal Logic formulas, the GUI, and kernel property statuses for plug-in collaboration.

2011-03-05 06:52
Carbon 20110201

Esta versión corrige los errores identificados en la versión beta 20101202 y hace que la API externa estable para los desarrolladores de plug-in. usuarios Valor análisis, considerar la aplicación de este parche antes de compilar: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2011-February/002527.html. Jessie usuarios: esta versión es compatible con 2.29 ¿Por qué, disponible en http://why.lri.fr/. WP usuarios: el Grupo de trabajo plug-in estará disponible por separado más adelante.
Tags: Stable
This release fixes bugs identified in beta version 20101202 and makes the API stable for external plug-in developers. Value analysis users, consider applying this patch before compiling: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2011-February/002527.html . Jessie users: this release is compatible with Why 2.29, available from http://why.lri.fr/ . WP users: the WP plug-in will be made available separately later.

2011-01-06 07:34
20101202

Muchas correcciones de errores. Pequeñas mejoras de usabilidad para la interfaz gráfica de usuario. Algunos cambios en el API. El análisis de valor: mejorar la velocidad y el consumo de memoria; mango tipo flotante de precisión simple como tales (en lugar de agrupar con doble como antes), un mejor manejo de las estructuras pasan como argumentos a funciones. Un nuevo plug-deductivo de verificación en: WP.
Tags: Beta
Many bugfixes. Small usability improvements to the GUI.
A few API changes. Value analysis: improved speed and memory consumption; handle single-precision type float as such (instead of lumping it with double as previously); better handling of structs passed as arguments to functions. A new deductive verification plug-in: WP.

2010-04-13 22:31
20100401

El soporte para el lenguaje de especificación ACSL se ha mejorado en todo el marco. El análisis de valor se beneficia de numerosas nuevas opciones para mejorar la precisión y la escala a las grandes bases de código.
The support for the ACSL specification language was improved framework-wide. The value analysis benefits from numerous new options to improve precision and scale to larger codebases.

Project Resources