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:
For plug-in developers:
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:
For plug-in developers:
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:
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:
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:
Libc:
Eva/Value plugin:
WP plugin:
WP now honors the kernel option -warn-(signed | unsigned)-(overflow | downcast). The cint and cfloat are used by default |
Rte plugin:
Nonterm plugin:
Changes in the compilation process:
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:
Control Flow Integrity for Remote Attestation [More details]
Keywords: control flow Integrity, remote attestation, runtime verification, static analysis, source code generation
[FILLED] Designing Compilation Techniques for Improving Efficiency of E-ACSL, a Runtime Assertion Checker for C Programs [More details]
Keywords: runtime assertion checking, compilation, source code generation, static analysis
[FILLED] Outline Runtime Assertion Checking [More details]
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
clausesDevelop and extend the applicability of Frama-C for cybersecurity purposes [More details]
Keywords: 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 !