Frama-C Latest News
Internship Position at CEA List - LSL
Keywords: Frama-C, Program Analysis, IDE, Continuous Integration
Internship Position at CEA List - LSL
Keywords: Program Verification, Refinement, Frama-C, Why3
MetAcsl v0.7 for Frama-C 29.0~ Copper
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). See its homepage for more information.
Main changes in this release include:
Frama-Clang v0.0.16 for Frama-C 29.0 Copper
Frama-Clang v0.0.16 is out.
Frama-Clang is an experimental C++ front-end for Frama-C, based on the clang compiler See its homepage for more information.
Main changes in this release include:
- Better handling of ACSL constructions
- Compatibility with Clang 18
- Compatibility with Frama-C 29 Copper
The Guide to Software Verification with Frama-C is available
The Guide to Software Verification with Frama-C is now available. This book gathers contributions from 39 authors. We hope that it will help you with code analysis using Frama-C!
Abstract
Frama-C is a popular open-source toolset for analysis and verification of C programs, largely used for teaching, experimental research, and industrial applications. With the growing complexity and ubiquity of modern software, there is increasing interest in code analysis tools at various levels of formalization to ensure safety and security of software products. Acknowledging the fact that no single technique will ever be able to fit all software verification needs, the Frama-C platform features a wide set of plug-ins that can be used or combined for solving specific verification tasks.
This guidebook presents a large panorama of basic usages, research results, and concrete applications of Frama-C since the very first open-source release of the platform in 2008. It covers the ACSL specification language, core verification plug-ins, advanced analyses and their combinations, key ingredients for developing new plug-ins, as well as successful industrial case studies in which Frama-C has helped engineers verify crucial safety or security properties.
The slides presented at Frama-C Days 2024 are available
The slides presented at the Frama-C Days 2024 are now available. We would like to thank again all participants for this amazing event!
Release of Frama-C 29.0 (Copper)
Frama-C 29.0 (Copper) is out. Download it here.
Main changes with respect to Frama-C 28 (Nickel) include:
Kernel
- Introduce :: prefix for ACSL extensions
- Refactor current location handling mechanism
- Removal of Db (Db.Main.extend is deprecated). Features related to asynchronous interactions are now handled in module Async
- Various fixes and improvements
Alias
- Better analysis results in the presence of structures
- Rework the API and improved the documentation
Eva
- Better reporting for garbled mix
- Improved handling of and _read
E-ACSL
- Fix TLS segment start address and size
- Remove option -e-acsl-version
WP
- Generation of counter examples, see option -wp-counter-examples
- Upgrade to Why3 1.7.x and improved prover selection
- Extended support for Ivette
Ivette
- Revamped workspace (tabs, views, dock, alerts, notifications, …)
- Types and Globals navigation
- Better feedback on Eva values evaluation
- Extended support for WP
- Improve performances
Beta release of Frama-C 29.0~beta (Copper)
Frama-C 29.0~beta (Copper) is out. Download it here.
Main changes with respect to Frama-C 28 (Nickel) include:
Kernel
- Introduce
\plugin::
prefix for ACSL extensions - Refactor current location handling mechanism
- Removal of Db (Db.Main.extend is deprecated). Features related to asynchronous interactions are now handled in module Async
- Various fixes and improvements
Alias
- Better analysis results in the presence of structures
- Rework the API and improved the documentation
Eva
- Better reporting for garbled mix
- Improved handling of
\valid
and\valid_read
E-ACSL
- Fix TLS segment start address and size
- Remove option -e-acsl-version
WP
- Generation of counter examples, see option -wp-counter-examples
- Upgrade to Why3 1.7.x and improved prover selection
- Extended support for Ivette
Ivette
- Revamped workspace (tabs, views, dock, alerts, …)
- Types and Globals navigation
- Better feedback on Eva values evaluation
- Extended support for WP
Postdoc Position at CEA List - LSL
Keywords: ACSL, contracts, static analysis
Postdoc Position at CEA List - LSL
Keywords: runtime assertion checking, compilation, source code generation, static analysis
Frama-C Days 2024
After 5 years of absence, the Frama-C Days are back!
On June 13 and 14, will be held the Frama-C Days at Maison de la Radio et de la Musique in Paris, so save the date and stay tuned!
The complete program is available through this link.
The blog post will be updated when registration is open.
Frama-Clang v0.0.15 for Frama-C 28.0 Nickel
Frama-Clang v0.0.15 is out.
See its homepage for more information.
Main changes in this release include:
- Better handling of mixed C/C++ code and
extern "C"
declarations - Compatibility with Clang 17
- Compatibility with Frama-C 28.x Nickel
Release of Frama-C 28.1 (Nickel)
Frama-C 28.1 (Nickel) is out. Download it here.
Main changes with respect to Frama-C 28.0 (Nickel) include:
Kernel
- Fix Cil.isConstant on lvalues with offset.
Ivette
- Fix Ivette shell wrapper on macOS.
WP
- Fix interactive prover startup.
MetAcsl v0.6 for Frama-C 28.0 Nickel
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). See its homepage for more information.
Main changes in this release include:
- compatibility with Frama-C 28.x Nickel
-meta-check-callee-assigns
can now also be given declared functions
Internship Position at CEA LIST - LSL
Keywords: Formal Methods, Abstraction, Refinement, ACSL, Frama-C
Release of Frama-C 28.0 (Nickel)
Frama-C 28.0 (Nickel) is out. Download it here.
Main changes with respect to Frama-C 27 (Cobalt) include:
Kernel
- Frama-C can now generate more default clauses (in particular terminates and exits)
- Removed deprecated options
-no-type
and-no-obj
Alias
- New plugin Alias, implements a points-to analysis
E-ACSL
- More efficient code arithmetic calculations
Eva
- Support for simple
\let
bindings - Removed deprecated Db.Value API
- Fixed unsoundness about initialization with goto and switch
WP
- New ACSL extensions for defining automatic proof strategies
- WP generates default exits and terminates, removed old options
-wp-*-terminate
- Fixed cache for interactive provers
Ivette
- Basic component for WP
- Many bug fixes
MetAcsl for Frama-C 27.x Cobalt
Following the release of Frama-C 27.0 (Cobalt), MetAcsl v0.5 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.
Main changes in this release include - new meta-variables \lhost_read
and \lhost_written
for \reading
and \writing
contexts respectively - new option -check-callee-assigns f
to treat calls to f
as writing to the locations mentioned in f
’s assigns
and reading to its \from
Permanent Computer Scientist Position at CEA LIST - LSL
Keywords: abstract interpretation, software analysis, formal methods, open source
Beta release of Frama-C 28.0~beta (Nickel)
Frama-C 28.0~beta (Nickel) is out. Download it here.
Main changes with respect to Frama-C 27 (Cobalt) include:
Kernel
- Frama-C can now generate more default clauses (in particular terminates and exits)
- Removed deprecated options
-no-type
and-no-obj
Alias
- New plugin Alias, implements a points-to analysis
E-ACSL
- More efficient code arithmetic calculations
Eva
- Support for simple
\let
bindings - Removed deprecated Db.Value API
- Fixed unsoundness about initialization with goto and switch
WP
- New ACSL extensions for defining automatic proof strategies
- WP generates default exits and terminates, removed old options
-wp-*-terminate
- Fixed cache for interactive provers
Ivette
- Basic component for WP
- Many bug fixes
Release of Frama-Clang 0.0.14
Frama-Clang 0.0.14 is out. You can download the sources here.
This release brings compatibility with Frama-C 27, Clang 15 and 16 (but removes support for Clang 10). In addition, it has now an official opam
package.
Release of Frama-C 27.1 (Cobalt)
Frama-C 27.1 (Cobalt) is out. Download it here.
Main changes with respect to Frama-C 27.0 (Cobalt) include:
Kernel
- Fixes a crash and a freeze in the GTK GUI
- Add a wrapper in
frama-c-script
formake_machdep.py
Ivette
- Fixes a crash with multiple instances of Ivette
Release of Frama-C 27.0 (Cobalt)
Frama-C 27.0 (Cobalt) is out. Download it here.
Main changes with respect to Frama-C 26 (Iron) include:
Kernel
- Supports C11
_Generic
- New machdep mechanism, based on YAML files
- New script for generating machdeps from a C11 compiler
Aoraï
- Supports specification about floating-point variables.
Eva
- The octagon domain can now infer relations between any lvalues of integer or pointer types.
- Fixes the bitwise domain on big-endian architectures.
WP
- Why3 version bumped to 1.6.0.
- New options for controlling goal automatic splitting
- Default timeout is now 2s
GTK GUI
- Removed GTK2 support
Ivette
- The Eva table can show the values of function parameters, the logical status of ACSL predicates, and the values of C lvalues in these predicates. It also shows the status of uninitialized and escaping variables.
- Information about C types are shown in the Inspector.
- Many bug fixes and user experience improvements.
Beta release of Frama-C 27.0~beta (Cobalt)
Frama-C 27.0~beta (Cobalt) is out. Download it here.
Main changes with respect to Frama-C 26 (Iron) include:
Kernel
- Supports C11
_Generic
- New machdep mechanism, based on YAML files
- New script for generating machdeps from a C11 compiler
Aoraï
- Supports specification about floating-point variables.
Eva
- The octagon domain can now infer relations between any lvalues of integer or pointer types.
- Fixes the bitwise domain on big-endian architectures.
WP
- Why3 version bumped to 1.6.0.
- New options for controlling goal automatic splitting
- Default timeout is now 2s
GTK GUI
- Removed GTK2 support
Ivette
- The Eva table can show the values of function parameters, the logical status of ACSL predicates, and the values of C lvalues in these predicates. It also shows the status of uninitialized and escaping variables.
- Information about C types are shown in the Inspector.
- Many bug fixes and user experience improvements.
Cyberhackathon Frama-C + Binsec
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)!
Registration is closed (the form is in French, but feel free to contact us directly in English if you prefer) or, for more details, click here.
3-year Engineer Position at CEA LIST - LSL
Keywords: Cybersecurity, Software Analysis, Formal Methods, OCaml
3-year Computer Scientist Position at CEA LIST - LSL
Keywords: Software Analysis, Formal Methods, OCaml
3-year Engineer Position at CEA LIST - LSL
Keywords: GUI, TypeScript, OCaml, Analysis Environment
3-year Computer Scientist Position at CEA LIST - LSL
Keywords: Software Analysis, Formal Methods, OCaml
Release of Frama-C 26.1 (Iron)
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:
Kernel
- Accepts attribute in logic annotations
- Fixes issue in pretty-printing ranges
WP
- Fixes ‘terminates’ goals generation when some ‘terminates’ or ‘decreases’ clauses are missing.
MetAcsl for Frama-C 26.0 Iron
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.
Release of Frama-C 26.0 (Iron)
Frama-C 26.0 (Iron) is out. Download it here.
Main changes with respect to Frama-C 25 (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).
Kernel
calls
ACSL extension for listing potential targets of indirect calls is now supported within kernel, and not only by the WP plug-in.
Aoraï
- remove (almost unused) support for LTL and Promela as input language.
- support for programs with indirect calls if they are annotated with
calls
annotations.
E-ACSL
- add support for logic functions returning a rational number.
Eva
- complete the Eva public API; the Db.Value API is now deprecated.
- allow reducing the value of arguments of functions interpreted by a builtin or an ACSL specification; this is especially useful on C asserts.
- improved precision and performance of the octagon domain.
WP
- improved Json output for verification statistics and results.
- Why3 version bumped to 1.5.1.
Ivette (new Frama-C GUI)
- the installation of Frama-C provides an installation script for Ivette. Run ‘ivette’ once to finalize installation (this requires node 16, yarn and an internet connection).
- improve the dataflow graphs generated by the Dive plug-in.
- when the taint domain of Eva is enabled, taint status of lvalues is shown in the Inspector component and in Dive graphs.
Internship Position at CEA LIST - LSL
Keywords: Deep Learning, Graph Neural Networks , Representation Learning, Static analysis, Formal methods
Beta release of Frama-C 26.0~beta (Iron)
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).
Kernel
calls
ACSL extension for listing potential targets of indirect calls is now supported within kernel, and not only by the WP plugin.
Aoraï
- remove (almost unused) support for LTL and Promela as input language.
- support for programs with indirect calls if they are annotated with
calls
annotations.
E-ACSL
- add support for logic functions returning a rational number.
Eva
- complete the Eva public API; the Db.Value API is now deprecated.
- allow reducing the value of arguments of functions interpreted by a builtin or an ACSL specification; this is especially useful on C asserts.
- improved precision and performance of the octagon domain.
WP
- improved Json output for verification statistics and results.
- Why3 version bumped to 1.5.1.
Ivette (new Frama-C GUI)
- the installation of Frama-C provides an installation script for Ivette. Run ‘ivette’ once to finalize installation (this requires node 16, yarn and an internet connection).
- improve the dataflow graphs generated by the Dive plugin.
- when the taint domain of Eva is enabled, taint status of lvalues is shown in the Inspector component and in Dive graphs.
Internship Position at CEA LIST - LSL
Keywords: Security, Software verification, Static analysis, Formal methods, Abstract Interpretation
Release of Frama-Clang 0.0.13
Frama-Clang 0.0.13 is out. Download it here.
Release of Frama-C 25.0 (Manganese)
Frama-C 25.0 (Manganese) is out. Download it here.
Main changes with respect to Frama-C 24 (Chromium) include:
Kernel
- The experimental AST Diff module allows to compute difference between the AST of two projects
- significant changes in AST types that might break existing development
E-ACSL
- add support for Linux’s pthread concurrency
EVA
- New public API to run the analysis and access its results, intended to replace the old API in Db.Value.
- Improved multidim domain: it is now more precise and more robust, and is able to infer simple array invariants and disjunctive struct invariants.
WP
- uses Why3 1.5.0
- new supported ACSL features : decreases clause and general measures for variant and decreases
- new tactics: Clear for hypothesis removal and ModMask for rewriting of mask and modulos
- removed deprecated legacy WP engine and native prover output (always use Why3)
- fixes loop invariant order and collect more hypotheses when proving them
Ivette (New Frama-C GUI)
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 !
Beta release of Frama-C 25.0~beta (Manganese)
Frama-C 25.0~beta (Manganese) is out. Download it here.
Main changes with respect to Frama-C 24 (Chromium) include:
Kernel
- The experimental AST Diff module allows to compute difference between the AST of two projects
- significant changes in AST types that might break existing development
E-ACSL
- add support for Linux’s pthread concurrency
EVA
- New public API to run the analysis and access its results, intended to replace the old API in Db.Value.
- Improved multidim domain: it is now more precise and more robust, and is able to infer simple array invariants and disjunctive struct invariants.
WP
- uses Why3 1.5.0
- new supported ACSL features : decreases clause and general measures for variant and decreases
- new tactics: Clear for hypothesis removal and ModMask for rewriting of mask and modulos
- removed deprecated legacy WP engine and native prover output (always use Why3)
- fixes loop invariant order and collect more hypotheses when proving them
Ivette (New Frama-C GUI)
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 !
Release of Frama-Clang 0.0.12
Frama-Clang 0.0.12 is out. Download it here.
Release of LTest 0.1
The LTest toolset is available in opam
. More information here.
PhD Position at CEA LIST - LSL
Keywords: machine learning, graph neural networks, code representation learning, formal methods
Permanent Computer Scientist Position at CEA LIST - LSL
Keywords: cybersecurity, software analysis, formal methods, open source
Release of Frama-C 24.0 (Chromium)
Frama-C 24.0 (Chromium) is out. Download it here.
Main changes with respect to Frama-C 23 (Vanadium) include:
Kernel
- support C11’s
_Static_assert
- support for flexible array members in nested struct (gcc machdeps only)
- fixes unsound reuse of recursive functions
E-ACSL
- new options for more precise reporting in case of failed assertion
- support for
\sum
,\prod
and\numof
Eva
- new experimental
taint
domain for taint analysis - new experimental
multidim
domain to improve analysis precision on arrays of structures and multidimensional arrays. - new options for interprocedural states partitioning
- new
dynamic_split
annotation - fixes soundness bugs in
octagon
andbitwise
domains - improve precision for
octagon
andsymbolic-locations
domains
Variadic
- translation of printf/scanf calls with non-constant formatting string (assuming arguments match the format)
- falls back to a generic translation if specialized one fails, to guarantee the absence of variadic calls after the plugin has run
WP
- removed
-wp-overflows
option, which was unsound - experimental support for
terminates
clauses
Beta release of Frama-C 24.0-beta (Chromium)
Frama-C 24.0-beta (Chromium) is out. Download it here.
Main changes with respect to Frama-C 23 (Vanadium) include:
Kernel
- support C11’s
_Static_assert
- support for flexible array members in nested struct (gcc machdeps only)
- fixes unsound reuse of recursive functions
E-ACSL
- new options for more precise reporting in case of failed assertion
- support for
\sum
,\prod
and\numof
Eva
- new experimental
taint
domain for taint analysis - new experimental
multidim
domain to improve analysis precision on arrays of structures and multidimensional arrays. - new options for interprocedural states partitioning
- new
dynamic_split
annotation - fixes soundness bugs in
octagon
andbitwise
domains - improve precision for
octagon
andsymbolic-locations
domains
Variadic
- translation of printf/scanf calls with non-constant formatting string (assuming arguments match the format)
- falls back to a generic translation if specialized one fails, to guarantee the absence of variadic calls after the plugin has run
WP
- removed
-wp-overflows
option, which was unsound - experimental support for
terminates
clauses
PhD Position at CEA List - LSL
Keywords: runtime assertion checking, outline monitoring, compilation, source code generation
Postdoc Position at CEA List - LSL
Keywords: control flow Integrity, remote attestation, runtime verification, static analysis, source code generation
Release of Frama-C 23.1 (Vanadium)
Frama-C 23.1 (Vanadium) is out. Download it here.
Main changes with respect to Frama-C 23.0 (Vanadium) include:
E-ACSL
- Fix crash related to several ACSL constructs
- Fix crash when raising some user errors
WP
- Fix a crash related to opaque structures memory typing
Release of Frama-Clang 0.0.11
Frama-Clang 0.0.11 is out. Download it here.
Release of Frama-C 23.0 (Vanadium)
Frama-C 23.0 (Vanadium) is out. Download it here.
Main changes with respect to Frama-C 22 (Titanium) include:
Kernel
- New
admit
annotations (which already acceptedassert
andcheck
) to express hypotheses to be admitted but not verified by Frama-C - Set default machdep to
x86_64
; allow setting machdep via environment variableFRAMAC_MACHDEP
AORAI
- New option for tracking the last N states of the automaton. Easier analysis of instrumented code with Eva
E-ACSL
- Add runtime support for Windows
- Add support for loop variant
- Add support for multiple binders in guarded quantifications
EVA
- Partial support for recursion: new option
-eva-unroll-recursive-calls
to precisely analyze the n first recursive calls, before using the function specification to interpret the remaining calls - Improved automatic widening thresholds
- Improved automatic loop unroll
WP
- New internal WP engine, fixing many issues related to control flow graph and local variable scoping. Support for stmt contracts has been removed. Support for looping gotos has been removed. Altough unsound, the legacy engine is still accessible via
-wp-legacy
option - Bump Why3 version to 1.4.0
- Section « Limitation & Roadmap » added to the WP manual
Beta release of Frama-C 23.0~rc1 (Vanadium)
Frama-C 23.0~rc1 (Vanadium) is out. Download it here.
Main changes with respect to Frama-C 22 (Titanium) include:
Kernel
- New
admit
annotations (which already acceptedassert
andcheck
) to express hypotheses to be admitted but not verified by Frama-C - Set default machdep to
x86_64
; allow setting machdep via environment variable FRAMAC_MACHDEP
AORAI
- New option for tracking the last N states of the automaton. Easier analysis of instrumented code with Eva.
E-ACSL
- Add runtime support for Windows
- Add support for loop variant
- Add support for multiple binders in guarded quantifications
EVA
- Partial support for recursion: new option -eva-unroll-recursive-calls to precisely analyze the n first recursive calls, before using the function specification to interpret the remaining calls.
- Improved automatic widening thresholds
- Improved automatic loop unroll
WP
- New internal WP engine, fixing many issues related to control flow graph and local variable scoping. Support for stmt contracts has been removed. Support for looping gotos has been removed. Altough unsound, the legacy engine is still accessible via -wp-legacy option.
- Bump Why3 version to 1.4.0
- Section « Limitation & Roadmap » added to the WP manual.
Release of Frama-Clang 0.0.10
Frama-Clang 0.0.10 is out. Download it here.
First release of MetAcsl plugin
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.
Release of Frama-C 22.0 (Titanium)
Frama-C 22.0 (Titanium) is out. Download it here.
Main changes with respect to Frama-C 21 (Scandium) include:
Kernel:
- OCaml version greater than or equal to 4.08.1 required.
- introduce check-only annotations for requires, ensures, loop invariant and lemmas
\from
now accepts&v
expressions- add option
-print-config-json
, to output Frama-C configuration data in JSON format - new option
-explain
, which provides help messages for options used on the command line - add option
-print-cpp-commands
, to print the preprocessing commands used by Frama-C - support for C11’s
_Noreturn
and_Thread_local
specifiers - allows for axiomatic blocks-like extensions
Aorai:
- Ya automata can set auxiliary variables during a transition, and use such variables in subsequent guards.
E-ACSL:
- support of bitwise operators
- support of
\separated
- support of
complete
anddisjoint
behaviors - support of logical array comparisons
Eva:
- easier setup of dynamic allocation builtins: new option
-eva-alloc-builtin
to configure uniformly their behavior (instead of mapping eachmalloc
/calloc
/realloc
function to the corresponding builtin), and new annotationeva_allocate
to locally override the global option - new builtins for trigonometric functions
acos
,asin
andatan
(and their single-precision versionacosf
,asinf
,atanf
) - improved automatic loop unroll (
-eva-auto-loop-unroll
option) on loops with several exit conditions, conditions using equality operators, temporary variables introduced by the Frama-C normalization orgoto
statements
Markdown Report:
- update Sarif output to 2.1.0 and prettier URI
Variadic:
- the generated code is now compilable and compatible with E-ACSL
WP:
- upgraded Why3 backend (requires why3 1.3.3)
- support of the
\initialized
ACSL predicate - support for generalized check-only ACSL annotations
- added support for Why3 interactive prover (Coq)
- new tactic Bit-Test range
- memory model hypotheses warnings are more precise
- new experimental option:
-wp-check-memory-model
to automatically check memory model hypotheses - new warning
pedantic-assigns
. WP needs preciseassigns ... \from ...
specification about out pointers to generate precise proof hypotheses
A complete changelog can be found here.
Beta release of Frama-C 22.0-beta (Titanium)
Frama-C 22.0-beta (Titanium) is out. Download it here.
Main changes with respect to Frama-C 21 (Scandium) include:
Kernel:
- OCaml version greater than or equal to 4.08.1 required.
- introduce check-only annotations for requires, ensures, loop invariant and lemmas
\from
now accepts&v
expressions- add option
-print-config-json
, to output Frama-C configuration data in JSON format - new option
-explain
, which provides help messages for options used on the command line - add option
-print-cpp-commands
, to print the preprocessing commands used by Frama-C - support for C11’s
_Noreturn
and_Thread_local
specifiers - allows for axiomatic blocks-like extensions
Aorai:
- Ya automata can set auxiliary variables during a transition, and use such variables in subsequent guards.
E-ACSL:
- support of bitwise operators
- support of
\separated
- support of
complete
anddisjoint
behaviors - support of logical array comparisons
Eva:
- easier setup of dynamic allocation builtins: new option
-eva-alloc-builtin
to configure uniformly their behavior (instead of mapping eachmalloc
/calloc
/realloc
function to the corresponding builtin), and new annotationeva_allocate
to locally override the global option - new builtins for trigonometric functions
acos
,asin
andatan
(and their single-precision versionacosf
,asinf
,atanf
) - improved automatic loop unroll (
-eva-auto-loop-unroll
option) on loops with several exit conditions, conditions using equality operators, temporary variables introduced by the Frama-C normalization orgoto
statements
Markdown Report:
- update Sarif output to 2.1.0 and prettier URI
Variadic:
- the generated code is now compilable and compatible with E-ACSL
WP:
- upgraded Why3 backend (requires why3 1.3.3)
- support of the
\initialized
ACSL predicate - support for generalized check-only ACSL annotations
- added support for Why3 interactive prover (Coq)
- new tactic Bit-Test range
- memory model hypotheses warnings are more precise
- new experimental option:
-wp-check-memory-model
to automatically check memory model hypotheses - new warning
pedantic-assigns
. WP needs preciseassigns ... \from ...
specification about out pointers to generate precise proof hypotheses
A complete changelog can be found here.
Release of Frama-Clang 0.0.9
Frama-Clang 0.0.9 is out. Download it here.
Release of Frama-C 21.1 (Scandium)
Frama-C 21.1 (Scandium) is out. Download it here.
This minor release fixes a few issues in WP.
Release of Frama-C 21.0 (Scandium)
Frama-C 21.0 (Scandium) is out. Download it here.
Main changes with respect to Frama-C 20 (Calcium) include:
Kernel:
- new option
-warn-invalid-pointer
(disabled by default; warns on pointer arithmetic resulting in invalid values) - new option
-warn-pointer-downcast
(enabled by default; warns when a pointer/integer conversion may lead to loss of precision) - improved ghost support: ghost else, and check that ghost code does not alter normal control flow
- constfold can now use value of const globals
Eva:
- New option
-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 - New option
-eva-domains-function
to enable domains only on given functions - When
-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) - The subdivision of evaluations can now be enabled locally:
- on given functions through option
-eva-subdivide-non-linear-function
- on specific statements via
/*@ subdivide N; */
annotations.
- on given functions through option
WP:
- Upgraded Why3 backend (requires why3 1.3.1)
- Support for IEEE float model (why3 provers only)
- Smoke Tests : attempt to find inconsistencies or dead code from requirements (see
-wp-smoke-tests
option in WP manual) - Many improvements in lemmas, tactics and cache management (see full WP Changelog for details).
E-ACSL:
- Better support of complex jumps for goto and switch statements
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.
Release of Frama-Clang 0.0.8
Frama-Clang 0.0.8 is out. Download it here.
Release of Frama-C 20.0 (Calcium)
Frama-C 20.0 (Calcium) is out. Download it here.
Main changes with respect to Frama-C 19 (Potassium) include:
Kernel:
- the minimum required OCaml version is now 4.05.0
- more strict checks related to ghost variables in non-ghost code, and support for ghost parameters
- visitor behavior functions were moved from Cil to a new module Visitor_behavior
Eva:
- New octagon domain inferring relations of the form a ≤ ±X±Y ≤ b between pairs of integer variables X and Y.
- New option “-eva-auto-loop-unroll N”, to unroll all loops whose number of iterations can be easily bounded by
. - Dynamic registration of abstract values and domains: developers of new domains no longer need to modify Eva’s engine.
WP:
- Use native Why3 API (now requires why3 at compile time); deprecated native alt-ergo & coq output
- New cache mechanism for why3 provers, see -wp-cache option
E-ACSL:
- Support of rational numbers and operations.
And a new plug-in, Markdown-report (MdR), to generate reports in both Markdown and SARIF formats.
A complete changelog can be found here.
Release of Frama-C 19.1 (Potassium)
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.
Release of Frama-Clang 0.0.7
Frama-Clang 0.0.7 is out. Download it here.
Release of Frama-C 19.0 (Potassium)
Frama-C 19.0 (Potassium) is out. Download it here.
Main changes with respect to Frama-C 18 (Argon) include:
Kernel:
- new check annotation, similar to assert except that it does not introduce additional hypotheses on the program state
- new options added to frama-c-script
GUI:
- compatibility with lablgtk3
Eva:
- New annotation “//@ split exp” to separate the analysis states for each possible value of an expression until a “//@ merge exp” annotation.
- New option -eva-partition-history to delay the join of the analysis states at merging points; useful when a reasoning depends on the path taken to reach a control point.
- By default, prints a summary at the end of the analysis.
- New meta option -eva-precision to globally configure the analysis.
- Improved precision on nested loops.
WP:
- new auto-search mode to automatically apply strategies and tactics (see -wp-auto)
- extended simplifications on range, bitwise and C-boolean values (_Bool is now handled by default)
- refactored float model (although it still requires further axiomatisation)
E-ACSL:
- support for user-defined logic functions and predicates without labels
- new option -e-acsl-functions that allows the user to specify a white/black list of functions in which annotations are monitored, or not.
A complete changelog can be found here.
Frama-C and SPARK Day 2019
Frama-C & SPARK Day 2019 will take place on June 3, 2019 in Paris.
Release of Frama-C 18.0 (Argon)
Frama-C 18.0 (Argon) is out. Download it here.
Main changes with respect to Frama-C 17 (Chlorine) include:
Kernel:
- Improved command-line options for treatment of warning categories: -plugin-warn-key category:status will set the status of category, instead of using 7 options -plugin-warn-abort, -plugin-warn-feedback, … with awkward ± categories
- All errors emitted during a run will now lead to a non-zero exit status of frama-c command line
- options for emitting an alarm on [left|right] shift of a negative value are now at kernel level (and removed from Eva)
- const globals are now unconditionally constants (option -const-writable is removed)
- several improvements to the frama-c libc specifications
- new binary frama-c-script to help with case studies
Eva:
- Eva is now consistently named “Eva”, and all its options start with -eva (compatibility with previous option names has been preserved).
- New “//@ loop unroll N;” annotations to unroll exactly the N first iterations of a loop, as an improvement over slevel options.
- The memexec cache is compatible with all domains, and is enabled by default. This cache greatly improves the analysis time.
- Builtins for memset and memcpy are now included in the open-source release.
- Alternative domains use the frama-c libc specification when a builtin is used, to minimize the loss of precision.
- Emits alarms when reading trap representations of type _Bool.
- New experimental domain numerors inferring absolute and relative errors of floating-point computations. Does not handle loops for now.
E-ACSL:
- support of ranges in memory built-ins, e.g. (t+(0..9))
- support of on logic variables, e.g. integer i; 0 <= i < 10 ==> t[i] == (t[i])
A complete Changelog can be found here.
Release of Frama-Clang 0.0.6
Frama-Clang 0.0.6, compatible with Frama-C 17 Chlorine, is out. Download it here.
Release of Frama-C 17.0 (Chlorine)
Frama-C 17.0 (Chlorine) is out. Download it here.
Main changes with respect to Frama-C 16 - Sulfur include:
Kernel
- Added option -inline-calls for syntactic inlining
- Introduced warning categories: possibility of disabling some warnings, converting warnings into errors and vice-versa, and more detailed warning messages
- Added support for CERT EXP46-C
- Extra-type checking verifications (e.g. in function pointer compatibility and lvalues assignments)
- Added support for JSON compilation databases, a.k.a. compile_commands.json (optional: requires package ‘yojson’)
EVA
- Added support for infinite floats and NaN (via option -warn-special-float)
- Added a new panel “Red alarms” in the GUI that shows all properties for which a red status has been emitted for some states during the analysis. They may not be completely invalid, but should often be investigated first
- Evaluate the preconditions of the functions for which a builtin is used; builtins do not emit alarms anymore
- The subdivision of evaluations (through the option -val-subdivide-non-linear) can subdivide the values of several lvalues simultaneously (on expressions such as xx - 2xy + yy)
- Various improvements in the equality domain which is now inter-procedural (equalities can be propagated through function calls)
WP
- Support for ACSL math builtins (, , , etc.) and _Bool type
- Improved Qed simplifications in many domains
- Upgrade reference versions for provers (Alt-Ergo 2.0.0, Coq 8.7.1 and Why-3 0.88.3)
- New and/or enhanced tactics available from the graphical user-interface
- Searching for strategies from the command line
E-ACSL
- New option -e-acsl-validate-format-strings to detect format string vulnerabilities in printf-like functions
A complete changelog can be found here.
Release of Frama-Clang 0.0.5
Frama-Clang 0.0.5, fixing compatibility issue with Debian/Ubuntu, is out. Download it here.
Release of Frama-Clang 0.0.4
Frama-Clang 0.0.4, compatible with Frama-C 16, is out. Download it here.
Release of Frama-C 16.0 (Sulfur)
Frama-C 16.0 (Sulfur) is out. Download it here.
Main changes with respect to Frama-C 15 - Phosphorus include:
Kernel
- Extra type checking verifications (e.g. const on local variables, qualifiers in function calls)
EVA
- Precision and efficiency improvements
- Better feedback for abstract domains
- Scripts to help analyze large programs (in $FRAMAC_SHARE/analysis-scripts)
WP
- New tacticals for TIP (for dealing with modulus, bit operations, equality rewriting, etc)
- Several new simplifications
RTE
- Emission of more alarms ()
Studia
- New plug-in for case studies with EVA, integrated in the GUI
GUI
- Display of local callgraphs (useful for large programs)
A complete changelog can be found here.
Release of Frama-Clang 0.0.3
Frama-Clang 0.0.3, compatible with Frama-C 15, is out. Download it here.
Release of Frama-C 15.0 (Phosphorus)
Frama-C 15.0 (Phosphorus) is out. Download it here.
Main changes with respect to Frama-C 14 - Silicon include:
Kernel
- E-ACSL is now included in the standard distribution
- Better handling of Variable-Length Arrays (VLA)
- ZArith is now a required dependency. Support of Big_int has been dropped
- Bash and Zsh completion for Frama-C options
- new AST nodes to explicitly mark local variable initialization
EVA
- better set of default options
- dropped support for legacy version of Value Analysis
WP
- Interactive Proof Editor in the GUI
- Extensible Proof Engine via Tactics and Strategies
- More powerful simplifications of goals
- Dynamic API is deprecated in favor of static API
- Fatally flawed support of generalized invariants (
-wp-invariants
) has been dropped
E-ACSL
- included in the standard Frama-C distribution
- use of a (much more efficient) shadow memory model by default
- much better support of unstructured control flow (complex goto, …)
Variadic
- translation of variadic calls is now enabled by default
- option names have changed to avoid confusion with EVA
A complete changelog can be found here.
Release of Frama-Clang 0.0.2
Version 0.0.2 of the Frama-Clang plugin is available for download.
Release of E-ACSL 0.0.8
Version 0.8 of the E-ACSL plugin is available.
Release of Frama-C 14.0 (Silicon)
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.
Release of Frama-Clang 0.0.1
The first version of the Frama-Clang plugin, an experimental C++ front-end for Frama-C, is available.
Release of Frama-C 13.0 (Aluminium)
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).
Release of Frama-C 12.0 (Magnesium)
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
Release of Frama-C 11.0 (Sodium)
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).
Release of Frama-C 10.0 (Neon)
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.