When invoked with the command-line:
frama-c -eva -eva-precision 1 first.c
Frama-C creates an analysis project for the file first.c.
The -eva option on the command-line causes the Eva plug-in to run and have its results ready before the interface appears.
The -eva-precision option is one of several options that influence the precision of the Eva plug-in. The actions of creating new analysis projects and activating plug-ins can also be done interactively.
The Eva plug-in computes sets of possible values for every variable at each point of the program. When providing such results, Frama-C guarantees that the variable does not take at that point any value other than those listed.
When the execution reaches this point inside the loop, the variable S always contains either 0, 1, 3, or 6.
For each statement, Frama-C can provide an exhaustive list of the memory cells that may be modified by this statement during the execution, even if the statement uses pointers.
Frama-C guarantees that anytime it is executed, the statement *tmp = S; does not change any memory location other than the cells of the array T.
The dependencies plug-in makes use of the results of the value analysis plug-in to highlight the statements that define the value of variable S at the selected program point.
The value contained in variable S at the statement *tmp = S; was defined by the statement S += i;.
This analysis highlights in green all the statements impacted by the selected statement.
The statement p = T; has repercussions on the statements tmp = p; p++; *tmp = S;.
It is guaranteed not to affect the statements S += i; and i ++;.
Frama-C 10.0 (Neon) is available.
This new major version includes too many bug fixes and improvements to list here: details are available at http://frama-c.com/Changelog.html.
The main highlights are: - The Value plugin is more efficient (computation and cache have been optimized). The experimental option -val-show-perf helps estimating which part of the C code takes time to analyze. One can send SIGUSR1 signal to a Frama-C process for stopping and saving the partial results of the Value plugin. - The From plugin computes separately data dependencies and indirect (address, control) dependencies with option -show-indirect-deps - The axiomatizations used by the WP plugin are now shared between the different prover outputs and mainly realized in Coq thanks to a better integration with Why3.
For plug-in developers: - The api for Dataflow have been greatly simplified. - This major release changes several Frama-C APIs in an incompatible way. Some of the plugin-side changes can be automatically applied by using the script bin/fluorine2neon.sh of the source distribution. Complex plug-ins should be reviewed for compatibility.
Frama-C 11.0 (Sodium) is available.
This new major version includes too many bug fixes and improvements to list here: details are available at http://frama-c.com/Changelog.html.
The main highlights are: - kernel: Frama-C standard library is included by default (-no-frama-c-stdlib for the previous behavior) - kernel: When preprocessor supports it, expansions of macros in annotations (-pp-annot) is now done by default. Efficiency of -pp-annot has been greatly improved. - kernel: the default machdep no longer assumes the compiler is gcc. See ‘frama-c -machdep help’ - Homogenization of collections options (eg: -cpp-extra-args, -slevel-function) - value: much-improved pretty-printing of pointer abstract values - value: logic ranges are now evaluated using a dedicated domain, resulting in faster analysis and more precise results - value: the parameters of a function call may be reduced if they are constrained by the callee - kernel, value: support for predicate - kernel, value, WP: support for const variables - rte, value: alarms are now emitted for casts from floating-point to integer that overflow - from: assigns/from acsl clauses of functions with a body can now be verified through option -from-verify-assigns - from: major performance improvements on large input programs. - semantic constant folding: better propagation on pointer variables
For plug-in developers: - New API for collections options - New AST nodes Throw and TryCatch for dealing with exception. The C front-end does not generate any such node. A code transformation can compile such nodes away if needed (see src/kernel/exn_flow.mli for more information).
Frama-C 12.0 (Magnesium) is available.
This new major version includes too many bug fixes and improvements to list here: details are available at http://frama-c.com/Changelog.html.
The main highlights are: - value: brand new GUI, found in the “Values” tab - value: new builtins for floating-point functions of the standard library - value: more fine-grained control on the value of padding after initialisation - value: multiple improvements to option -subdivide-float-var - wp: many improvements for user experience (see Changelog) - wp: many new or improved simplifications in Qed (see Changelog) - wp: support for global const (see -wp-init-const option) - wp: refined memory access and compound encoding - wp: new memory model ‘Caveat’ for unit-proofs - wp: new (less precise) integer model ‘rg’ to simplify integral ranges - wp: more ACSL builtins (, _NaN, _finite, _infinite, _plus_infinity, _minus_infinity) - report: new report in .csv format
Frama-C 13.0 (Aluminium) is available.
This major version fixes many bugs and includes improvements and three new plug-ins.
The main highlights are: - variadic: new plug-in which translates variadic functions, calls and macros to allow analyses to handle them more easily. - loop: new plug-in which estimates loop bounds and -slevel-function parameters. - nonterm: new plug-in for detection of definite non-termination based on Value. - value: major reimplementation of large parts of the plugin. New analysis domains are available (see options -eva-equality-domain and -eva-bitwise-domain), and the analysis of conditionals has been improved. ‘direct’ and ‘indirect’ annotations are now used to evaluate assigns clauses. Better propagation strategy for nested loops and changes in the widening strategy for frontiers of integer types. - cil: various improvements to the handling of empty structs, zero-length arrays, and flexible array members. - kernel: automatic generation of assigns from GCC’s extended asm. - ACSL: new predicate _function, requiring the compatibility between the type of the pointer and the function being pointed (currently supported by Value), notation { x, y, z } for defining sets and built-in operators for lists (currently supported by WP).
The first version of the Frama-Clang plugin, an experimental C++ front-end for Frama-C, is available.
Frama-C 14.0 (Silicon) is available.
Main changes are:
Kernel: - refactoring of ACSL extensions + allow extensions in loop annotations - rename multiple types of the logic AST for more coherence
Libc: - The implementations of some functions of the standard library are now available in share/libc/*.c. The .c and .h files in share/libc are deprecated.
Eva/Value plugin: - two now (experimental) analysis domains are available. Gauges infer affine relations between variables in loops. Symbolic locations keep track of the contents of l-values such as *p or t[i]. - new builtins are available for dynamic allocation, and some functions of string.h and. Default builtins can be activated through option -val-builtins-auto.
WP plugin: - unified variable usage for all models - WP now honors the kernel option -warn-(signed|unsigned)-(overflow|downcast). The cint and cfloat are used by default
Rte plugin: - new option -rte-pointer-call, to generate annotations for calls through function pointers.
Nonterm plugin: - overall increase in precision, especially on compound statements (if, switch, loops…).
Changes in the compilation process: - OCamlGraph is no longer packaged within Frama-C, and must be installed to build Frama-C from source. - OCaml version greater or equal than 4.02.3 required..
A complete changelog can be found here.
Version 0.8 of the E-ACSL plugin is available.
Version 0.0.2 of the Frama-Clang plugin is available for download.
Frama-C 15.0 (Phosphorus) is out. Download it here.
Main changes with respect to Frama-C 14 - Silicon include:
-wp-invariants
) has been droppedA complete changelog can be found here.
Frama-Clang 0.0.3, compatible with Frama-C 15, is out. Download it here.
Frama-C 16.0 (Sulfur) is out. Download it here.
Main changes with respect to Frama-C 15 - Phosphorus include:
A complete changelog can be found here.
Frama-Clang 0.0.4, compatible with Frama-C 16, is out. Download it here.
Frama-Clang 0.0.5, fixing compatibility issue with Debian/Ubuntu, is out. Download it here.
Frama-C 17.0 (Chlorine) is out. Download it here.
Main changes with respect to Frama-C 16 - Sulfur include:
A complete changelog can be found here.
Frama-Clang 0.0.6, compatible with Frama-C 17 Chlorine, is out. Download it here.
Frama-C 18.0 (Argon) is out. Download it here.
Main changes with respect to Frama-C 17 (Chlorine) include:
A complete Changelog can be found here.
Frama-C & SPARK Day 2019 will take place on June 3, 2019 in Paris. Registration and program here.
Frama-C 19.0 (Potassium) is out. Download it here.
Main changes with respect to Frama-C 18 (Argon) include:
A complete changelog can be found here.
Frama-Clang 0.0.7 is out. Download it here.
Frama-C 19.1 (Potassium) is out. Download it here.
This minor release merely restores compatibility with OCaml 4.08.1 (and the new 4.09.0), and fixes a few issues with lablgtk3.
Frama-C 20.0 (Calcium) is out. Download it here.
Main changes with respect to Frama-C 19 (Potassium) include:
And a new plug-in, Markdown-report (MdR), to generate reports in both Markdown and SARIF formats.
A complete changelog can be found here.
Frama-Clang 0.0.8 is out. Download it here.
Frama-C 21.0 (Scandium) is out. Download it here.
Main changes with respect to Frama-C 20 (Calcium) include:
-warn-invalid-pointer
(disabled by default; warns on pointer arithmetic resulting in invalid values)-warn-pointer-downcast
(enabled by default; warns when a pointer/integer conversion may lead to loss of precision)-eva-domains
to enable a list of analysis domains (replacing the former options -eva-name-domain). -eva-domains help
prints the list of available domains with a short description-eva-domains-function
to enable domains only on given functions-warn-invalid-pointers
is enabled, emits alarms on invalid pointer arithmetics resulting in a pointer that does not point inside an object or one past an object (even if the pointer is not used afterward)-eva-subdivide-non-linear-function
/*@ subdivide N; */
annotations.-wp-smoke-tests
option in WP manual)And a new plug-in, Instantiate, to generate function specializations e.g. for functions with void*
(memcpy
/memset
/etc), to help other plugins such as WP.
A complete changelog can be found here.
Frama-C 21.1 (Scandium) is out. Download it here.
This minor release fixes a few issues in WP.
Frama-Clang 0.0.9 is out. Download it here.
Frama-C 22.0-beta (Titanium) is out. Download it here.
Main changes with respect to Frama-C 21 (Scandium) include:
\from
now accepts &v
expressions-print-config-json
, to output Frama-C configuration data in JSON format-explain
, which provides help messages for options used on the command line-print-cpp-commands
, to print the preprocessing commands used by Frama-C_Noreturn
and _Thread_local
specifiers\separated
complete
and disjoint
behaviors-eva-alloc-builtin
to configure uniformly their behavior (instead of mapping each malloc
/calloc
/realloc
function to the corresponding builtin), and new annotation eva_allocate
to locally override the global optionacos
, asin
and atan
(and their single-precision version acosf
, asinf
, atanf
)-eva-auto-loop-unroll
option) on loops with several exit conditions, conditions using equality operators, temporary variables introduced by the Frama-C normalization or goto
statements\initialized
ACSL predicate-wp-check-memory-model
to automatically check memory model hypothesespedantic-assigns
. WP needs precise assigns ... \from ...
specification about out pointers to generate precise proof hypothesesA complete changelog can be found here.
Frama-C 22.0 (Titanium) is out. Download it here.
Main changes with respect to Frama-C 21 (Scandium) include:
\from
now accepts &v
expressions-print-config-json
, to output Frama-C configuration data in JSON format-explain
, which provides help messages for options used on the command line-print-cpp-commands
, to print the preprocessing commands used by Frama-C_Noreturn
and _Thread_local
specifiers\separated
complete
and disjoint
behaviors-eva-alloc-builtin
to configure uniformly their behavior (instead of mapping each malloc
/calloc
/realloc
function to the corresponding builtin), and new annotation eva_allocate
to locally override the global optionacos
, asin
and atan
(and their single-precision version acosf
, asinf
, atanf
)-eva-auto-loop-unroll
option) on loops with several exit conditions, conditions using equality operators, temporary variables introduced by the Frama-C normalization or goto
statements\initialized
ACSL predicate-wp-check-memory-model
to automatically check memory model hypothesespedantic-assigns
. WP needs precise assigns ... \from ...
specification about out pointers to generate precise proof hypothesesA complete changelog can be found here.
Following the release of Frama-C 22.0 (Titanium), MetAcsl v0.1 is out and ready to be installed via opam install frama-c-metacsl
.
MetAcsl intends to provide simple and compact ways to express properties that would demand peppering the code with thousands of annotations in plain ACSL. Its main use cases focus on security properties (notably ensuring that write and read accesses to sensitive memory locations are guarded appropriately). Feel free to consult its homepage for more information.
Frama-Clang 0.0.10 is out. Download it here.
Frama-C 23.0~rc1 (Vanadium) is out. Download it here.
Main changes with respect to Frama-C 22 (Titanium) include:
admit
annotations (which already accepted assert
and check
) to express hypotheses to be admitted but not verified by Frama-Cx86_64
; allow setting machdep via environment variable FRAMAC_MACHDEPFrama-C 23.0 (Vanadium) is out. Download it here.
Main changes with respect to Frama-C 22 (Titanium) include:
admit
annotations (which already accepted assert
and check
) to express hypotheses to be admitted but not verified by Frama-Cx86_64
; allow setting machdep via environment variable FRAMAC_MACHDEP
-eva-unroll-recursive-calls
to precisely analyze the n first recursive calls, before using the function specification to interpret the remaining calls-wp-legacy
optionFrama-Clang 0.0.11 is out. Download it here.
Frama-C 23.1 (Vanadium) is out. Download it here.
Main changes with respect to Frama-C 23 (Vanadium) include:
Keywords: control flow Integrity, remote attestation, runtime verification, static analysis, source code generation
Keywords: runtime assertion checking, compilation, source code generation, static analysis
Keywords: runtime assertion checking, outline monitoring, compilation, source code generation
Frama-C 24.0-beta (Chromium) is out. Download it here.
Main changes with respect to Frama-C 23 (Vanadium) include:
_Static_assert
\sum
, \prod
and \numof
taint
domain for taint analysismultidim
domain to improve analysis precision on arrays of structures and multidimensional arrays.dynamic_split
annotationoctagon
and bitwise
domainsoctagon
and symbolic-locations
domains-wp-overflows
option, which was unsoundterminates
clausesFrama-C 24.0 (Chromium) is out. Download it here.
Main changes with respect to Frama-C 23 (Vanadium) include:
_Static_assert
\sum
, \prod
and \numof
taint
domain for taint analysismultidim
domain to improve analysis precision on arrays of structures and multidimensional arrays.dynamic_split
annotationoctagon
and bitwise
domainsoctagon
and symbolic-locations
domains-wp-overflows
option, which was unsoundterminates
clausesKeywords: cybersecurity, software analysis, formal methods, open source
Machine Learning for Improving Formal Verification of Code [More details]
Keywords: machine learning, graph neural networks, code representation learning, formal methods
The LTest toolset is available in opam
. More information here.
Frama-Clang 0.0.12 is out. Download it here.
Frama-C 25.0~beta (Manganese) is out. Download it here.
Main changes with respect to Frama-C 24 (Chromium) include:
We are introducing Ivette, a new GUI for Frama-C. In this preliminary version, only EVA and some of its derived plug-ins are supported.
Build & install instructions are in ivette/INSTALL.md
from the source tarball. To try it, simply use ivette
in replacement of frama-c-gui
. Your feedback is welcome.
Have fun !
Frama-C 25.0 (Manganese) is out. Download it here.
Main changes with respect to Frama-C 24 (Chromium) include:
We are introducing Ivette, a new GUI for Frama-C. In this preliminary version, only EVA and some of its derived plug-ins are supported.
Build & install instructions are in ivette/INSTALL.md
from the source tarball. To try it, simply use ivette
in replacement of frama-c-gui
. Your feedback is welcome.
Have fun !
Frama-Clang 0.0.13 is out. Download it here.
Cybersecurity and Safety analysis with Frama-C / Eva [More details]
Keywords: Security, Software verification, Static analysis, Formal methods, Abstract Interpretation
Frama-C 26.0~beta (Iron) is out. Download it here.
Main changes with respect to Frama-C 25.0 (Manganese) include:
The Frama-C build now uses dune. Hopefully, this should have no impact on most Frama-C users. Maintainers of external plugins must now use dune as well (see the plugin migration section in the developer manual), and the loading of modules and scripts has changed (see the frama-c-build-scripts.sh tool to build scripts for Frama-C).
calls
ACSL extension for listing potential targets of indirect calls is now supported within kernel, and not only by the WP plugin.calls
annotations.Deep Learning for improving formal verification with Frama-C / Eva [More details]
Keywords: Deep Learning, Graph Neural Networks , Representation Learning, Static analysis, Formal methods
Frama-C 26.0 (Iron) is out. Download it here.
Main changes with respect to Frama-C 25.0 (Manganese) include:
The Frama-C build now uses dune. Hopefully, this should have no impact on most Frama-C users. Maintainers of external plug-ins must now use dune as well (see the plug-in migration section in the developer manual), and the loading of modules and scripts has changed (see the frama-c-build-scripts.sh tool to build scripts for Frama-C).
calls
ACSL extension for listing potential targets of indirect calls is now supported within kernel, and not only by the WP plug-in.calls
annotations.Following the release of Frama-C 26.0 (Iron), MetAcsl v0.4 is out. The corresponding opam
package should be available soon.
MetAcsl intends to provide simple and compact ways to express properties that would demand peppering the code with thousands of annotations in plain ACSL. Its main use cases focus on security properties (notably ensuring that write and read accesses to sensitive memory locations are guarded appropriately). Feel free to consult its homepage for more information.
Frama-C 26.1 (Iron) is out. Download it here.
This minor release fixes some issues related to the compilation and installation of Frama-C.
Other changes with respect to Frama-C 26.0 (Iron) include:
Develop and extend the formal analysis capability of Frama-C [More details]
Keywords: software analysis, formal methods, open source
Develop and extend the new Frama-C GUI [More details]
Keywords: graphical user interface, software analysis, formal methods, open source
Develop and extend the kernel of Frama-C [More details]
Keywords: software analysis, formal methods, open source
Develop and extend the applicability of Frama-C for cybersecurity purposes [More details]
Keywords: cybersecurity, software analysis, formal methods, open source
If you are near Paris, come to the Cyber-hackathon Frama-C + Binsec, on 28/04 from 9h to 17h, at CEA List, in the Paris-Saclay campus (Nano-Innov, 2 bd Thomas Gobert, 91120 Palaiseau)!
Click here to register (the form is in French, but feel free to contact us directly in English if you prefer) or, for more details, click here.
Frama-C 27.0~beta (Cobalt) is out. Download it here.
Main changes with respect to Frama-C 26.0 (Iron) include:
_Generic