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.

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 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 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-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 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 E-ACSL 0.0.8

Version 0.8 of the E-ACSL plugin is available.

Release of Frama-Clang 0.0.2

Version 0.0.2 of the Frama-Clang plugin is available for download.

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.3

Frama-Clang 0.0.3, compatible with Frama-C 15, 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.4

Frama-Clang 0.0.4, compatible with Frama-C 16, is out. Download it 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-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.6

Frama-Clang 0.0.6, compatible with Frama-C 17 Chlorine, is out. Download it here.

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.

Frama-C and SPARK Day 2019

Frama-C & SPARK Day 2019 will take place on June 3, 2019 in Paris. Registration and program 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.

Release of Frama-Clang 0.0.7

Frama-Clang 0.0.7 is out. Download it 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-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-Clang 0.0.8

Frama-Clang 0.0.8 is out. Download it here.

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.

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-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-Clang 0.0.9

Frama-Clang 0.0.9 is out. Download it 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 and disjoint 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 each malloc/calloc/realloc function to the corresponding builtin), and new annotation eva_allocate to locally override the global option
• new builtins for trigonometric functions acos, asin and atan (and their single-precision version acosf, 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 or goto 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 precise assigns ... \from ... specification about out pointers to generate precise proof hypotheses

A complete changelog can be found here.

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 and disjoint 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 each malloc/calloc/realloc function to the corresponding builtin), and new annotation eva_allocate to locally override the global option
• new builtins for trigonometric functions acos, asin and atan (and their single-precision version acosf, 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 or goto 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 precise assigns ... \from ... specification about out pointers to generate precise proof hypotheses

A complete changelog can be found 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-Clang 0.0.10

Frama-Clang 0.0.10 is out. Download it here.

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 accepted assert and check) 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-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 accepted assert and check) 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.11

Frama-Clang 0.0.11 is out. Download it here.

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

Postdoc Position at CEA List - LSL

Keywords: control flow Integrity, remote attestation, runtime verification, static analysis, source code generation

Postdoc Position at CEA List - LSL

Keywords: runtime assertion checking, compilation, source code generation, static analysis

PhD Position at CEA List - LSL

Keywords: runtime assertion checking, outline monitoring, compilation, source code generation

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 and bitwise domains
• improve precision for octagon and symbolic-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

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 and bitwise domains
• improve precision for octagon and symbolic-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

Permanent Computer Scientist Position at CEA LIST - LSL

Keywords: cybersecurity, software analysis, formal methods, open source

PhD Position at CEA LIST - LSL

Keywords: machine learning, graph neural networks, code representation learning, formal methods

Release of LTest 0.1

The LTest toolset is available in opam. More information here.

Release of Frama-Clang 0.0.12

Frama-Clang 0.0.12 is out. Download it here.

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-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 !

Release of Frama-Clang 0.0.13

Frama-Clang 0.0.13 is out. Download it here.

Internship Position at CEA LIST - LSL

Cybersecurity and Safety analysis with Frama-C / Eva [More details]

Keywords: Security, Software verification, Static analysis, Formal methods, Abstract Interpretation

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

Deep Learning for improving formal verification with Frama-C / Eva [More details]

Keywords: Deep Learning, Graph Neural Networks , Representation Learning, Static analysis, Formal methods

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.

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.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.

3-year Computer Scientist Position at CEA LIST - LSL

Develop and extend the formal analysis capability of Frama-C. In particular, provide new features either in the Eva plug-in or WP plug-in [More details]

Keywords: Software Analysis, Formal Methods, OCaml

3-year Engineer Position at CEA LIST - LSL

Develop and extend Ivette, the new Electron-based Frama-C graphical user interface [More details]

Keywords: GUI, TypeScript, OCaml, Analysis Environment

3-year Computer Scientist Position at CEA LIST - LSL

Develop and extend the kernel of Frama-C [More details]

Keywords: Software Analysis, Formal Methods, OCaml

3-year Engineer Position at CEA LIST - LSL

Keywords: Cybersecurity, Software Analysis, Formal Methods, OCaml

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)!

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.

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.

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.

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 for make_machdep.py

Ivette

• Fixes a crash with multiple instances of Ivette

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.

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

Permanent Computer Scientist Position at CEA LIST - LSL

Join the development team of Eva, the Frama-C plug-in based on abstract interpretation [More details]

Keywords: abstract interpretation, software analysis, formal methods, open source

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