OSDN -- Développer et télécharger des logiciels Open Source
Traduction statut du Français translation status for fr

RSS
Télécharger la liste

Description du projet

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.

Système requise

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

Cette version apporte des améliorations dans le front-end C et dans l'analyse (analyse de débit automatique des données contextuelles), WP (vérification de propriétés fonctionnelles, à l'aide de la logique de Hoare), tranchage (génération de programmes C compilables simplifiées) et 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

Cette nouvelle version majeure comprend beaucoup de corrections de bogues et d'améliorations. Améliorations de performances bénéficient les plug-ins d'analyse de la valeur et le tranchage, le Aoraï plug-in pour la vérification de programmes c contre les formules logique temporelle linéaire, le GUI et de statuts de propriété du noyau de plug-in collaboration.
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

Cette version corrige des bugs identifiés dans la version bêta 20101202 et rend l'API externe stable pour les développeurs de plug-in. Analyse de la valeur aux utilisateurs, envisager d'appliquer ce patch avant la compilation: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2011-February/002527.html. Jessie utilisateurs: cette version est compatible avec Pourquoi 2.29, disponible auprès de http://why.lri.fr/. utilisateurs WP: le plug-in WP sera mis à disposition séparément plus tard.
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

Beaucoup de corrections de bugs. Petite amélioration de la convivialité de l'interface graphique. Quelques changements API. Analyse de la Valeur: amélioration de la vitesse et la consommation de mémoire; poignée de type simple précision float en tant que telle (au lieu de l'amalgame avec le double comme précédemment), une meilleure gestion des structs passés comme arguments à des fonctions. Un nouveau plug-in de vérification déductive: 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

Le support pour le langage de spécification ACSL a été l'amélioration du cadre à l'échelle. L'analyse de la valeur des prestations de nombreuses options nouvelles pour améliorer la précision et l'échelle à une plus grande bases de code.
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

Page d'accueil Project Page