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 \dangling 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 (\subset, \is_NaN, \is_finite, \is_infinite, \is_plus_infinity, \is_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 \valid_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 (\initialized)

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 (\sqrt, \exp, \log, 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. \valid(t+(0..9))
• support of \at on logic variables, e.g. \forall integer i; 0 <= i < 10 ==> t[i] == \old(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

Permanent Engineer/Researcher Position at CEA LIST - LSL

Develop and extend the applicability of Frama-C for cybersecurity purposes [More details]

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

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

Control Flow Integrity for Remote Attestation [More details]

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

Postdoc Position at CEA List - LSL

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

PhD Position at CEA List - LSL

Outline Runtime Assertion Checking [More details]

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