Tags give the ability to mark specific points in history as being important
  • 22.0
    Release 22.0

    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
  • 22.0-beta
  • 2020-10-16
  • 21.1
    9abcd565 · 21.1 minor release ·
  • 21.0   Frama-C 21.0 (Scandium) release.
    Release 21.0

    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
  • 21.0-beta
  • Vessedia-D3.5   Frama-C release as provided in Vessedia D3.5 deliverable
  • 20.0
    333b5db4 · fix changelog for release ·
  • 19.1
  • 19.0
  • 18.0