Plugin E-ACSL

• [E-ACSL]  reduce the number of "annotating undefined function" warnings for functions that do not affect memory
  
  

Frama-C General

New Features

• [Kernel]  Removed loop pragma UNROLL annotations
• [Kernel]  New ACSL extension loop unfold (replaces loop pragma UNROLL)
• [Kernel]  Changed `Config_dir` module signature, and behavior on macOS and Windows
• [Kernel]  New minimal OCaml version: 4.14
• [Kernel]  Place noreturn attribute on types instead of vars
• [Kernel]  New warning category typing:implicit-int, allowing to omit type specifiers in declarations (default is error).
• [Kernel]  Extension for importing external modules in ACSL
• [Kernel]  Support for ACSL modules.
• [Kernel]  Option for converting stmt contracts into ACSL assert for plug-ins with incomplete stmt contract support See option -inline-stmt-contracts
• [Kernel]  Asm contracts can now have \initialized ensures. See option -asm-contracts-ensure-init
• [Kernel]  Warn when encountering an unknown attribute
• [Kernel]  Add partial parsing support for statement/label attributes

Developers Only

• [Kernel]  Renamed module Unroll_loop into Unfold_loop
• [Kernel]  mapNoCopy moved to Extlib and deprecated in Cil
• [Kernel]  Changed `Share` module signature
• [Kernel]  Added new modules `Cache_dir` and `State_dir` and additional facilities to build sub-directories in these
• [Kernel]  Plug-ins Dominators and Postdominators have been removed and replaced by the Dominators module in the kernel.
• [Kernel]  New Machine module to manage theMachine and machdeps. Cil functions related to theMachine are deprecated.
• [Kernel]  Pragma nodes in the AST have been removed
• [Kernel]  Move functions for finding logic types, functions, predicates and constructors from Logic_typing to Logic_env.
• [Kernel]  API to register ACSL extern modules import functions
• [Kernel]  ACSL extensions are now associated to a plug-in, allowing the registration of several extensions with the same name from different plug-ins
• [Kernel]  introduce logic type Lboolean and constants

Plugin Alias

• no longer classify virtually all casts as unsafe

Plugin E-ACSL

New Feature

• [E-ACSL]  add support for labelled logic functions in case they are called only with the Here label.

Bug Fixes

• [E-ACSL]  fix typing of logic functions over rationals
  
  
• [E-ACSL]  fix arity confusion of generated functions. When a logic function is called from different contexts requiring different return types, this was not correctly taken into account, leading to functions calls with an incorrect number of arguments.
• [E-ACSL]  no longer crash with an exception during typing phase when encountering certain unsupported expressions; instead emit the usual not-yet-supported warning.
• [E-ACSL]  handle negative integers generated by RTE
• [E-ACSL]  fix logic variable escaping its scope
• [E-ACSL]  fix usage of structural equality of terms; By using physical equality we ensure that structurally identical terms are translated according to their context.

Plugin Eva

New Features

• Support for 'calls' ACSL extension
• Removes approximation messages "more than N elements to enumerate".
• Fewer false alarms of signed overflow on divisions.
• Never emit alarms on pointer conversions to intptr_t or uintptr_t.

Bug Fixes

• Fixes possible unsoundness when writing 0 on a set of contiguous and non-overlapping locations containing a value with a different size or alignment than the write.
• Fixes number of sure alarms by function shown in Ivette.
• Fixed missing signed overflow alarm on modulo.

Developers Only

• Export profiling information about the analysis performance via the new module Eva_perf in Eva.mli.

Plugin Impact

• -impact-pragma is now -impact-annot
• `impact pragma stmt` is now `impact_stmt`

Plugin Ivette

• Improved colored status bullets in AST view.
  
  
• In the sidebar, global variables and types are sorted by name.
• Include global initializations in the list of writes of a global variable.
• New left sidebar to configure and run Eva analyses.
• New flamegraph component to visualize Eva analysis time by C functions, in the "Eva Summary" view by default.
• Show the "Source Code" view at first launch.
• Complete rewriting of the callgraph, improving its readability and usability and adding new features: filtering and selecting functions, showing alarms by function, and more.

Plugin RTE

• Fixed missing assertion on modulo signed overflow.

Plugin Slicing

• -slice-pragma is now -slice-annot
• `slice pragma <elem>` is now `slice_preserve_<elem>`

Plugin WP

• [WP]  Why3 module importer (See manual § 2.4.13)
• [WP]  -wp-par now defaults to the number of logical cores
• [WP]  Remove wp_region
• [WP]  Fixed parsing of decimal literals
  
  

Frama-C General

New Features

• [Kernel]  Introduce \plugin:: prefix for ACSL extensions, unknown extensions can be safely ignored when the plug-in that handles them is not available
• [Kernel]  Systematically abort when a function is redeclared with an incompatible type, instead of trying to finish type-checking, preventing misleading error msgs after the first report. IncompatibleDeclHook has thus been removed from the API.
• [Kernel]  Avoid ambiguous pretty-printing when C labels match the name of an ACSL built-in label (fix #1359)
• [Kernel]  Change format of custom_defs field in machdep schema and allow #undefining builtin macros in the command-line.
• [Kernel]  new warning category too-large-array, allowing to use array > SIZE_MAX by changing its status (default is error).

Bug Fixes

• [Kernel]  When an array is declared with a fixed length l, raise an error if l * sizeof(elem) > SIZE_MAX
• [Kernel]  Accept conditional expr whose 2d and 3d operands have type void, as per C11 6.5.15§3

Developers Only

• [Dev]  Remove frama-c-build-scripts.sh; add a section in the user manual about how to manually replace it.
• [Kernel]  Db is now mostly empty, the only remaining value is Db.Main.extend which is deprecated and replaced by Boot.Main.extend. Features related to asynchronous interactions are now handled in module Async
• [Kernel]  Merged AST nodes TCastE and TLogic_coerce
• [Kernel]  More coherent naming of functions determining if a symbol is a Frama-C built-in.
• [Kernel]  Refactor current location handling mechanism
• [Kernel]  Annotations.{fold,iter}_behaviors now pass full behaviors to the iterated function. To iter on fragments split by behavior and emitter, use {fold,iter}_behaviors_by_emitter.
• [Kernel]  Remove deprecated funcs Extlib.string_{pre,suf}fix

Plugin Alias

• Fix analysis results in the presence of structures. Complete rework of the API. Improved documentation. Fix stack overflow in case of a cyclic graph.

Plugin E-ACSL

• [E-ACSL]  remove option -e-acsl-version.
• [E-ACSL]  fix TLS segment start address and size
  
  

Plugin Eva

New Features

• Better reporting of imprecise "garbled mix" values (resulting from imprecise or unsupported operations on addresses) through more relevant messages and a compact summary at the end of the analysis, enabled by default.
• Reduce pointer values according to ACSL predicate valid_string and valid_read_string.
• Reduce pointer values according to ACSL predicate \base_addr.
• Remove support for deprecated WIDEN_HINTS loop pragma. Use ACSL extension "widen_hints" instead.
• Improve builtins memcpy, memmove and memset when arguments are imprecise.

Bug Fix

• Fix a crash when running successive analyses using the -eva-domains-function parameter.

Plugin Ivette

New Features

• Global variables and types are listed in the sidebar. Global variables can be filtered according to some criteria.
  
  
• Complete redesign of the main view. Components and views can be selected in the left sidebar (the right sidebar has been removed). The top bar contains tabs of the currently selected views. Components can be docked in the bottom bar, to be shown or hidden on a simple click.
• Add shortcut to select next/previous tab.
• Add feedback when the user requests the evaluation of a custom term.
• In the Eva values table, show values before/after statements with annotation, as values can be reduced after them.
• New notifications at the bottom-right of the main window. Some components are highlighted in the bottom bar when they are updated but are not currently visible.
• Fix performance issues on large codebases.

Developers Only

• Upgrade to node 20 and electron 28. Use vite instead of webpack. Upgrade many dependencies.

Plugin Variadic

• Make sure that generated functions have fresh names

Plugin WP

• [GUI]  Introduce goal visualization and tactics in Ivette
  
  
• [WP]  Introduce counter examples via the new option -wp-counter-examples. Also introduce an ACSL extension to create probes on terms for counter examples.
• [WP]  wp_nullable_args is renamed \wp::nullable_args to follow kernel changes
• [WP]  Type logic function calls when they have C types
• [WP]  Fix interactive prover startup when the script already exists

Frama-C General

• [Kernel]  Fix Cil.isConstant on lvalues with offset.

Plugin Ivette

• Fix Ivette shell wrapper on macOS.
  
  

Plugin WP

• [WP]  Fix interactive prover startup.
  
  

Frama-C General

New Features

• [Kernel]  Fix #846 (printing ACSL attribute in ghost code)
• [Kernel]  New options -generated-spec-mode and -generated-spec-custom for configuring how default specifications are generated
• [Kernel]  Remove options -no-type and -no-obj and related functions.

Developers Only

• [Kernel]  Expose Cil functions for type compatibility
• [Kernel]  Remove Dynamic.Unloadable exception, useless since the move from dynamic to static API for plug-ins.
• [Kernel]  New mechanism for generating default specifications

Plugin Alias

• New alias plugin that implements a points-to analysis and an alias analysis based on Steensgaard's algorithm. For these purposes it presents a more efficient (albeit less precise) alternative to Eva. See src/plugins/alias/README.md.

Plugin E-ACSL

• [E-ACSL]  Generate more efficient code for arithmetic calculations. This is achieved by appraising more precisely the possible values an arithmetic variable can take. This allows in many cases for native computations instead of generating slower GMP code. Introduces new flags: -e-acsl-widening-*
  
  

Plugin Eva

New Features

• Print less messages unless -eva-show-progress is set.
• Adds warning key "garbled-mix" to all log messages related to garbled mix (degenerated imprecise values).
• Support evaluation of simple \let bindings in ACSL terms and predicates.
• Optimization of the multidim domain.

Bug Fixes

• Fix convergence issue on dynamic memory allocation in some loops.
  
  
• Fix unsound behavior on goto or switch statements skipping local variable declarations: initialization alarms about such variables are now properly emitted.

Developers Only

• Remove deprecated API Db.Value.

Plugin WP

• [GUI]  Basic WP goals component for Ivette
• [TIP]  Activation of Strategies
• [WP]  ACSL extension 'proof' for proof resolution hints
  
  
• [WP]  ACSL extension 'strategy' for proof strategies
• [WP]  New option -wp-strategy s,... for default strategies
• [WP]  New option -wp-tactic to search for tactics
• [WP]  New option -wp-status to print unproved goals
• [WP]  New option -wp-script=mode (see also -wp-cache-env)
• [WP]  New option -wp-no-strategy-engine to deactivate strategies
• [WP]  Option -wp-prop extended to lemma and function names
• [WP]  Tactic Absurd now also applies to proof goal
• [WP]  Tactic Compute (new, generalize Definition and Split)
• [WP]  Fixed cache for interactive provers
• [WP]  New option -wp-memlimit for provers
• [WP]  Sequent simplification now applies to lemmas
• [WP]  Removed options -wp-frama-c-stdlib-terminate, -wp-declarations-terminate and -wp-definitions-terminate. Use -generated-spec-* to disable generation of terminates (or exits)
• [WP]  WP generates exits and terminates specification on all functions, using the mechanism provided by the Frama-C kernel
• [WP]  Ensure compatibility with Why3 1.7.0

Frama-C General

• [Kernel]  New frama-c-script wrapper for make_machdep.py

Frama-C GUI

• [Gui]  Fixes freeze when a plugin aborts during splash screen
• [Gui]  Fixes crash related to tags and undefined types
  
  

Plugin Ivette

• Fixes crash with multiple instances

Frama-C General

• [Kernel]  New machdep mechanism, based on YAML files. A new make_machdep.py script allows automatic machdep creation from a C11-compatible (cross-)compiler.
• [Kernel]  Deprecate option -c11 (now enabled by default).
• [Kernel]  Add support for C11's _Generic. Modifies Cabs AST.

Frama-C GUI

• [Gui]  Remove GTK2 bindings. Only support GTK3 as of now.

Plugin Aorai

• Allows comments in .ya automata files.
• Supports specification about floating-point variables.

Plugin E-ACSL

• [e-acsl-gcc]  arguments to options -e/--cpp-flags now overload the default values set by e-acsl-gcc instead of being ignored.
  
  

Plugin Eva

New Features

• Better partitioning splits on ACSL predicates.
  
  
• Fixes performance issues on programs with too many function calls (more than 20000 callsites).
• Better display of large integer sets for high values of the -eva-ilevel parameter.
• When possible, Eva shows the name of enumeration tags instead of their integer values, in the log and the GUI.
• The octagon domain can now infer relations between any lvalues of integer or pointer types.

Bug Fixes

• Fixes unsoundness of the bitwise domain on shifts and casts on big-endian architectures.
• Fixes a soundness bug of the equality domain when the same equality holds in two programs paths, but involving a pointer pointing to different variables in the two paths.
• Fixes interpretation of Eva annotations at the end of a block, and of multiple split annotations after a function call.

Plugin Ivette

New Features

• Shows information about C types in the Inspector.
• Better display of dead and non-terminating statements.
• Improves function filtering in the left sidebar.
• The values table can show the logical status of ACSL predicates, and the values of C lvalues in these predicates.
• The values table shows values of function parameters.
• The values table shows the status of uninitialized and escaping variables.
• New callgraph component.

Bug Fixes

• Custom views are correctly saved and reloaded.
• Ends properly frama-c process when Ivette is closed.

Plugin WP

• [WP]  new option -wp-why3-extra-config for providing additional Why3 configuration files
  
  
• [WP]  Upgrade to Why3 1.6.0
• [WP]  renamed option -wp-split-depth into -wp-split-cnf
• [WP]  new option -wp-split-conj to split conjunctive goals
• [WP]  new option -wp-split-switch to split switches
• [WP]  fix option -wp-split to only split conditions
• [WP]  Default timeout set to 2s
• [WP]  new warning against unions (see -wp-warn-key "union")

Frama-C General

• [Logic]  Accept \ghost attribute in logic annotations (#2638)
• [Logic]  Fix issue in pretty-printing ranges (#2639)
  
  

Plugin WP

• [WP]  Fixes 'terminates' goals generation when some 'terminates' or 'decreases' clauses are missing.
  
  

Frama-C General

New Features

• [Kernel]  Remove journalisation.
• [Kernel]  Improve error message for invalid options -D/-I/-U.
• [Kernel]  -version prints a newline, -print-version does not.
• [Kernel]  Support for ghost VLA and calls to builtins with ghost arguments.
• [Kernel]  'calls' ACSL extension is now registered in the kernel and not WP

Developers Only

• [Configure]  Removed autoconf and configure
• [Makefile]  Removed Makefile, Frama-C is now built using Dune 3.x

Plugin Aorai

• Remove support for LTL and Promela input formats

Plugin E-ACSL

New Features

• [E-ACSL]  Improve typing precision of variables appearing in comparisons.
• [E-ACSL]  Add support for functions returning a rational.

Bug Fixes

• [E-ACSL]  Fix wrong cast from pointer to integer (#1119).
  
  
• [E-ACSL]  Fix typing of recursive predicates (#198).
• [E-ACSL]  Fix assign clause and result as extra argument for functions returning a structure (#1139).
• [E-ACSL]  Fix clashing name when a function with contract and a logic function have the same name (#204).

Plugin Eva

New Features

• Avoid false alarms of partially overlapping lvalue assignments when writing a struct array from itself.
  
  
• Improved precision: arguments of calls interpreted by an Eva builtin or with an ACSL specification can now be reduced in the caller. This is especially useful on C asserts.
• Numerors now needs MLMPFR 4.1.0+bugfix2
• The octagon domain can infer relations on the integer conversion of floating-point variables.

Bug Fixes

• Fixes a possible crash when -eva-subdivide-non-linear and relational domains are enabled.
• Fixes a crash on recursive functions with an ACSL specification without assigns clause.

Developers Only

• Deprecate Db.Value API: use the new Eva API instead.

Plugin From

• Removed Db.From API: use the From API instead.

Plugin Ivette

• In the AST component, the user can fold/unfold ACSL specifications, and preconditions are now shown at call sites.
• New component 'Eva States' that prints the internal Eva domain states at a given statement for the selected marker.
• Fixes some issues in the data dependency graphs generated by the Dive plugin in the 'Dive Dataflow' component.
• The installation of Frama-C provides an installation script for Ivette: run 'ivette' once to finalize its installation.
• After an Eva analysis with taint, the taint status of lvalues is shown in the Inspector component and in Dive graphs.

Plugin Pdg

• Removed from Db. Use proper Pdg API instead.

Plugin WP

• [Cmd]  Improves the WP JSON report provided by -wp-report-json
  
  
• [WP]  'calls' ACSL extension moved into the kernel; option -wp-dynamic marked as obsolete
• [WP]  Upgrade to Why3 1.5.1

Frama-C General

Bug Fixes

• [Kernel]  Reject array whose size is too big with a proper error message instead of a crash (fixes #2590)
• [Kernel]  Reject array whose size is too big with a proper error message instead of a crash (fixes #2590)
• [Kernel]  Reject programs using unsupported vector_size attribute (fixes #2573)
• [Kernel]  Fix list of potential types for decimal integer literal constants
• [Logic]  Fix type of expressions whose value are functions

Developers Only

• [Kernel]  Integer.pretty does not have the optional argument hexa anymore. Use Integer.pretty_hex or Integer.pp_hex if you want to print integers in hexadecimal format.
  
  
• [Kernel]  Remove unused AST node Dcustom_annot and field fpadding_in_bits. Do not cache size of types in the AST but in a dedicated table.
• [Kernel]  Removed obsolete AST nodes IndexPI and Info
• [Kernel]  Remove State_selection.Static (deprecated since 10 years, use directly State_selection instead)
• [Kernel]  New visitor functions visitFramacFileFunctions and visitCilFileFunctions to visit only function definitions, for better performance.
• [Kernel]  Known compiler builtins are no longer hardcoded in OCaml, but defined via JSON files (in share/compliance).
• [Kernel]  Prototype of AST comparison between two versions of the same program, via the new option -ast-diff.

Plugin E-ACSL

New Features

• [E-ACSL]  Add Linux's pthread concurrency support.
• [E-ACSL]  Improve translation of `\at()` terms and predicates (#108).
• [runtime]  Improve runtime debug logs: the %a modifier now outputs in hexadecimal, the debug logs now all end in new lines, the trace now outputs to stderr.

Bug Fixes

• [E-ACSL]  Now the same Frama-C options are used when parsing the user sources and the E-ACSL's RTL.
  
  
• [E-ACSL]  Add support for VDSO segment on Linux.
• [E-ACSL]  Fix crash when binding a lambda-abstraction to a local variable (#189).
• [E-ACSL]  Fix crash when creating an axiomatic with an existing name in E-ACSL's RTL (#161).
• [E-ACSL]  Fix normalization of global annotations that may lead to crashes (#195).
• [E-ACSL]  Fix wrong cast of pointer to integer (#1119).
• [E-ACSL]  Fix crash for quantifications over enum types (#199).
• [e-acsl-gcc]  Fix e-acsl-gcc.sh detection of failures in subcommands.
• [e-acsl-gcc]  Fix e-acsl-gcc.sh bash autocompletion script and install it at a standard location.
• [runtime]  Fix default stack size: E_ACSL_STACK_SIZE is now correctly used by the runtime, the default values have been adjusted to what was effectively used.

Plugin Eva

• Fixes stack overflow errors on very large C functions.
• Improve the multidim abstract domain: it is now more precise and more robust, it is able to infer simple array invariants on some loops without unrolling, and has a new option -eva-multidim-disjunctive-invariants to infer structures disjunctive invariants.
• New API to run the analysis and access its results, intended to replace the old API in Db.Value. It is more precise as it uses all available domains to evaluate values and locations. See file Eva.mli for more details.

Plugin WP

New Features

• [TIP]  Extended Split tactic: can split in hypotheses, can split conjunctions into multiple hypotheses.
• [TIP]  New tactic Clear: remove hypothesis
• [TIP]  New tactic Mod-Mask: rewrite bitmask into/from modulo
• [WP]  Removed legacy WP engine and option -wp-legacy
  
  
• [WP]  Weakened loop invariant verification (in particular for check loop invariant)
• [WP]  Supported decreases clause
• [WP]  Supported general variant measure
• [WP]  Removed deprecated "native:alt-ergo" prover
• [WP]  Removed deprecated "native:coq" prover
• [WP]  New option -wp-smoke-dead-local-init, smoke tests on local variables initialization
• [WP]  New option -wp-fct-timeout, used to customize the provers timeout per function
• [WP]  Upgrade to Why3 1.5

Bug Fix

• [WP]  Fixed loop invariant order

Frama-C General

New Features

• [ACSL]  better type checks for volatile clauses
• [Kernel]  0-sized flexible array members only available in gcc_* machdeps, that now also support FAM in nested struct.
• [Kernel]  Support for C11's _Static_assert
• [Libc]  Frama-C's libc #define _STDC_NO_COMPLEX as mandated by ISO C11 for libraries without support for complex numbers

Bug Fix

• [Kernel]  Fixes crashes on C integer constants overflowing ocaml integers.

Developers Only

• [Kernel]  New module Cil_builder, simplifies C and ACSL code generation.
• [Ptests]  Add new PLUGIN directive and new predefined macros.

Plugin E-ACSL

New Features

• [E-ACSL]  Support for \sum.
• [E-ACSL]  Correct monitoring of code depending on libc function calls that write memory locations (#157).
• [E-ACSL]  Support for \prod and \numof.
• [E-ACSL]  Add option -e-acsl-assert-print-data (--assert-print-data in e-acsl-gcc.sh) to print data contributing to a failed assertion along with the error message. Add option --external-print-value in e-acsl-gcc.sh to provide a custom implementation of __e_acsl_print_value().

Bug Fixes

• [E-ACSL]  Do not translate contracts of E-ACSL built-ins.
  
  
• [E-ACSL]  Fix pointer address on memory annotations with range indices (#148).
• [E-ACSL]  Fix literal string replacements in function arguments during a local initialization.
• [E-ACSL]  Fix a crash that occured when using certain combinations of nested blocks and annotations.
• [E-ACSL]  Fix crash when using some built-in labels (#173).
• [E-ACSL]  Fix crash when raising some user errors (#170).
• [E-ACSL]  Fix crash occurring when two or more successive logic coercions were done in a term (#172).
• [E-ACSL]  Fix incorrect evaluation of quantified predicates when a strict guard overlaps with the type of the bound variable (unlikely in practice) (#149).
• [E-ACSL]  Fix unsound reuse of previously typed recursive functions (#177)
• [E-ACSL]  Fix translation order of the default behavior's requires clauses. They are now translated before the evaluation of the assumes clauses of the other behaviors.
• [E-ACSL]  Fix code generation of properties proven invalid with a previous analysis (#166).

Plugin Eva

New Features

• Support for ACSL predicate \is_infinite.
  
  
• New taint analysis via an experimental taint domain. New annotations //@ taint … (for statements) and //@ taints … (in function contracts) to initiate taint on lvalues. Tainted properties can then be seen in the future GUI Ivette.
• New annotation dynamic_split, similar to split, but separates the analysis w.r.t. the current value of an expression instead of the value it had at the annotation point: the partition can be changed at an assignment to ensure that the expression always evaluates to a singleton in each analysis state.
• Annotations split and dynamic_split can be applied to logic predicates (in addition to terms).
• New experimental multidim domain to improve analysis precision on arrays of structures and multidimensional arrays.
• Reduction of "garbled mix" values by \valid and \valid_read ACSL predicates.
• New \tainted predicate to evaluate if the value of an expression is tainted according to the taint domain.
• Removes the maximum limit of option -eva-ilevel.
• Improves the symbolic-locations domain precision.
• Improves the precision of the octagon domain on unsigned variables.
• On a SIGINT signal (Ctrl-C), the analysis is stopped but partial results are saved if option -save is set.
• Supports the evaluation of ACSL set comprehension.
• New options to allow states partitioning to survive function returns: -eva-interprocedural-split for disjunctions from split annotations, and -eva-interprocedural-history for disjunctions from the -eva-partition-history option.

Bug Fixes

• Fixes a crash in the octagon domain.
• Fixes a soundness bug of the bitwise domain with the memexec cache.
• Fixes a soundness bug in the octagon domain on integer downcasts wrapping around.
• Always checks the arguments of builtin calls for alarms about initialization, escaping pointers and special floating-point values, unless -eva-warn-copy-indeterminate is set.
• Always emits alarms about initialization, escaping pointers and special floating-point values for the arguments of calls to functions without body (or whose body is not analyzed), even when -eva-warn-copy-indeterminate is unset.

Developers Only

• Changes the Domain_builder.Complete functor to automatically build more abstract domain functions.

Plugin Variadic

• translates printf/scanf calls even if formatting string is not constant, warning that it will assume arguments match the format.
• Create a fallback specialisation if there is an error while translating a variadic call so that no variadic call are left in the AST after Variadic.

Plugin WP

• [TIP]  Generalized Overflow tactic
  
  
• [WP]  Removes -wp-overflows option (unsound)
• [WP]  Adds an experimental support of "terminates" clauses. Adds the options -wp-declaration-terminate and -wp-frama-c-stdlib to claim that external functions terminates. Adds -wp-definitions-terminate option to claim that defined function terminates. Adds -wp-variant-with-terminates to verify loop variants under the termination hypothesis.
• [WP]  -wp-smoke-tests detects incoherent assumes when no requires are specified, can be disabled with new option -wp-smoke-dead-assumes

Plugin E-ACSL

• [E-ACSL]  Fix crash occurring when two or more successive logic coercions were done in a term (#172).
• [E-ACSL]  Fix crash when raising some user errors (#170).
• [E-ACSL]  Fix crash when using some built-in labels (#173).
• [E-ACSL]  Fix crash when encountering a GMP value in a loop variant (#169).
  
  

Plugin WP

• [WP]  Fix a crash related to opaque structures memory typing
  
  

Frama-C General

New Features

• [ACSL]  New admit annotations to express hypotheses to be admitted but not verified by Frama-C.
• [Kernel]  Allow -add-symbolic-path to survive saves/loads and invert argument order (path:name).
• [Kernel]  Set default machdep to x86_64 (was x86_32); allow setting machdep via environment variable FRAMAC_MACHDEP.
• [Libc]  Remove obsolete attribute FRAMA_C_MODEL in the libc. Fixes #877.
• [Libc]  In math.h specifications, new behaviors for cases creating NaN or infinite values. These behaviors are allowed or forbidden according to the -warn-special-float option.

Bug Fixes

• [Kernel]  Raise an error if trying to merge a tentative definition with a proper definition during linking
• [Kernel]  Pretty prints array formals in their original form. Fixes pub/frama-c#392
• [Kernel]  Do not crash on _Alignof(void): accept or properly reject, depending on machdep. Fixes pub/frama-c#2551
• [Logic]  The assigns clause can't mention const locations anymore. Fixes #855.

Developers Only

• [Kernel]  Extract builtin-related functions from module Cil to module Cil_builtins. Code can be updated using `bin/migration_scripts/titanium2vanadium.sh`.
• [Kernel]  Make cfields list optional. None means undefined, empty struct allowed only in specific machdeps. removed cdefined field
• [Kernel]  Avoid triggering warning 16 (unerasable optional argument). Implies changing some labeled functions' signatures.
• [Kernel]  Change the type of the measure from string to logic_info in the variant AST node.
• [Kernel]  Filepath directories functions now return Filepath.Normalized.t, Frama-C configuration and plugin configuration getters updated accordingly
• [Kernel]  Removed deprecated function Filepath.pretty
• [Ptests]  Add new EXIT directive.
• [Ptests]  Modify MODULE directive.
• [Ptests]  FILTER directive reads the standard input and can be chained.

Plugin Aorai

• New option for tracking last N states of the automaton. Easier analysis of instrumented code with Eva.

Plugin E-ACSL

New Features

• [E-ACSL]  Update e-acsl-gcc.sh so that the library dlmalloc can be compiled and used from sources.
  
  
• [E-ACSL]  Add RTL support for Windows.
• [E-ACSL]  Add support for `check` and `admit` annotations (#142).
• [E-ACSL]  Add support for multiple binders in guarded quantifications (#127).
• [E-ACSL]  Add support for loop variant.
• [e-acsl-gcc]  Do not load Frama-C plugins when retrieving share and plugins paths (#104).
• [e-acsl-gcc]  Deactivate Variadic translation when using incompatible option --validate-format-strings (#104).
• [e-acsl-gcc]  Remove obsolete options from documentation and bash completion script (#104).
• [e-acsl-gcc]  Try to find Frama-C binary in script or development directory if not present in PATH (#104).

Bug Fixes

• [E-ACSL]  Fix crash when comparing two structs, which is currently unsupported (#139).
• [E-ACSL]  Fix crash when running another analysis after E-ACSL caused by E-ACSL breaking some internal kernel invariant (#145).
• [E-ACSL]  Fix wrong computation of the base pointer when calling \valid predicate leading to undetected array overflows.
• [E-ACSL]  Restore behavior of option -e-acsl-no-valid broken since Titanium (included).
• [Makefile]  Fix dependencies in bytecode-only compilation.
• [runtime]  Fix integration of contracts from the runtime library into Frama-C (#999).
• [runtime]  Fix the end address of the memory segments in the RTL layouts.
• [runtime]  Fix incorrect check on program arguments when the main function takes no arguments (#151).
• [runtime]  Fix backtrace output on failed assertion (#151).

Plugin Eva

New Features

• Allow using Eva directives Frama_C_show_each and Frama_C_dump_each in ghost code.
• Better interpretation of logical operators && and || (useful when option -keep-logical-operators is enabled).
• Improved automatic widening thresholds (widen hints): use constant modulo as threshold, and infer thresholds globally for global variables.
• New "audit mode" to track file checksums, correctness options and enabled warnings, via options -audit-prepare and -audit-check.
• Slightly more precise evaluation of ACSL quantifiers.
• Improved automatic loop unroll (-eva-auto-loop-unroll option) of loops with goto or continue statements, or assigning constant values to loop variants.
• 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. The unsound option -eva-ignore-recursive-calls has been removed.

Bug Fix

• Fixes a crash when subdividing the evaluation of pointer expressions (via option -eva-subdivide-non-linear).

Developers Only

• New signature for builtins, that are now registered via Eva.mli instead of Db.Value.

Plugin Metrics

• Add json output in addition to text and html.
  
  

Plugin RTE

• -rte-initialized takes a set of functions as parameter (defaults to none)
• No more initialization warnings for full structures and unions reads. Initialization warnings for other types *without* trap representation. Refer to the documentation for more details.
• Remove spurious assert when comparing function pointer to NULL (fixes #940)

Plugin WP

New Features

• [TIP]  New tactic: Induction
• [TIP]  New tactic: Sequence unrolling
• [WP]  Removed option -wp-bits (now always enabled)
  
  
• [WP]  Improved -wp-unfold-assigns <depth> Now recursively applies to all compounds
• [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.
• [WP]  Section « Limitation & Roadmap » added to the WP manual.

Bug Fix

• [WP]  Fixes opaque structures handling

Frama-C General

• [ACSL]  Allows for axiomatic blocks-like extensions
• [Dev]  Support for OCamlGraph 2.0.0
• [Kernel]  Support for C11's _Noreturn function specifier
  
  
• [Kernel]  New option -explain, which provides help messages for options used on the command line.
• [Kernel]  Support for C11's _Thread_local storage specifier
• [Kernel]  OCaml version greater than or equal to 4.08.1 required.
• [Kernel]  Add option -print-cpp-commands, to print the preprocessing commands used by Frama-C.
• [Kernel]  Option -permissive now allows non-existent option names.
• [Kernel]  New option -autocomplete p1, ..., pn that list the options of plug-ins p1, ..., pn in a format suitable for autocompletion scripts.
• [Kernel]  Add option -print-config-json, to output Frama-C configuration data in JSON format.
• [Logic]  Introduce check-only annotations for requires, ensures, loop invariant and lemmas
• [Logic]  '\from' now accepts '&v' expressions

Plugin Aorai

• Ya automata can set auxiliary variables during a transition, and use such variables in subsequent guards.

Plugin E-ACSL

New Features

• [E-ACSL]  Add support to create GMP rational from GMP integer (#120).
• [E-ACSL]  Add support of bitwise operators (#33).
• [E-ACSL]  Add support for logical array comparison (#99).
• [E-ACSL]  Remove option -e-acsl-check.
• [E-ACSL]  Remove option -e-acsl-prepare-ast.
• [E-ACSL]  Deprecate -e-acsl-full-mmodel in favor of -e-acsl-full-mtracking.
• [E-ACSL]  Support of complete and disjoint behavior (#92 and #27).
• [E-ACSL]  Add support for the `\separated` predicate. (#31)
• [E-ACSL]  Support for Variadic generated functions in the AST (#128).
• [e-acsl-gcc]  Deprecate --full-mmodel in favor of --full-mtracking.

Bug Fixes

• [E-ACSL]  Fix support of VLA memory tracking (#119).
  
  
• [E-ACSL]  Decrease the number of allocated blocks when one block is freed.
• [E-ACSL]  Fix translation of trange (incorrect length).
• [E-ACSL]  Fix unstable order of generated globals (#124).
• [E-ACSL]  Fix crash that may occur when translating properties that have been proved valid by another plug-in (#106).
• [E-ACSL]  Fix a soundness bug when translating a range with a logic variable.
• [E-ACSL]  Fix soundness bug when checking initialization of a chunk of heap memory block.
• [runtime]  Fix wrong value returned for the stack size in the segment memory model (#126).

Plugin Eva

New Features

• Supports the ACSL mathematical operator \abs
• New option -eva-alloc-builtin to configure uniformly the behavior of allocation builtins, instead of providing several builtins with different behaviors for malloc/calloc/realloc.
• New annotation eva_allocate to configure the behavior of an allocation builtin for a call, overriding 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.
• Deprecates legacy options aliases -val-* in favor of option names -eva-*.

Bug Fix

• Improved string builtins on wide strings: crash fixed, better performance, misaligned pointers now considered invalid.

Plugin MdR

• Update Sarif output to 2.1.0 + prettier URI

Plugin Metrics

• Distinguish between undefined but specified functions and functions with neither definition nor specification.

Plugin Slicing

• Better handling of invalid command line options.

Plugin Variadic

• Don't print generated function name but print original name and a comment with the generated name so that the printed code is compilable.

Plugin WP

• [WP]  Supports the \initialized ACSL predicate
  
  
• [WP]  New option -wp-cache-print
• [WP]  Option -wp-cache-env now defaults to false
• [WP]  Removed debug keys "no-xxx-info" (subsumed by "shell")
• [WP]  Support for generalized @check ACSL annotations
• [WP]  Hypotheses: assigned memory locations
• [WP]  New experimental option: -wp-check-memory-model Insert function contracts for model hypotheses
• [WP]  New option -wp-interactive-timeout <seconds>
• [WP]  New option -wp-interactive <mode>
• [WP]  Added support for Why3 Coq interactive prover
• [WP]  Added support for Why3 interactive prover (Coq)
• [WP]  New tactic Bit-Test range
• [WP]  Hypotheses: out pointers (\result + written pointers)
• [WP]  New warning "pedantic-assigns". WP needs precise 'assigns ... \from ...' specification about out pointers (\result and assigned pointers) to generate precise proof hypotheses.

Plugin WP

• [WP]  Fixes Coq region function
• [WP]  Fixes MemTyped structure loader for wp-rte
  
  

Frama-C General

New Features

• [ACSL]  Make conversion from C ptr to logic array explicit
• [Kernel]  -constfold now takes into account value of const globals
• [Kernel]  checks that ghost code does not modify the normal control flow of the non-ghost program
• [Kernel]  support for ghost else blocks
• [Kernel]  Add option -cpp-extra-args-per-file
• [Kernel]  New option -warn-pointer-downcast (activated by default), to warn when a conversion between pointer and integer might provoke a loss of precision.
• [Kernel]  New option -warn-invalid-pointer (disabled by default) to warn on invalid pointer arithmetics resulting in a pointer that does not point to an object or one past an object.
• [Kernel]  Report user errors when keys are not bound to a value for command-line options that require pairs of key:value as arguments. Such keys were silently ignored.

Bug Fixes

• [Doc]  Fixes internal refs in generated pdfs (fixes #2505)
• [Kernel]  fixes issue that could prevent loading plug-ins on Windows installation
• [Kernel]  Fixes #818 (term generated for downcast alarms)
• [Kernel]  Fixes #823 (-load-module/-load-script now accept spaces in filename)
• [Kernel]  Reject labels at end of blocks.
• [Kernel]  Accept UCN-encoded unicode char in ACSL (fixes #849)

Developers Only

• [ACSL]  Add possibility for ACSL extensions to alter the sequence of untyped terms they receive from the parser. Make also possible to customize the short pretty printer of extensions.
• [Kernel]  Removed FCBuffer, FCMap and FCSet. Use directly OCaml stdlib modules Buffer, Map and Set instead.
• [Kernel]  Deprecated: - Logic_typing.register_*_extension - Cil_printer.register_*_extension - Cil.register_behavior_extension Use Acsl_extension.register_* instead
• [Kernel]  Plug-ins specific dirs now use Filepath instead of mere strings.

Frama-C GUI

• [Gui]  Fix order of globals in the source panel.

Plugin E-ACSL

New Features

• [E-ACSL]  Improve verdict messages emitted by e_acsl_assert.
• [E-ACSL]  Call `__e_acsl_memory_init` only if the memory model analysis is running.
• [E-ACSL]  Call E-ACSL's free functions for globals in a separate function at the end of main.

Bug Fixes

• [E-ACSL]  Fix bug with compiler built-ins.
  
  
• [E-ACSL]  Fix typing bug in presence of variable-length arrays that may lead to incorrect generated code.
• [E-ACSL]  Fix '1386' and #91 about the tracking of variables declared inside the body of switches.
• [E-ACSL]  Fix #105 about misplaced `__e_acsl_delete_block` in presence of gotos to return statements.
• [E-ACSL]  Fix automatic deactivation of plug-in Variadic when E-ACSL is directly called from Frama-C without using e-acsl-gcc.sh.
• [E-ACSL]  Fix a soundness bug (#14) when initializing rationals from integers.
• [E-ACSL]  Fix #13: bug when mixing integers and floats in annotations while -e-acsl-gmp-only is activated.

Plugin Eva

New Features

• Subdivisions can now be enabled locally: - through the new option -eva-subdivide-non-linear-function that overrides the global option for the given functions; - via /*@ subdivide N; */ annotations on specific statements.
  
  
• Adds consistency checks on return and parameters types between a builtin and the replaced C function.
• Renamed option -eva-malloc-functions into -eva-alloc-functions. Also contains calloc and realloc by default.
• Supports the logic evaluation of quantifiers introducing mathematical variables (integer or real).
• New option "-eva-domains <d1>,<d2>,..." to enable several domains at once. The list of available domains is given in the help message of the option.
• Slightly better heuristics for the subdivision of evaluations (option -eva-subdivide-non-linear).
• Evaluates the logic predicate memchr_off, used in Frama-C libc specifications.
• deprecate options -eva-*-domain in favor of -eva-domains
• Supports the ACSL extended quantifiers \min and \max.
• Emits alarm on pointer downcast when option is on
• Emits alarm on invalid pointers when option is on
• New experimental builtins for dynamic allocation Frama_C_*alloc_imprecise: faster convergence, but very imprecise.
• New option -eva-domains-function to enable domains only on given functions. Argument <d:f> enables the domain [d] on function [f], while <d:f+> also enables it on all functions called from [f]. <d:f-> disables [d] from function [f].
• Fixes the Memexec cache on functions with logical annotations about variables unused in the C body of the function.

Bug Fix

• Fixes the evaluation of logic predicates involving empty sets.

Developers Only

• Simplifies abstract domain signature by removing the Transfer functor.

Plugin Instantiate

• New plug-in Instantiate, to create function specializations for specific plug-ins and functions (e.g. malloc, memcpy, memset), to overcome limitations due to their specifications.

Plugin RTE

• Emits alarm on invalid pointers when option is on
• Emits alarm on pointer downcast when option is on

Plugin WP

• [TIP]  Extends bitwise tactics to dis-equalities
• [TIP]  Refactor structure of session directory (remove models)
• [TIP]  Specification of JSON script format
• [TIP]  Create session directory only on demand
• [WP]  Additional lemmas about logical shift compositions
  
  
• [WP]  Additional lemma about remainder (mod)
• [WP]  Limit the number of splits (see -wp-max-split)
• [WP]  Emit a warning when no goal is generated
• [WP]  Checks for inconsistent requires (-wp-smoke-tests)
• [WP]  Added option -wp-run-all-provers
• [WP]  Fix drivers in different projects
• [WP]  Control splitting with -wp-max-split <n>
• [WP]  Extended frame conditions with global C-types
• [WP]  Extended frame conditions to pointers inside compound
• [WP]  Move frame conditions to Type section for better filtering
• [WP]  Update scripts with FRAMAC_WP_SCRIPT=update and -wp-prover script
• [WP]  Specify cache mode with FRAMAC_WP_CACHE=<mode> (-wp-cache-env)
• [WP]  Fixes handling of LoopCurrent in loop invariants
• [WP]  Why3 prover full-names use ':' instead of ','
• [WP]  Why3 prover version fallback
• [WP]  Fixed scope problem on block outgoing edge
• [WP]  Added support for invalid-pointer predicate
• [WP]  Added smoke tests for dead loop (-wp-smoke-dead-loop)
• [WP]  Added smoke tests for dead code (-wp-smoke-dead-code)
• [WP]  Added smoke tests for dead call (-wp-smoke-dead-call)
• [WP]  Removed option -wp-check
• [WP]  Full support for Why3 IEEE float library

Frama-C General

New Features

• [ACSL]  Support for ghost parameters
• [Kernel]  Improve placeholders handling in -cpp-command
• [Kernel]  OCaml version greater than or equal to 4.05.0 required.
• [Kernel]  Add -keep-unused-types normalization option
• [Kernel]  Supports macro INFINITY and NAN.
• [Kernel]  More stringent verifications on the use of ghost variable in non ghost-code. Fixes #2421
• [Libc]  Remove obsolete (and forcing cpp error) builtins.h

Bug Fixes

• [Kernel]  fixes dangling ref when removing unused static local
  
  
• [Kernel]  Fixed sequence of -removed-projects and -then options.
• [Kernel]  Fixes a rare but critical bug which occured when Frama-C internally switched the current project in presence of >2 projects and destroyed the old current project at about the same time: the Frama-C internal state became inconsistent and lead to unsound computations and crashes. It may be revealed to the end-user when using a long sequence of -then-replace (at least 3 of them).
• [Kernel]  Fixes Hptmap on keys with id greater than 2^28.
• [Makefile]  Fixes #2378 - bytecode only compilation (patch contributed by madroach) and use -thread where needed.

Developers Only

• [Kernel]  removes AST constructors TCoerce, TCoerceE, PLCoercion, PLCoercionE, Psubtype and PLsubtype
• [Kernel]  Types in Properties are now records and not tuples
• [Kernel]  Functions over visitor's behaviors have been moved from Cil into a new module Visitor_behavior. Apply the migration script potassium2calcium.sh to update your plug-ins automatically.
• [Ptests]  Add new MODULE directive for compiling and loading an auxiliary OCaml module for a test

Plugin Config

• ocp-indent 1.7.0 is now used for indentation

Plugin E-ACSL

• [E-ACSL]  Support of rational numbers and operations.
• [E-ACSL]  Deactivate the unsound support of real numbers (that are not rationals). They were previously unsoundly converted to floating point numbers.
  
  

Plugin Eva

New Features

• Supports ACSL floating-point comparison operators eq_float, le_float, eq_double, le_double, etc.
• Evaluates ACSL predicates \is_plus_infinity and \is_minus_infinity.
• New octagon domain inferring relations of the form l ≤ ±X±Y ≤ e between pairs of integer variables X and Y. Enabled with option -eva-octagon-domain. Only infers relations between pairs of scalar variables occuring in a same instruction. Intra-procedural by default; octagons can be propagated through function calls with option -eva-octagon-through-calls.
• New option -eva-auto-loop-unroll N to unroll all loops whose number of iterations can be easily bounded by <N>.
• In the summary, fixes the total number of functions (and thus the computed analysis coverage).
• In the summary, fixes the number of alarms by category when the RTE plugin is used, and do not count logical properties in dead code as proven.

Bug Fix

• Fixes the reduction by the negation of \initialized and \dangling predicates on imprecise lvalues.

Developers Only

• Dynamic registration of abstract values and domains: developers of new domains no longer need to modify Eva's engine.

Plugin MdR

• New plug-in Markdown-Report (MdR) for markdown and SARIF outputs

Plugin Sparecode

• Removed from Db. Use proper Sparecode API instead.

Plugin WP

New Features

• [GUI]  Updated panel for provers, models, cache, etc.
• [Qed]  Transform (some) boolean quantifications into variable assignments
  
  
• [TIP]  Using all selected Why-3 provers for proof search
• [WP]  Improving Cint simplifier and quantifier introduction
• [WP]  Use native Why3 API (now requires why3 at compile time)
• [WP]  Default -wp-prover <p> changed to <why3:p> (including default alt-ergo)
• [WP]  Default -wp-init-const changed to true
• [WP]  Default -wp-extensional changed to true
• [WP]  Removed -wp-depth
• [WP]  Removed -wp-why-lib
• [WP]  Removed -wp-why3
• [WP]  Removed -wp-include
• [WP]  Renamed -wp-init-alias into -wp-alias-init
• [WP]  Renamed -wp-why-opt into -wp-why3-opt
• [WP]  Deprecated & Renamed -wp-hints into -wp-coq-hints
• [WP]  Deprecated & Renamed -wp-tryhints into -wp-coq-tryhints
• [WP]  Deprecated & Renamed -wp-tactic into -wp-coq-tactic
• [WP]  Deprecated & Renamed -wp-update-script into -wp-update-coq-script
• [WP]  Deprecated & Renamed -wp-script into -wp-coq-script
• [WP]  Deprecated native alt-ergo & coq output, see -wp-prover option
• [WP]  New cache mechanism for why3 provers, see -wp-cache option

Developers Only

• [Qed]  More secure API for quantifier management

Frama-C General

New Features

• [ACSL]  Clarifies which C variables are in scope under a \at(·,L) (#575)
• [ACSL]  Add check annotation, similar to assert except that it does not introduce additional hypotheses on the program state
• [Kernel]  Improved precision of integer abstract bitwise operators.
• [Kernel]  Add statement attributes (sattr) to the AST. They are not printed by default, use -kernel-msg-key printer:attrs
• [Kernel]  Add attributes for loop statements to allow distinguishing between for, while and dowhile loops.
• [Libc]  Ask clang not to warn about unknown FRAMA_C_MODEL attribute when pre-processing frama-c's libc
• [Libc]  Better specs and removal of half-implemented ifdef that tried to take various POSIX versions into account

Bug Fixes

• [ACSL]  Accept C identifiers that happen to be ACSL keywords in volatile and reads clauses
• [Kernel]  Fixes #553 - pretty-printing of basic asm template
  
  
• [Kernel]  Fixes AST integrity check wrt volatile accesses
• [Kernel]  Better detection of invalid goto in presence of VLA (fixes #499)
• [Kernel]  Avoid crashing on one-letter attributes. Fixes #2432
• [Makefile]  Do not attempt to install .cmx on bytecode-only architectures. Patch by M. Dogguy backported from Debian package

Developers Only

• [Kernel]  New functions for retrieving major and minor version
• [Kernel]  Integer API moving closer to Zarith
• [Kernel]  When registering extended ACSL annotations, one must now indicate whether they should have a status.

Frama-C GUI

• [Gui]  Compatibility with lablgtk3 and improved handling of some widgets

Plugin Aorai

• Fixes #586: avoid removing the initial state of the automaton

Plugin E-ACSL

New Features

• [E-ACSL]  Predicates with empty quantifications directly generate \true or \false instead of nested loops.
  
  
• [E-ACSL]  New option -e-acsl-functions to monitor only annotations in a white list of functions.
• [E-ACSL]  New option -e-acsl-instrument to instrument only a specified set of functions. It may lead to incorrect verdicts.
• [E-ACSL]  Support for logic functions and predicates without labels.
• [runtime]  The behavior of __e_acsl_assert now depends on the runtime value of the global variable __e_acsl_sound_verdict: if 0, it means that its verdict is possibly incorrect.

Bug Fixes

• [runtime]  Fix overlap of TLS with other memory segments for large memory spaces.
• [runtime]  Fix initialization of the E-ACSL runtime in presence of multiple calls to its initializer (for instance, if the main is a recursive function).

Plugin Eva

New Features

• Improved precision on nested loops (by postponing the widening on inner loops according to -eva-widening-period).
• Ignore annotations with "no_eva" tag
• New warning category for detecting loops without 'unroll' directive
• New option -eva-precision to globally configure the analysis from 0 (fast but imprecise) to 11 (accurate but slow). A precision of 5 is often a reasonable trade-off. This meta-option automatically sets up other options that can also be overriden.
• Prints an analysis summary at the end, outlining the analysis coverage and the number of errors, warnings and emitted alarms. It can be disabled with the option -eva-msg-key=-summary
• Loop unroll annotations now accept non-constant but bounded expressions as the maximum number of unrollings to perform.
• New option -eva-partition-history N to delay the join of abstract states for up to N merging points, thus keeping these states separate longer. Useful when a reasoning depends on the path taken to reach a control point, but can increase the analysis time exponentially in N.
• The new annotation /*@ split exp; */ enumerates the possible values of an expression and continues the analysis for each of these value separately, until a /*@ merge exp; */ is encountered. It is also possible to maintain this partitioning at all times with the option -eva-partition-value exp.

Bug Fix

• Fixes -eva-split-return on uninitialized or escaping function returns when -eva-warn-copy-indeterminate is disabled.

Plugin Inout

• Fix performance issue when initializing large arrays.
• Fixes operational input on const local initialization

Plugin Obfuscator

• Also obfuscate formals in function pointer types. Fixes #2433.
• Obfuscate logic types and logic constructors.

Plugin RTE

• fixes a crash when visiting variable declarations
• RTE has a static API

Plugin WP

• [Qed]  New simplifications for validity and ranges
• [Qed]  Extends simplifications for lsl,lsr and div
• [TIP]  New tacticals for validity and ranges
  
  
• [TIP]  New tactical Congruence (divisions and products)
• [TIP]  Fix bug that makes the TIP wrongly reuse previous results
• [TIP]  New Strategies for bitwise and congruence operations
• [TIP]  Auto-Search mode from the GUI
• [TIP]  Fix wrong reconciliation of sub-scripts during replay
• [TIP]  Extend bitwise-eq auto-strategy on hypotheses
• [WP]  Auto filter properties with name "no_wp:"
• [WP]  Filter out some variables from separation
• [Wp]  Fix soundness bug when assigning non-valid ranges
• [Wp]  Option -wp-unfold-assigns for proving assigns of aggregates field by field
• [Wp]  Option -wp-print-separation changed into -wp-warn-separation
• [Wp]  Auto-Search mode, see -wp-auto
• [Wp]  New floating-point model
• [Wp]  Now -wp-dynamic is set by default (annotation @calls)
• [Wp]  Better naming convention, consistent with report-classify
• [Wp]  Support for @check ACSL annotations
• [Wp]  Support for Why3 1.* and Coq 8.{7-9}
• [Wp]  Removed option -wp-bool-range
• [Wp]  Now requires -warn-invalid-bool
• [Wp]  Fixes -wp-simplify-is-cint simplifier

Frama-C General

New Features

• [ACSL]  Introduce extensions to global annotations and better characterization of each extension kind. See development guide for more information
• [Kernel]  New option -remove-inlined to remove function(s) after -inline-calls, add category @inline to refer to all functions with inline attribute (for both options).
• [Kernel]  Fix compilation on OpenBSD patch contributed by madroach. Fixes #2379
• [Kernel]  Remove option -const-writable: const globals are unconditionally constants
• [Kernel]  Introduce Filepath dataype for more consistent normalization of filenames
• [Kernel]  New options -warn-left-shift-negative (enabled by default) and -warn-right-shift-negative (disabled by default), to control the emission of alarms on shifts on negative integers.
• [Kernel]  New warning (disabled by default) when multiple side effects are unsequenced (CERT-EXP10-C recommandation). Fixes #492
• [Kernel]  New option -warn-invalid-bool, to warn when reading trap representations of type _Bool.
• [Kernel]  More ergonomic command-line options for governing warning categories statuses.
• [Kernel]  Log.error and Log.failure will eventually make Frama-C exit with a non-zero status. Fixes #552

Bug Fixes

• [ACSL]  introduce ACSL operators \le_double, \ge_double, ... in addition to \le_float, \ge_float, ... Remove overloading of \le_float that made it accept double as arguments. Fixes #502
• [ACSL]  Avoid removing cast of void ptr used as argument of function expecting a ptr with known size. Fixes #432
• [Kernel]  Respect relative order of labels and ACSL annots. Fixes #524
• [Kernel]  Do not allow compound assignments to const variables Fixes #384
• [Kernel]  Add attribute to allow writing into const lvals in specific (aka C++ constructors and mutable fields) circumstances. Fixes #2395.
• [Kernel]  Rejects sizeof of an incomplete type. Fixes #560.
• [Kernel]  Consider that asm can change content of pointers used as inputs when generating assigns clauses. Fixes #458
• [Kernel]  Fixes parsing of compound initializers with anonymous fields. Fixes #2384

Developers Only

• [Kernel]  Remove completely outdated module Dataflow. Deprecated since 3+ years. Use Dataflow2 instead.
• [Ptests]  Do not keep oracles for empty stderr. Fixes #402

Plugin Constant Propagation

• Removing Db API for Constant Propagation plug-in. Calls to !Db.Constant_Propagation should be replaced by calls to Constant_Propagation.Api.

Plugin E-ACSL

New Feature

• [E-ACSL]  Support for ranges in memory builtins (\valid, \initialized, etc).
  
  

Bug Fixes

• [E-ACSL]  Fix bug #2305 about taking the address of a bitfield.
• [E-ACSL]  Support for \at on purely logic variables. Fix bug #1762 about out-of-scope variables when using \old.
• [E-ACSL]  Fix bug #2386 about incorrect typing when performing pointer subtraction.
• [E-ACSL]  Fix bug #2406 about monitoring of variables with incomplete types.
• [E-ACSL]  Fix typing bug in quantifications when the guards of the quantifier variable cannot be represented into its type.
• [runtime]  Fix bug #2405 about memory initialization in presence of GCC constructors.

Plugin Eva

New Features

• New propagation strategy that allows unrolling loops even when the slevel has been exceeded. Unroll the N first loop iterations via the global option -eva-min-loop-unrolling N or via specific code annotations /*@ loop unroll N; */. The new strategy may affect analyses even without loop unrolling.
  
  
• Renamed option -wlevel into -eva-widening-delay. New option -eva-widening-period to control the number of iterations between two widenings.
• Improved precision of string builtins for strlen, strchr and memchr.
• The variables from the frama-c libc are no longer shown in the initial state print.
• When a cvalue builtin is used, other domains use the frama-c libc specification to interpret the call without losing too much information.
• Release all builtins, including memset and memcpy, as open-source.
• New option -eva-report-red-statuses listing in a csv file the properties invalid for some states of the analysis (as in the "Red Alarms" panel of the GUI).
• The debug category "garbled-mix" becomes a warning category. Better track of garbled mix created by specification.
• Rename plug-in shortname from 'value' to 'eva'. Eva is now properly named Eva in all logs, in the GUI, and as the emitter of the alarms.
• All options of Eva start with -eva. Aliases to previous option names preserve backward compatibility.
• Fixes the alarms on subtractions and comparisons of pointers on weak bases (created by allocations in loops).
• Supports the ACSL functions \min and \max.
• Better reduction of floating-point values cast into integer types when an alarm is emitted.
• Reduction of values leading to division by zero alarms, when possible.
• Remove option -val-warn-left-shift-negative, and comply with kernel option -warn-[left|right]-shift-negative.
• Some fixes and improvements of the equality domain.
• Fix the gauges domain on weak bases.
• Warn about currently unsupported specifications of some libc functions.
• ACSL predicates with a "no_eva" tag are now ignored.
• Remove option -obviously-terminates.
• New experimental domain "numerors" inferring absolute and relative errors of floating-point computations. Enabled by the option -eva-numerors-domain. Does not handle loops for now.
• The memexec cache is now fully compatible with all abstract domains provided by Eva. However, the binding to the Apron domains disable memexec.
• Improved performances when the symbolic locations domain and the memexec cache are enabled.
• Enable the memexec cache by default. It can be disabled by option -eva-no-memexec.

Bug Fix

• Deprecate option -val-warn-builtin-override in favor of warning category builtins:override.

Plugin Metrics

• Add option -metrics-used-files, to help identify unnecessary files given in the command line

Plugin RTE

• Remove option -rte-precond.
• Stop generating spurious \initialized alarms. Fixes #429

Plugin WP

• [Qed]  Added more simplifications for invertible functions
• [Qed]  Added builtin simplification on array operations
• [TIP]  Extends tactical 'Split' to distribution of qualitifiers
  
  
• [Wp]  Added more simplifications on list operations
• [Wp]  Use functional havoc instead of a predicate in Typed model
• [Wp]  Option -wp-warn-separation changed into -wp-warn-memory-model Adding memory model hypotheses related to pointer validity
• [Wp]  Added support for ACSL \offset construct

Frama-C General

• [Libc]  Fix C++ compatibility for Frama-Clang plug-in
  
  

Frama-C General

New Features

• [Kernel]  Make some typechecking warnings controllable with -kernel-msg-key keys.
• [Kernel]  Option -warn-not-finite-float renamed into -warn-special-float and extended (accepts non-finite/nan/none).
• [Kernel]  Alarms Logic_memory_access and Valid_string, that were only emitted by Eva builtins, are removed.
• [Kernel]  Added option -json-compilation-database to help with preprocessing. Requires yojson during Frama-C compilation.
• [Kernel]  Better renaming of variables in case of name collision.
• [Kernel]  introduce warning categories, with various possible behaviors. Refactor management of debug categories
• [Kernel]  deprecate option -continue-annot-error in favor of warning category annot-error
• [Kernel]  More possible statuses for warning categories. Fixes #486
• [Kernel]  Deprecate option -warn-decimal-float in favor of warning category parser:decimal-float
• [Kernel]  Added option -inline-calls for syntactic inlining
• [Logic]  Ghost code now supports /@ ... @/ annotations
• [Typing]  Support for CERT EXP46-C

Bug Fixes

• [ACSL]  Reinforce rejection of implicit casts from array types to pointer types in the arguments of ACSL built-in constructs related to memory blocks and pointer dereferencing.
• [ACSL]  Reinforce rejection of void* pointer types in the arguments of ACSL built-in constructs related to memory blocks and pointer dereferencing.
• [Kernel]  Clean up typechecking environment when dropping side-effects (in sizeof et al.). Fixes #430
• [Kernel]  Handle anonymous struct/union init. Fixes #376
• [Kernel]  Avoid crash when re-declaring a function with formals after it has been called without any. Fixes #454
• [Typing]  Stronger checks w.r.t. implicit conversions in function pointers (must have compatible types) and assignments (modifiable lvalues). Fixes #479

Developers Only

• [Kernel]  Old Cil.isCharType renamed as Cil.isAnyCharType. New Cil.isCharType is now only true for plain char, neither signed nor unsigned. Derived functions (isCharPtr et al.) also updated
• [Kernel]  Keep information about syntactic scope of local static variables. Accessed through Globals.Syntactic_search.find_in_scope.
• [Kernel]  Never or rarely used Log functions have been removed or deprecated
• [Kernel]  Change Cil.typeHasAttributeDeep into Cil.typeHasAttributeMemoryBlock. Fixes #489
• [Lib]  New Rich_text module to create message with tags
• [Logic]  properly reset logic environment in case of typing errors. Fixes #326

Frama-C GUI

• [Gui]  Added Preferences menu (shortcut: Ctrl+P) to set themes for property bullets and external source editor
• [Gui]  The preconditions of a function call can now be displayed before the call statement itself (click on status bullets with '+' or '-' to unfold/fold them)

Plugin E-ACSL

New Features

• [E-ACSL]  New option -e-acsl-validate-format-strings to detect format string errors in printf-like functions.
• [E-ACSL]  New option -e-acsl-replace-libc-functions to replace a few libc functions by built-ins that efficiently detects when they are incorrectly called.
• [E-ACSL]  Support for let binding.

Bug Fixes

• [E-ACSL]  Restore behavior of option -e-acsl-valid broken since Phosphorus (included).
  
  
• [E-ACSL]  Fix 'segmentation fault' of the generated monitor whenever the main has a precondition depending on the memory model.
• [E-ACSL]  Fix a crash when translating a postcondition that should generate a local variable (bts #2339).
• [E-ACSL]  Fix incorrect typing in presence of comparison operators (may only be visible when directly analyzing the E-ACSL's generated code with Frama-C without pretty-printing it).
• [E-ACSL]  Correct support of variable-length array (fix bug #1834).
• [e-acsl-gcc]  Several files may be given to e-acsl-gcc.sh (as specified).
• [runtime]  E-ACSL aborted when run on a machine with a low hard limit on the stack size.
• [runtime]  Function __e_acsl_offset now returns size_t.

Plugin Eva

New Features

• New panel "Red alarms" in the GUI that shows all red statuses emitted for some states during the analysis. They are not completely invalid, but should often be investigated first.
• Various improvements in the handling of floating-point variables: evaluation of \is_finite, computation of the bits of a floating-point range, etc
• In the log, messages on preconditions are now reported with the location of the call site.
• New builtins for the single-precision mathematical functions fmodf, cosf, sinf and atan2f.
• New option -val-skip-stdlib-specs, set by default. When analyzing the body of a function from Frama-C's standard library, specifications will be skipped.
• Eva complies with option -warn-special-float, and propagates or warns on NaN and infinite values accordingly.
• Fix a crash when using -val-stop-at-nth-alarm.
• Evaluate the preconditions of the functions for which a builtin is used; builtins do not emit alarms anymore.
• The Simple_memory functor lets builtins interpret C functions from the value of arguments to the result value.
• New function post_analysis in abstract domains, called at the end of the analysis.
• Renamed option -val-malloc-returns-null to -val-alloc-returns-null, which also applies to realloc builtins.
• The subdivision of evaluations (through the option -val-subdivide-non-linear) can subdivide the values of several lvalues simultaneously (on expressions such as x*x - 2*x*y + y*y).
• Warn about unsupported allocates clauses.
• By default, do not emit pointer_comparable alarms for non pointer operations. Always compute {0;1} for non pointer comparisons involving incomparable addresses.
• Shifts of addresses now create garbled mixes (as any other arithmetic operation).
• Removed *_alloced_return base created for functions without body that return pointers. Such bases were imprecise and could be unsound in corner cases.
• When an lvalue lv is assigned or leaves the scope, the equality domain tries to replace lv by an equal term (if any) in the expressions depending on lv (instead of removing them).
• Equalities can be propagated through function calls. New options -eva-equality-through-calls[-function] to decide (globally or by function) which ones are kept from the caller.
• deprecate option -val-warn-on-alarms in favor of warning category alarm
• Fix a soundness bug in the equality domain: do not infer incorrect equalities between incomparable pointers, or between -0. and +0.
• Avoid enumeration on values with too many bases — fixes a performance issue.
• In the logic, interpret the ACSL function \sign and the constructors \Positive and \Negative.
• Fix the initialization of local volatile variables, which can always have any value.
• Initialization of volatile pointers now keeps the base addresses of the pointer (with arbitrary offsets).
• Interpret the logic constants \pi and \e.
• Added scripts and templates to help automate case studies (in $FRAMAC_SHARE/analysis-scripts)

Bug Fixes

• Fix bug in the handling of non-explicitly volatile fields inside volatile structs or unions
  
  
• Fix bugs in builtins for cos and sin. The results may be less precise than previously

Developers Only

• Option -all-rounding-modes has been removed
• The Fval module now supports NaN and infinite values. Major API changes in Fval, Ival and Cvalue.V (regarding casts, mostly)

Plugin Impact

• Removing Db API for Impact plug-in. Calls to !Db.Impact should be replaced by calls to Impact.Register.

Plugin Metrics

• When the value coverage is computed, also shows the total number of statements by function in the filetree of the Gui.

Plugin Occurrence

• Removing Db API for Occurrence plug-in. Calls to !Db.Occurrence should be replaced by calls to Occurrence.Register.

Plugin RTE

• Do not emit spurious 'idx < 0' assert on gcc-style FAM. Fixes #393

Plugin Users

• Removing Db API for Users plug-in. Calls to !Db.Users should be replaced by calls to Users.Users_register.

Plugin WP

• [Qed]  New simplifications for validirt and ranges
• [Qed]  Extends simplifications for lsl,lsr and div
• [Qed]  Transforms some quantifications into let constructs
• [TIP]  New tacticals for validity and ranges
  
  
• [TIP]  New tactical Congruence (divisions and products)
• [TIP]  Fix bug that makes the TIP wrongly reuse previous results
• [TIP]  New Strategies for bitwise and congruence operations
• [TIP]  Auto-Search mode from the GUI
• [TIP]  Fix wrong reconciliation of sub-scripts during replay
• [TIP]  Extend bitwise-eq auto-strategy on hypotheses
• [WP]  Fix soundness bug when assigning non-valid ranges
• [WP]  Option -wp-unfold-assigns for proving assigns of aggregates field by field
• [WP]  Option -wp-print-separation changed into -wp-warn-separation
• [WP]  Auto-Search mode, see -wp-auto
• [WP]  Upgrade to Why-3 0.88.3
• [WP]  Upgrade to Coq 8.7.1
• [WP]  Upgrade to Alt-Ergo 2.0.0
• [WP]  Filter out some variables from separation
• [WP]  Allow backtracking when using strategies (-wp-auto-backtrack)
• [WP]  Better handling of \null and (void *)0L
• [WP]  Experimental support for _Bool range (-wp-bool-range)
• [WP]  Add the missing ACSL math builtins (see manual)

Frama-C General

New Features

• [ACSL]  Explicitely disallow /* and */ in ACSL annotations. Allows to re-use logic parser for parsing annotations in external files that can use /* ... */ as comments. As a consequence, expressions like y/*p are thus rejected, but this was already the case when -pp-annot is activated (default for .c files) and can be fixed easily in y / *p (as it is pretty-printed)
• [Kernel]  qualifiers are dropped from the return type of functions, as they make no real sense
• [Kernel]  Added option -print-return to inline gotos to return
• [Kernel]  Composite types are now required to have equal tags as per the C standard; no more support for isomorphic structs.
• [Kernel]  Fix invalid eids on code generated through loop unrolling

Bug Fixes

• [Kernel]  stop removing const attribute on local variables. Fixes #301
• [Kernel]  Parser now handle mixed concatenation of string and wstring. Fixes #1467
• [Kernel]  Fix unmarshalling of save files that contain more than 4Gb of uncompressed data. Patch from TIS-interpreter.
• [Kernel]  Strip bitfield attribute when performing integral promotions on bitfields of size short or char. Fixes incorrect attributes on the resulting expression.
• [Kernel]  Fix various typos in source code and user messages. Patch by Debian. Fixes #2323
• [Kernel]  Fixes configure script on bytecode only architecture. Initial version of the patch by Debian. Fixes #2325
• [Kernel]  More thorough checks on l-values with function type. Non-sensical expressions are now rejected at parsing type.

Developers Only

• [ACSL]  Refactor handling of logic labels in AST
• [Kernel]  Completely separate types between Cil_types and Logic_ptree, removing needless polymorphism
• [Kernel]  Remove needless repetition of declared logic labels in Tapp and Papp nodes. Fixes #274
• [Kernel]  sizeof() and alignof() applied to a function can now be rejected when the compiler does not support this construct, depending on the fields sizeof_fun and alignof_fun of the machdep
• [Makefile]  add gui-byte target to only build bytecode GUI

Frama-C GUI

• [Gui]  In the filetree, the filter menu appears on a right click on the header, while a left click sorts the tree.

Plugin Callgraph

• Option -cg-init-roots replaced by -cg-service-roots (almost equivalent); new options -cg-function-pointers (ignore function pointers; unsound) and -cg-roots (compute subgraphs).

Plugin E-ACSL

New Features

• [E-ACSL]  New detection of temporal errors in E-ACSL through -e-acsl-temporal-validity (disabled by default).
• [e-acsl-gcc]  Add --stack-size and --heap-size options to e-acsl-gcc.sh allowing to change the default sizes of the respective shadow spaces.
  
  
• [e-acsl-gcc]  Add --keep-going option to e-acsl.gcc.sh allowing a program to continue execution after an assertion failure.
• [e-acsl-gcc]  Add --rt-verbose option to e-acsl.gcc.sh.
• [e-acsl-gcc]  Add --weak-validity option to e-acsl.gcc.sh.
• [e-acsl-gcc]  Add --temporal option to e-acsl.gcc.sh.
• [e-acsl-gcc]  Add --fail-with-code option to e-acsl.gcc.sh.
• [e-acsl-gcc]  Add --free-valid-address option to e-acsl.gcc.sh.

Bug Fix

• [E-ACSL]  Fix bug #2303 about unnamed formals in annotated functions.

Plugin Eva

New Features

• More precise evaluation of \initialized and \dangling predicates.
  
  
• New directive Frama_C_domain_show_each prints the internal properties about the arguments inferred by each available domain whose log category is enabled.
• Frama_C_dump_each prints the state of each available domain whose log category is enabled.
• Removes all effects of the special functions Frama_C_[dump|show]_each on the analyses: no alarms are emitted and the states are never reduced on these calls.
• The subdivision of the evaluation of non-linear expressions (through the -val-subdivide-non-linear option) also applies to the new evaluations requested by the equality domain.
• New sign domain for demonstration purposes only.
• Better handling of function alloca(), via builtin Frama_C_alloca.
• In the GUI, the "Values" panel displays the values computed by using the properties inferred by all enabled domains.
• Emits overflow alarms on unsigned left shift when -warn-unsigned-overflow is enabled.
• Fixed memory leak with option -val-subdivide-non-linear
• Fix soundness (resp. precision) bug on big-endian (resp. little-endian) architectures. This bug triggered on low-level code, typically when using bitfields
• Various precision improvements in the interpretation of the behaviors of a specification.
• The backward propagation tries to reduce integer values by considering separately the bounds of their intervals.
• Uses assigns clauses to over-approximate the effects of assembly statements. Warns if no assigns clause is provided.

Bug Fixes

• Fix soundness bug in string builtins where some invalid offsets did not generate alarms.
• Fix missing alarms when downcasting pointer values.
• Fix a crash when downcasting pointer values with the option -val-warn-signed-converted-downcast enabled.
• The cvalue states saved after each statement are now properly deleted when an Eva parameter is changed in the GUI.
• Fix performance issue with the equality domain.
• Fixes a soundness bug where a loop invariant could be wrongly proved correct in some marginal cases.
• Fixes an optimization issue where the reduction by a loop invariant just after widenings could impede the convergence.
• Fixes a performance issue in offsetmaps, that occured when reading or copying values smaller than cells in large arrays.
• Fix bug in the handling of non-explicitly volatile fields inside volatile structs or unions
• Fix bugs when evaluating \ìnitialized, \dangling and \separated on addresses of bitfields

Developers Only

• Abstract domains have to provide a log category and a function show_expr that prints the internal properties inferred about an expression.
• The argument ~with_alarms for functions of Db.Value is now optional, and will be removed in a later version.
• New functor in domains/simple_memory.ml to build a complete domain from a value abstraction. The abstract states link each scalar variable of a program to an abstract value.
• In abstract domains, compute_using_specification is replaced by logic_assign, that interprets one \assigns clause. Complete specification are now interpreted through successive calls to evaluate_predicate, reduce_by_predicate and logic_assign.

Plugin Metrics

• In the Gui, shows the percentage and the number of dead statements (when computed) for each function of the filetree.

Plugin Report

• Removing Db API for Report plug-in. Calls to !Db.Report.print should be replaced by calls to Report.Register.print.

Plugin RTE

• add option -rte-initialized to generate assertions over read accesses to potentially uninitialized locations.
• Fix bounds of alarms emitted when downcasting to bitfields (issue '2314')
• Emits overflow alarms on unsigned left shift when -warn-unsigned-overflow is enabled.
• add -warn-not-finite-float for checking that infinite and NaN floats are not produced.

Plugin Scope

• Removing Db API for Scope plug-in. Calls to !Db.Scope should be replaced by calls to Scope.

Plugin Slicing

• Fix invalid eids on code generated through option -slicing-level >= 2
• Removing Db API for Slicing plug-in. Calls to !Db.Slicing should be replaced by calls to Slicing.Api.
• Removing deprecated '-slice-option' and related !Db.Slicing.Projet.print_exported_project. Minor changes into !Db.Slicing.Projet.extract.

Plugin Sparecode

• Rename option -rm-unused-globals to -sparecode-rm-unused-globals.

Plugin WP

New Features

• [TIP]  New tactical Rewrite (two apply equalities)
• [TIP]  New tactical Bitwised, BitRange and Shift
• [TIP]  New tactical Ratio (divisions and products)
• [TIP]  New tactical Overflow (to cope with modulus)
• [TIP]  Options -wp-time-{extra|margin} for more stability
• [WP]  More simplifications wrt integer domains
  
  
• [WP]  Reduction of equalities with logic functions
• [WP]  Option -wp-overflows to add explicit assumptions
• [WP]  Option -wp-prenex to normalize nested binders
• [WP]  New simplification for ground terms (-wp-ground)
• [WP]  New simplification of unused variables (-wp-parasite)
• [WP]  New simplification logic functions (-wp-reduce)
• [WP]  Improved model and simplifications of logical shifts
• [WP]  Support for LoopCurrent and LoopEntry

Bug Fix

• [GUI]  Fixed bug when running prover from the TIP

Frama-C General

New Features

• [Kernel]  Stricter verification for extern, static and inline specifiers (support for CERT DCL-36-C coding rule)
• [Kernel]  New option -no-autoload-plugins (equivalent to old -no-dynlink); mostly for internal use.
• [Kernel]  New option -print-machdep (help group).
• [Kernel]  Bash completion for Frama-C options. See #154.
• [Kernel]  New option -print-libc, to expand include directives for files in the Frama-C stdlib (no longer expanded by default).
• [Kernel]  Zarith library is now required
• [Kernel]  Better handling of VLA (use explicit function calls to mark deallocation of VLA at appropriate program points)
• [Kernel]  Explicit AST nodes to mark local variables initialization.
• [Kernel]  Dynlink is now mandatory, no degraded static mode.

Bug Fixes

• [Cil]  Pointer subtractions with arguments of incompatible types are now refused. The resulting expression is typed as ptrdiff_t instead of int.
• [Kernel]  Fixed some issues with #pragma pack() behavior, in both GCC and MSVC machdeps. Also fixed some related issues with __aligned__ and __packed__ attributes (including bts #2249).
• [Kernel]  Fixes oneret normalization in presence of statement contract and absence of return. See #255 and #2235.
• [Kernel]  Fix crash when loading a saved file without a plug-in which has previously emitted a status with a tuning parameter.

Developers Only

• [Kernel]  Utility API for checking volatile attribute in Cil.

Frama-C GUI

• [Gui]  Signature change for constructor Pretty_source.PVDecl

Plugin Callgraph

• Fixes inverted callers/callee in indirect calls

Plugin E-ACSL

New Features

• [e-acsl-gcc]  Remove precond rte option from e-acsl-gss.sh.
• [e-acsl-gcc]  Add --check option to e-acsl-gcc.sh which allows to check the integrity of the generated AST before instrumentation.
• [e-acsl-gcc]  Remove --print|-p option from e-acsl-gcc.sh
• [runtime]  The (much more efficient) shadow memory model is now used by default.

Bug Fixes

• [E-ACSL]  Fix bug with typing of unary and binary operations in a few cases: the generated code might have overflowed.
  
  
• [E-ACSL]  Fix bug #2252 about pointer arithmetic with negative offsets.
• [E-ACSL]  Fix bug with goto which points to a labeled statement which must be instrumented.
• [E-ACSL]  Fix crash with casts from non-integral terms to integral types (bts #2284).
• [E-ACSL]  Correct support of stdin, stdout and stderr in annotations.
• [E-ACSL]  Fix bts #1740 about incorrect monitoring of memory properties when early exiting a block through goto, break or continue.
• [runtime]  Fix backtrace when the failed instrumented programs do not require memory model.

Plugin Eva

New Features

• New (internal) mechanism to handle C functions' return values. Messages now mention \result<foo> for the value returned by 'foo'.
• Option -val-show-progress is now unset by default
• Activate option -remove-redundant-alarms by default.
• New option -val-builtins-list
• Renamed dynamic allocation builtins for improved consistency. In particular, Frama_C_alloc_size becomes Frama_C_malloc_fresh.

Bug Fixes

• Unsound support for recursion, through option -val-ignore-recursive-calls. The support of recursion through the use of 'assigns' clauses, previously available in Value, was unsound and has been removed
• Fix bug #2277. The initial state of the analysis now depends on all relevant options, including kernel options -warn-...
• Fixes a crash with the -val-subdivide-non-linear option, on subdivisions of evaluations involving pointer values.
• Fixes a crash when backward-propagating an imprecise value on a 32-bits floating point addition. A non-single precision value was erroneously returned.
• Perform widening in the symbolic locations domain.
• Fix widening in the gauges domain, in particular with nested loops and pointers that change base address through iterations

Developers Only

• Functions Db.Value.fun_set_args and Db.Value.globals_set_initial_state are now compatible with Eva.
  
  
• Incompatible API changes in module Cvalue.Model. Functions named 'unspecified' have been renamed into 'indeterminate', and some arguments have been removed.

Plugin Inout

• Option -inout-callwise is now always active, and will be removed in a later version
• Prevent formal variables of functions with only a specification from leaking into results

Plugin Metrics

• Programmatic API for some functions via Metrics.mli.

Plugin Obfuscator

• Fix typo in help message (bts #2269).

Plugin Rte

• Remove option -rte-all.

Plugin Scope

• Fix bug in the functions of Db.Scope in presence of alarms refering to volatile memory locations, or to variables that leave scope. Also impacts Eva option -remove-redundant-alarms

Plugin Value

• Support for the legacy value analysis has been abandoned, Eva is now always active. Option -no-eva has been removed.
• Widen hints directives @widen_hints now accept arbitrary l-values (evaluated at analysis time) in place of variables.

Plugin Variadic

• Change of command line argument names for the plugin Variadic. The new names are more expressive and avoid confusions with the plugin Value. Use -variadic-translation or -variadic-no-translation instead of -va or -no-va.
• The plugin is now enabled by default. Use the option -variadic-no-translation to keep the original behaviour. The specification generated for the fprintf function family is now more accurate.

Plugin WP

New Features

• [GUI]  Interactive Proof Engine
• [GUI]  Pretty-print of memory side effects
• [Qed]  Improved simplifiers
• [Qed]  Mutualized type inference in Term
• [Qed]  Negation of forall-exists qualitifers
• [Qed]  Add E_fun constructor for neutral and absorbent
• [Qed]  Transforms some quantifications into let constructs
• [WP]  Fix volatile access (see -wp-no-volatile)
  
  
• [WP]  Warn against access to volatile l-values
• [WP]  Simplification of ACSL sequences
• [WP]  Improved Sequent API (Conditions)
• [WP]  Fixed bug #2246 (unsound switch)
• [WP]  Improved sequent simplifier
• [WP]  Deprecated Dynamic API
• [WP]  Extensible Proof Engine
• [WP]  Generated HTML API (make wp-doc-api)
• [WP]  Improved filtering (prevents loss of init clauses)
• [WP]  Improved comparison of logic compounds
• [WP]  Fix bug on negative 0x float constants
• [WP]  Trivial simplification for truncate
• [WP]  Remove support for generalized invariants (-wp-invariants)
• [WP]  Extract inductive predicates as Inductive in Coq

Developers Only

• [Ergo]  Update qualif tests to Alt-Ergo 1.30

Frama-C General

New Features

• [Cil]  Conversions between a bit-field lvalue and the (integral) type of the bitfield are now always made explicit through casts; the attribute FRAMA_C_BITFIELD_SIZE is present on the type of the cast if needed.
• [Kernel]  OCaml version greater than or equal to 4.02.3 required.
• [Kernel]  OCamlGraph is no longer packaged within Frama-C, and must be installed to build Frama-C from source
• [Kernel]  Deprecated Pretty_utils.sfprintf, use Format.asprintf instead.
• [Kernel]  Support for C11 redefinition of typedefs
• [Kernel]  Fix bug that may occur when modifying several times command line-options taking functions as argument (issue #109)
• [Kernel]  Fix major bug in the backward dataflow of module Dataflows
• [Libc]  Implementations of some functions of the standard library are now available in share/libc/*.c
• [Libc]  New file share/libc/string.c, with simple implementations for C99 functions defined in string.h. Duplicate implementations were removed from share/libc.c.
• [Libc]  Functions in share/libc.c have been inlined into the proper .c files under share/libc
• [Logic]  Refactoring of ACSL extensions + allow extensions in loop annotations

Bug Fixes

• [Kernel]  Side-effect free instructions such as 'e;' are now translated as 'tmp = e;' instead of 'if (e) {}' (which was incorrect when e did not have a scalar type)
• [Kernel]  Scripts that use Gtk can again be loaded using option -load-script (bug report: http://stackoverflow.com/questions/38677256/)
• [Kernel]  Fix bug #2239 about unsoundness of callgraph's services computation (bug introduced in Frama-C Magnesium).
• [Kernel]  Fix bug when pretty printing an ACSL term "divisor / *p" (bts #2250).
• [Makefile]  Fix compilation of plug-ins which depends on another plug-ins when compiled outside Frama-C.

Developers Only

• [Kernel]  Functions Integer.pgcd and Integer.ppcm are now guaranteed to return a positive result.
  
  
• [Kernel]  Fixes merging of contract when using Annotations.add_code_annot
• [Kernel]  Remove class Filecheck.check from API. Use Filecheck.check_ast that provides the correct encapsulation.
• [Kernel]  Suppress return_stmt field of kernel_function type. Use Kernel_function.find_return instead.
• [Kernel]  Rename some types of the logic AST for more coherence
• [Makefile]  Warnings and warn-error are activated only if a file .for_devel is present along side the Makefile (also for plugins)

Frama-C GUI

• [Gui]  Different filters for user assertions and RTEs are now available.

Plugin Eva

New Features

• Support for options -warn-signed-downcast and -warn-unsigned-downcast.
• Improvements to option -val-subdivide-non-linear on expressions such as x*x+y*y, or t[i*i].
• Improvements to option -val-subdivide-non-linear for high number of subdivisions
• Various improvements to experimental Apron domain
• More systematic backward-propagation between actual parameters and formals
• New experimental Gauges domain, that relates integer variable to loop counters.

Bug Fixes

• Setting option -val-warn-copy-indeterminate now forces lvalue copies to perform a full evaluation. This includes converting the copied value to the proper type, and emitting alarms if it is indeterminate. This option should not be set for memcpy-like functions, or for functions that copy bits of pointers
• fix performance bug in the equality domain, especially visible on programs with many local variables.
• Fix bug in equality domain, after assignements lv = e where the modified locations intersect those involved in computing lv
• Prevent incorrect reductions on memory locations with volatile qualifier
• Fix bug in the bitwise domain, on some applications of the & and | operators
• Fix soundness bug on statements with RTE or programmatically-added user assertions (bts #2258). This leads to minor changes in the way states are propagated when all slevel has been consumed. Also, consolidated states now return the abstraction before any reduction by assertions or alarms.

Plugin From

• Removed options -experimental-path-deps and -experimental-mem-deps.

Plugin Nonterm

• overall increase in precision, especially on compound statements (if, switch, loops...). Verbosity has been decreased
• New options -nonterm-ignore f1,..,fn (to ignore calls to functions f1,..,fn) and -nonterm-dead-code (to warn about syntactically dead code)

Plugin Rte

• New option -rte-pointer-call, to generate annotations for calls through function pointers

Plugin Scope

• Fix bug that might lead to unsoundness and / or looping in 'Datascope' functionality (#235)

Plugin Value

New Features

• Builtins are now available for malloc: Frama_C_alloc_size (one new base each time, may diverge) and Frama_C_alloc_by_stack (one base by stack, may end up performing weak updates).
• New message key final-states, that can be used to deactivate the printing of the abstract states at the end of each function
• New option -val-warn-on-alarms, which governs whether alarms are printed as warnings or text.
• New message key 'garbled-mix', to track garbled mix generated during the analysis
• Several warnings emitted by Value are now properly prefixed by [value] instead of [kernel]
• API changes in modules Lmap and Cvalue.Model. All occurrences of `Map in returned value should be replaced by `Value
• Pointers to functions with an incompatible type are now handled in a more stringent manner. Previously, arguments with incompatibles types but equal size were reported with an orange status. Now, any mismatch (e.g. int/float or signed/unsigned) causes a red alarm.
• New option -val-flamegraph, to dump information about analysis times as a Flamegraph
• Option -val-show-time has been removed. Options -val-show-perf or -val-flamegraph offer more information
• Do not compute the sizeof of a function when evaluating a function call through a pointer. This avoids some warnings in MSVC mode.
• valid_string and valid_read_string predicates are now evaluated by Value
• New builtins for string-related functions: Frama_C_strlen, Frama_C_strchr, Frama_C_strnlen, Frama_C_memchr and Frama_C_rawmemchr
• Extended support for syntactic widening hints (@widen_hints - see the Value user manual for more details)
• Option -val-warn-copy-indeterminate is now set by default. See command-line help if you want to deactivate it.
• New (experimental) option -val-builtins-auto, to automatically replace known C functions by builtins. Will be set by default in Phosphorus.

Bug Fixes

• Fix crash when extracting bits of a long double value. (Issue 92 on TIS-interpreter, reported by ch3root.).
• Option -val-show-initial-state has been removed. Instead, -value-msg-key=-initial-state can be used
• Garbled mix created when analyzing assigns / from clauses are now tagged as having "Library function" origin
• Option -val-show-perf now properly takes into account the time taken by the main function itself (without its callees)
• Frama_C_cos and Frama_C_sin builtins are now precise by default. The former Frama_C_cos / Frama_Csin_precise have been removed

Plugin WP

• [WP]  Fix -wp-rte with respect to models and kernel options
  
  
• [WP]  Use cint and cfloat models by default
• [WP]  Use kernel options -warn-xxx in cint model
• [WP]  Simplification of arithmetics models
• [WP]  Unified variable usage for all models

Plugin E-ACSL

New Features

• [E-ACSL]  Re-implementation of the type system which improves the efficiency of the generated code over integers.
• [E-ACSL]  New option -e-acsl-builtins which allows to declare pure C functions which can be used in logic function application.

Bug Fixes

• [configure]  Added --enable-optimized-rtl option to configure
• [E-ACSL]  Fix bug #1395 about recursive functions.
• [E-ACSL]  Fix bug #2191 about complicate structs and literate string.
• [E-ACSL]  Add monitoring support for aligned memory allocation via posix_memalign and aligned alloc functions.
• [E-ACSL]  Enable reporting of stack traces during assertion failures in instrumented programs.
• [e-acsl-gcc]  Add an e-acsl-gcc.sh option (--rte|-a) allowing to annotate the source program with memory-safety assertions prior to instrumentation.
• [e-acsl-gcc]  Add an e-acsl-gcc.sh option (--print--models) allowing to print the names of the supported memory models.
• [e-acsl-gcc]  Removed --production|-P, --no-stdlib|-N and --debug-log|-D options of e-acsl-gcc.sh.
• [e-acsl-gcc]  Added --rt-debug feature to e-acsl-gcc.sh. --enable-optimized-rtl configure option removed
• [e-acsl-gcc]  Added --rte-select feature to e-acsl-gcc.sh.
• [Makefile]  Fix 'make clean' in tests.
• [Makefile]  Fix 'make install' when executed within Frama-C.
• [runtime]  Fix several bugs related to incorrect partial initialization of tracked memory blocks in the E-ACSL memory model library.
  
  
• [runtime]  Improve performance of Patricia Trie memory model.
• [runtime]  Add custom implementation of malloc for use with E-ACSL runtime library (via jemalloc library).
• [runtime]  Add local version of GMP library customized for use with E-ACSL runtime library.

Frama-C General

New Features

• [ACSL]  Add notation '{ x, y, z }' for defining sets.
• [ACSL]  Add built-in operators for lists.
• [ACSL]  New predicate \valid_function, requiring the compatibility between the type of the pointer and the function being pointed.
• [Cil]  Typing within comparisons is now more strict, or made more explicit through casts.
• [Cil]  Double pointer casts on the NULL pointer are now simplified.
• [Cil]  Add support for parsing digraphs.
• [Cil]  Incorrect return statements (return void on non-void functions and vice-versa) now generate errors instead of warnings.
• [Cil]  Better handling of C99 flexible array members (FAMs). Static initialization of FAMs (a GCC extension) is no longer supported.
• [Cil]  Changes in the handling of incomplete structs and zero-length arrays. Initialization of incomplete (completely undefined) structs is now duly rejected. Several compiler extensions to the C99 standard (empty initializers, zero-length arrays, etc.) now require a GCC or MSVC machdep (e.g. -machdep gcc_x86_32).
• [Cil]  Operator ! applied to constant expression is no longer simplified when not required.
• [Cil]  Add proper support for empty aggregate initializers in GCC mode.
• [Kernel]  New option -set-project-as-default.
  
  
• [Kernel]  New option -remove-projects.
• [Kernel]  New options -then-last and -then-replace.
• [Kernel]  The untyped AST is no longer removed by basic program transformations such as loop unrolling.
• [Kernel]  Option -warn-undeclared-callee changed to -implicit-function-declaration, which receives an argument (ignore, warn or error) specifying what to do when an undeclared function is called.
• [Kernel]  Option -collect-messages is obsolete and will be removed in a future version; messages are now always collected.
• [Kernel]  Automatic generation of assigns from GCC's extended asm.
• [Kernel]  Registering twice the same machdep is now accepted.
• [Kernel]  New option -<plugin>-log to copy the output of plug-ins into one or several text files (described in the User Manual).
• [Makefile]  Target 'make rebuild' has been renamed into 'make clean-rebuild'.

Bug Fixes

• [ACSL]  Fixes example of logic label use. Fixes bug #2203.
• [ACSL]  Fixes implicit logic label generation on recursive definitions. Fixes bug #2158.
• [ACSL]  Fixes precedence uncompliance within ACSL Manual of some bitwise operators and more aggressive checks of consistent relation chains.
• [Kernel]  Comments are preserved even when loops are unrolled. Fixes issue #2176.
• [Kernel]  Avoid comment duplications on generated code.
• [Kernel]  do not crash when loading statuses depending from non existing parameter. Fixes issue #2181.
• [Libc]  Fix specifications of memchr and strncpy.
• [Logic]  Meaningless assigns clauses are now rejected more aggressively. Fixes bug #1790.

Developers Only

• [Cil]  Buggy record Cil.miscState has been removed. Customization must be done directly in Cil_printer.state.
• [Kernel]  API change for function Alarms.register. See .mli for details.
• [Kernel]  Removed function State_selection.list_state_union. Use State_selection.of_list or State_selection.list_union instead.
• [Kernel]  Several incompatible changes in module Property.
• [Kernel]  Do not raise Invalid_arg and Failure exn but use custom exceptions instead. Prevents warning 52 in OCaml 4.03.0 Functions raising new exceptions are: - Db.From.find_deps_term_no_transitivity_state - Db.Interp.*
• [Makefile]  Get rid of FRAMAC_MAKE variable. Use FRAMAC_INTERNAL instead for distinguishing internal and external mode.
• [Makefile]  New option PLUGIN_EXTRA_DIRS for multi-dir plugins.
• [Ptests]  New EXEC: directive.

Frama-C GUI

• [Gui]  Refactor GUI Helpers. (Toolbox and (partially) Gtk_helper moved to Wutil,Widget, Wform, Wtext and Wtable).
• [Gui]  Signature change for function Design.register_source_highlighter; the first argument of the callback has now type Design.reactive_buffer, which can be coerced back to a GSourceView2.source_buffer using method buffer.

Plugin Eva

New Features

• More aggressive reductions in complex conditions such as if(a+3 < 10).
• Improvements to backward propagation, on memory accsses and bitwise operations.
• Experimental domain dedicated to storing and learning information from syntactic equalities (option -eva-equality-domain).
• New experimental domain that improves precision on bitwise operations, for example on pointers. Activated by option -eva-bitwise-domain.

Bug Fix

• Fixed some bugs related to 0. vs. -0. in conditions.

Plugin From

• Option -from-verify-assigns takes into account direct and indirect dependencies.

Plugin LoopAnalysis

• New plug-in 'LoopAnalysis' which estimates loop bounds and -slevel-function parameters. Invoked using option -loop.

Plugin Metrics

• Fix list of undefined functions; functions that are never called were not reported.
• Fix option -metrics-value-cover when option -metrics-libc is not set.
• Global variables defined in Frama-C standard library are no longer counted when option -metrics-libc is not set.

Plugin Nonterm

• New plug-in 'nonterm' for detection of definite non-termination based on Value.

Plugin RTE

• Fix unsoundness for overflows on binary operations when one or two operands were constant.
• Fix unsoundness on unary minus expressions when option -rte-trivial-annotations is active.

Plugin Sparecode

• Fix crash when an entire function becomes spare. (issue #157).

Plugin Value

New Features

• Better precision for calls through function pointers when multiple functions are possible. The abstract state now contains the information of which function was called.
• During the evaluation of ACSL 'assert', intermediate statuses (e.g. True, then Unknown, then True) are now reported in the console.
• New option -val-warn-undefined-pointer-comparison.
• Better propagation strategy for nested loops. Results are usually much more predictable (and often more precise) when the loops are not fully unrolled by slevel.
• Widening hints now includes signed and unsigned limits for the bitsize of the value being widened, but does not include arbitrary limits anymore. The convergence is generally faster but results may be more or less precises depending on the case.
• Support for \valid_function predicate during evaluation.
• Distinguish direct and indirect dependencies in 'from' clauses to compute the effecst of an 'assigns/from' clause. See section 7.2 of the manual.
• Messages on ACSL predicates with Unknown/Invalid status are now emitted with a 'warning' severity, consistently with the emission of alarms. 'True' statuses are hidden if option -val-show-progress is unset.
• Informative messages about inactive behaviors are now emitted only at verbosity level 2.
• Support for evaluation of predicate \valid_read_string on constant strings.

Bug Fixes

• The preconditions of functions overridden by builtins no longer receive an 'Unreachable status for calls within dead code: the specification is ignored everywhere. Fixes bug #1956.
• Reimplementation of all the upper layers of the plugin. Compatibility with the legacy version is almost complete, save for some text messages and a few functions of the API. Use option -no-eva to switch back to the legacy version. Changelog entries labelled 'Eva' refer to this new version. Entries labelled 'Value' apply to both versions.
• Take into account 'volatile' qualifiers on struct typedefs, which were previously ignored. Fixes issue #102.
• Evaluation of ACSL ranges takes into account option -safe-arrays. In particular t[..] remains within the bounds of t. Fixes bug #1639.
• Fix crashes when analysing a function (without a body) that returns an empty struct, or a pointer to an empty struct. Bugs reported by TrustInSoft.
• Fix handling of functions without a body that return a pointer. The pointer was aligned on an incorrect frontier.

Developers Only

• Functions filter_le_ge_lt_gt_* have been renamed into backward_comp_*. Evaluation and reduction functions for comparisons now use and return dedicated types, in Abstract_interp.Comp.
• Base.base_max_offset has been removed. Part of its functionality is still available via Base.valid_range, whose return type is now more expressive.
• API change in functor Lmap.Make.

Plugin Variadic

• New plug-in 'Variadic' which translates variadic functions, calls and macros to allow analyses to handle them more easily. Invoked using the -va option.

Plugin WP

• [Caveat]  Separation Hypotheses with -wp-print-separation
• [Coq]  Support for Proof General 4.3
  
  
• [Coq]  Fixed bug #2214 (coq realbase)
• [WP]  New options to set prover commands
• [WP]  Added support for built-in ACSL lists
• [WP]  Exported OCaml API via Wp.mli
• [WP]  Strict parsing of -wp-model (stop on error)
• [WP]  Removed alias '-wp-log' (use '-wp-msg-key' instead)
• [WP]  Added support for ACSL let-predicate
• [WP]  Now follows '-safe-arrays' when refining 'p+(..)'
• [WP]  Fix behavior on ASM code
• [WP]  Support for Alt-Ergo 1.01
• [WP]  Support for Coq 8.5
• [WP]  Support for Why3 0.86
• [WP]  Support for why3 0.87 (and ide)

Frama-C General

New Features

• [Cil]  Function Printer.change_printer now allows composing printers, and is called Printer.update_printer.
• [Cil]  Fix incorrect simplifications of '!E' to 0 when E is either an enum with value 0 (bug #2090), or an expression whose value wraps.
• [Cil]  Parsing no longer accepts structures containing incomplete types. Fixes bug #2091.
• [Doc]  Fixed typo in the manual (Thx Mihaela Sighireanu).
• [Kernel]  Add new suffix '.ci' for pre-processed files containing ACSL annotations to be pre-processed.
• [Kernel]  Added -no-tty option to disable terminal capabilities
• [Kernel]  macro __FRAMAC__ is defined when pre-processing C files in Frama-C.
• [Kernel]  Removed option -no-dynlink.
• [Kernel]  New ACSL predicate \valid_read_string in share/libc/__fc_string_axiomatic.h.
• [Kernel]  Special functions CEA_ have been removed.
• [Kernel]  New API for backward dataflow propagation in file Dataflows.
• [Kernel]  Reformulated help messages. Option -help is more concise. Option -version only prints version number. Options -print-xxx uniformized. New options -plugins, -print-config.
• [Kernel]  Dynamic now rely on Findlib. Small changes in API. Option -load-module can now load any Findlib package and its dependencies as well.
• [Kernel]  New option -custom-char-annot for changing the character introducing ACSL annotations (instead of '@').
• [Kernel]  Removed support for OCaml 3.12.1
• [Libc]  Most .c and .h files under /share have been merged into /share/libc. Inclusions of builtin.h should be replaced by __fc_builtin.h.
• [Makefile]  Dynamic plug-ins are now declared as Findlib packages. Use variables PLUGIN_REQUIRES and PLUGIN_DEPENDENCIES. Loading a plug-in automatically loads all necessary dependencies. Plugin "MyPlugin" is register under "frama-c-myplugin" package.

Bug Fixes

• [Cil]  Fix iterators on C99 designated initializers.
• [Cil]  Disallow all incomplete types for struct fields Fixes bug #1672.
• [Cil]  Switch statements in which some cases are not constant expressions are now completely disallowed, as per the C standard.
• [Cil]  Fix parsing of packing directives of the form '#pragma pack(push, N)'.
• [Cil]  Better typing of '?' operator. Fixes bug #2117.
• [Cil]  Cil transformation can introduce assertion to ensure that size expressions in an array declarations evaluated at program execution time are positive and do not overflow.
• [Cil]  Fix bug #1553, related to nested initialisations of structures containing pointers.
• [Kernel]  Fix clearing of old statuses and hypotheses when a new status is emitted or an annotation is removed.
• [Libc]  Added ACSL specifications to some standard library functions, including read, write and realloc. Fixes bug #1939.
• [Libc]  Fix bug in the specifications of readir, opendir, closedir and fopen functions, that would cause incorrect analysis in -lib-entry-mode.
• [Libc]  Removed obsolete file machine.h (along with other similar files) from the Frama-C share folder. Fixes bug #2171
• [Logic]  Better overloading resolution. Fixes bug #2098.
• [Logic]  Correct handling of string and char constant in logic pre-processing. Fixes bug #2101.
• [Logic]  Fix typing bug when converting into a term an expression containing a pointer subtraction.

Developers Only

• [Kernel]  Fixed bug #2012 about combining Ast.is_last_decl and Kernel_function.get_global.
• [Kernel]  Function Integer.two_power now raises an exception for overly big arguments.
• [Kernel]  AST change: split GVarDecl into GVarDecl and GFunDecl
• [Kernel]  Remove long-obsoleted functions Cfg.computeCFGInfo Cfg.printCfgFilename, and Cfg.printCfgChannel.
• [Kernel]  Remove support of plug-ins without .mli. Fixes bug #1825.
• [Kernel]  Ival.Float_abstract renamed to Fval. Fval.inject_r now may raise Fval.Non_finite instead of the old Float_abstract.Bottom.
• [Kernel]  Modules Dataflow is deprecated, and will be removed in Aluminium. Module Dataflow2 offers a very similar but simpler API.
• [Logic]  Functions Db.Properties.Interp.lval and Db.Properties.Interp.expr have been renamed (into term_lval and term, respectively), and have a new signature.
• [Ptests]  New LOG: directive.

Frama-C GUI

New Features

• [Gui]  Variables are now left- and right- clickable in the 'information' panel.
• [Gui]  Internal ids (for statements, code annotations, etc.) are now hidden by default. Start the GUI in debug mode if you want to see them.
• [Gui]  When a call statement is selected, the statuses of the preconditions of the called functions are displayed in the 'information' panel.

Bug Fix

• [Gui]  Filenames in the GUI file tree (top-left panel) are now sorted correctly. Fixes bug #2173.

Developers Only

• [Gui]  Constructor Pretty_source.PTermLval now has an additional argument, the property in which the term appears.
• [Gui]  Minor API changes regarding Design.reactive_buffer. Some values that used to have an option type are now guaranteed to be present.

Plugin Callgraph

• Remove Cil.Callgraph, Db.Syntactic_callgraph and Db.Semantic_callgraph which are all replaced by the single plug-in Callgraph. See Changelog_detailled.md for further detail about this change.
• New plug-in callgraph which merges the old Syntactic_callgraph and Semantic_callgraph plug-ins (now removed). Either this plug-in uses Value if already computed, or computes the syntactic callgraph otherwise. This new plug-in unifies the behavior of its two ancestors. In particular, the edges of callgraph computed with the help of Value are now directed in the same way as the syntactic callgraph (was reversed before) and so the computed services are now equivalent. Also, the uncalled functions are now displayed by default. For plug-in developers, the callgraph is easily accessible via an API (bts #755).

Plugin Defs

• L-values for which defs are queried are now evaluated only for the callstacks that are currently active, resulting in possibly less locations.

Plugin Impact

• Removed function Db.Impact.slice, that was actually unrelated to Impact. You can use the functions contained in Db.Slicing.Select, in particular Db.Slicing.Select.select_stmt, to obtain the same result.

Plugin Inout

• The inputs of an instruction whose evaluation always fail include the sub-expressions for which evaluation succeeds.

Plugin Metrics

• Fix computation of global cyclomatic complexity. Fixes bug #2089.
• New category 'Extern global variables', that can be used to check whether some files are missing.
• Functions from Frama-C standard library are now hidden by default.

Plugin Parsing

• Black-list gcc's builtin macros for logic pre-processing to avoid warnings for duplication. Fixes bug #2161.

Plugin Report

• Reports in csv format now honor option -report-specialized (previously, preconditions at a callsite were always skipped).
• New option -report-proven to control the display of proven properties.
• New export format (.csv), through option -report-csv.

Plugin Scope

• Assertions previously removed by -remove-redundant-alarms are now marked as proven, but remain in the AST.

Plugin Value

New Features

• Support for \subset predicate.
  
  
• Improvements to option -subdivide-float-var, when subdividing may avoid the emission of an alarm.
• New option -val-initialization-padding-globals to specify how padding bits should be initialized. Option -initialized-padding-globals is deprecated.
• Improved reduction by assertions of the form \initialized(&t[0..N]) when N is above -plevel.
• Option -subdivide-float-var has been renamed into -val-subdivide-non-linear, and has now an effect on non-linear integer expressions.
• Local variables that are in scope but not yet initialized are now present in the environment.
• In synthetic results, for local variables that are not those of the current function, the approximated values encompass only the callstacks for which the variables were in scope in one of the callers.
• Faster treatment of imprecise struct copying and left shifts in the logic.
• Fix bug in -memexec-all option in presence of instructions where evaluation was guaranteed to fail.
• Terms involving l-values that are bit-fields are now correctly handled.
• In -lib-entry mode, functions pointers no longer force the generation of dummy functions. Instead, they are initialized to NULL. Fixes bug #2104.
• New GUI panel 'Values', that displays nearly all the information previously available under the 'Information' panel.
• Added built-ins for mathematical functions: atan2, fmod, pow, expf, logf, log10f, powf, sqrtf, floor, floorf, ceil, ceilf, round, roundf, trunc, truncf.
• Improved reduction by predicate \initialized when the left argument is a range of locations.
• Functions call using a function pointer are now treated more leniently when too many arguments are supplied. An alarm is emitted, but execution continues with the right number of arguments.
• Option -val-split-return-auto now always split between NULL/non-NULL pointers.
• The semantics of copying a lvalue has been changed when a type mismatch occurs between the destination and the copied value. A bitwise reinterpretation of the value to the destination type is now performed during the copy.
• Do not emit pointer_comparable alarms on valid pointer comparisons involving objects of size 0.
• Float operations that are guaranteed to lead to +/-infty (e.g. x = FLT_MAX*10.) now stop propagation. Previous behavior was to continue with an imprecise value for x.
• Garbled mix origins now include at most one source location.
• All plugins that depend on Value, plus Value itself are now dynamic. Custom plugins must specify in their Makefile the plugins they depend on (e.g. PLUGIN_DEPENDENCIES:=Inout Value).
• WIDEN_HINTS directive are now cumulative with automatically inferred bounds. Fixes bug #876.
• The alarms raised when evaluating a global initializer that leads to an undefined behavior are now marked with an "Invalid" status.
• Assertions containing \at(P, L), where L is a C label, can now be evaluated. Evaluation is done once Value has run; thus, it ignores option -slevel.

Bug Fixes

• Fix incorrect initialization of padding bits. Option -initialized-padding was ignored in some cases.
• Fix initial state in which some volatile qualifiers for nested types were ignored.
• In -lib-entry mode, allow the generation of initial states with 0-sized bitfields.
• Pointer comparisons using relational operators (<, >=, etc) between a pointer and NULL is now flagged as undefined.
• Check the validity of the operands of the ACSL operators /, %, << and >> when evaluating a predicate.
• pointer_comparable alarms are now emitted with arguments properly cast to void* or void (*)().

Developers Only

• Removed function Cvalue.V.min_and_max_float. Use Cvalue.V.project_ival and Ival.min_and_max_float.
• Remove duplicate values Ival.singleton_zero and Ival.singleton_one. Use script sodium2magnesium.sh for automatic migration.

Plugin WP

New Features

• [Caveat]  New 'Caveat' memory model.
• [Coq]  Inductive if-then-else construct.
• [Qed]  Factorization of core equalities (-wp-core).
• [Qed]  Automatic introduction of existentials.
• [Qed]  Aggressive ite-lifting.
• [Qed]  More aggressive filtering and pruning (-wp-filter).
• [Qed]  More simplifications on strict inequalities.
• [Qed]  Fold constant expressions in goals.
• [Report]  Support for CVC4 reporting.
• [Typed]  Named shift operators (better triggers).
• [WP]  Now accept patterns in drivers.
• [WP]  Support for \subset.
• [WP]  Options -wp-*-vars to tune memory model detection.
• [WP]  More lemmas for bitwise operations.
• [WP]  New integer model '+rg'.
• [WP]  Simplifications of 'is_cint' with quantifiers.
• [WP]  Summarize initializers (-wp-init-summarize-array).
• [WP]  Improved -wp-check mode.
• [WP]  -wp-simplify-forall of quantifier guards (unsound).
• [WP]  -wp-simplify-type remove some most type constraints (sound, incomplete).
• [WP]  Refactoring of compound objects modeling.
• [WP]  Added solver mean time to console output.
• [WP]  Quiet output on TTY (see -tty kernel option).
• [WP]  Handle global constants (-wp-init-const).
• [WP]  Added support for float-classification. (\is_NaN, \is_finite, \is_infinite, \is_plus_infinity, \is_minus_infinity).

Bug Fixes

• [Hoare]  Fixed incorrect partial assignments in compound objects.
• [WP]  Fixed bug #1828 (separation of locals/formals/heap).
  
  
• [WP]  Fixed bug #1785 (fixed pre-condition with Clang).
• [WP]  Fix bugs with -wp-extern-arrays.
• [WP]  Fix sharing bug in proof obligation output.
• [WP]  Improved typing for alt-ergo let-bindings.
• [WP]  Fixed bug #1683 (duplicate Qed results).
• [WP]  Fixed bool-prop conversions.
• [WP]  Fixed bug #2079 (incorrect pointer arithmetics).
• [WP]  Fixed bug #1683 (multiply reported Qed proofs).
• [WP]  Fixed bug #2126 (0-shift rewriting).
• [WP]  Fixed bug #2127 (unsigned inequality).
• [WP]  Fixed bug #2078 (ill typed PO with void*).
• [WP]  Fixed bug #2144 (lost \result after explicit assignment).
• [WP]  Fixed bug #2141 (incorrect simplification of 'x%1').
• [WP]  Fixed bug #2110 (wrong premisses for structs assigns).
• [WP]  Fixed bug #2040 (wrong label Here in assumes).
• [WP]  Fixed bug #2082 (crash with \is_infinite).

Plugin E-ACSL

New Feature

• [e-acsl-gcc]  Add a convenience script e-acsl-gcc.sh for small runs of the E-ACSL plugin.

Bug Fixes

• [E-ACSL]  Fix bug #1817 about incorrect initialization of literal strings in global arrays with compound initializers.
• [e-acsl-gcc]  Add an e-acsl-gcc.sh option allowing to skip compilation of original sources.
• [Makefile]  Fix installation with custom --prefix.
• [runtime]  Fix a crash occuring when using a recent libc while GMP headers provided by E-ACSL are used.
  
  
• [runtime]  Fix bug in the memory model that caused the tracked size of heap memory be computed incorrectly.

Frama-C General

New Features

• [Cil]  Values extracted from initializers of const variables are now accepted as arguments of directives pragma loop UNROLL.
• [Cil]  Frama-C's x86 default machdeps no longer assume that the compiler is GCC. Some typing extensions and builtin are thus deactivated. If you want a GCC-centric analysis, use the gcc-prefixed machdeps.
• [Cil]  Option -pp-annot should be much faster when parsing files with many ACSL annotations.
• [Cil]  Default preprocessing command now includes Frama-C's standard library, and when possible sets option '-nostdinc'. See options -frama-c-stdlib and -cpp-gnu-like.
• [Kernel]  add instructions for downloading the manuals
• [Kernel]  require ocamlgraph version 1.8.5
• [Kernel]  Nicer error message in case of code incompatibility when loading a plug-in.
• [Kernel]  New option -const-readonly (set by default), that asserts that 'const' variables must never be written.
• [Kernel]  New way to handle command line options which accepts sets of values. Values may be prefixed by '+' or '-' to add/remove them and categories of values prefixed by '@' are available as well (for instance @all).
• [Kernel]  New option '-then-last', which behaves like '-then-on' on the last project created by a program transformer.
• [Kernel]  Improve pretty-printing of some loops.
• [Kernel]  Tests are added to the distrib (make tests).
• [Logic]  New builtin functions \min and \max of type Set(Integer) -> Int
• [Logic]  New logic label "Init", that refers to the state just after the initialization of globals.
• [Logic]  The ACSL predicate '\specified', which has been renamed to '!\dangling_contents' is now supported.
• [Logic]  The ACSL parser now ignores /*@{ and /*@} comments, to avoid conflicting with Doxygen.

Bug Fixes

• [Cil]  Fix erroneous integral promotion of type 'char' on architectures where 'char' is unsigned.
• [Cil]  Variables __FC_MACHDEP_FOO_BAR are now automatically positioned when setting a non-standard machdep and using Frama-C's standard library.
• [Configure]  fix for autoconf < 2.67 when checking ability of default pre-processor to keep comments
  
  
• [Configure]  use the gcc from the configure for compiling c files
• [Kernel]  Fix bug #1765 (spelling errors).
• [Kernel]  allow dynamically loaded module to start with a lower-case letter. Fixes #1276.
• [Kernel]  -load-module M now works fine if M uses the API of another plug-in (bts #1824).
• [Logic]  The ACSL parser accepts qualifiers in logic C types.
• [Makefile]  Do not install ZArith with Frama-C anymore.

Developers Only

• [Cil]  The ikind for Cil.kinteger64 is now optional.
• [Cil]  Modifications in some fields of type Cil_types.mach. Function File.new_machdep has a simpler type.
• [Cil]  The field 'vlogic' of type Cil_types.varinfo has been replaced by the field 'vsource', to avoid confusion with logic variables. The value of the new field is the negation of the previous one.
• [Cil]  Variables are created with a field 'vgenerated' set to 'false' by default. Only Cil should position this field to 'true'.
• [Cil]  Field 'vgenerated' of type Cil_types.varinfo has been replaced by the field 'vtemp' to emphasize the fact that it should only be set to true for temp variables generated during elaboration.
• [Kernel]  A new bunch of functors are available to define command line collections.
• [Logic]  Annotations.{iter,fold}_all_code_annot are now by default sorted. Use ~sorted:false in case of efficiency issues.
• [Makefile]  Fixed compilation bug for plug-ins with both a GUI and a non-empty API (bug #1798).

Frama-C GUI

• [Gui]  Logic l-values inside function specifications can now be selected
• [Gui]  New option -gui-project to run the GUI in a given project.
• [Gui]  C expressions can now be selected through the source panel.

Plugin From

• New option -from-verify-assigns to give assigns/from clauses of function with bodies a validity status.
• Major performance improvements on big analyses.

Plugin Inout

• Remove undocumented option -access-path

Plugin Report

• New option -report-callsite-preconditions.
• More consistent behavior when option -report-untried is not set.
• Better reporting of reachability statuses; do not coalesce unproven reachability assertions with other alarms.

Plugin Rte

• Very big floating-point constants that are converted to an integer are now reported as overflowing in only one direction

Plugin Semantic Constant

New Features

• Folding Floating-point constants can now be propagated.
• Folding Generate nicer constants for integers and pointers
• Folding New option -scf-project-name.
• Folding Reducing the number of introduced casts; feature issue #1697.
• Folding Reducing the number of introduced casts; feature #1787.

Bug Fix

• Folding Fix crashes and/or multiple declations when a global was referenced in the constant-folded project earlier than in the original one.

Plugin Slicing

• Fix issues about slicing calls to the main function and journalization (bug #1684).
• Fix crashes about multiple slicing pragma inside a function (bug #1768).

Plugin Value

New Features

• Option -val-after-results is now always active by default, and can no longer be unset
  
  
• Instructions whose execution is guaranteed to fail are now displayed in the GUI
• Alarms when converting integers to floating-point are now reported only for the range that overflows
• Preconditions of functions that are never called are now also marked as dead at each call-site.
• Alarms are now re-evaluated at the end of the analysis. If their truth value is 'Valid' or 'Invalid', this more precise status is used, instead of the previous 'Unknown' one.
• Improve precision of &.
• File-scope and formal const variables are read-only. Any possibility of writing there is treated as alarm.
• Complete rewrite of the modules Int_Intervals and Offsetmap_bitwise; both are now implemented with the same datastructure as Offsetmap. Many performance improvements. Many changes in the API of module Offsetmap_bitwise. Few changes in Int_Intervals, but the englobing module Lattice_Interval_Set has been removed.
• When option -val-callstack-results is set, the GUI now displays a callstacks-wide consolidation of the possibles values for expressions and terms. Previously, the potentially less precise summary state was used.
• The GUI now showns the value of logic l-values inside function specifications. They are evaluated in the pre-state of the function, before the evaluation of preconditions.
• Improved widening on variables that are used to access an array
• Improved pretty-printing of variables containing pointers.
• Improve conversion of float values that have been written as integers (through low-level memory accesses)
• Option -val-split-return can now be used to split between NULL / non-NULL pointers
• More systematic emission of message 'operation [...] incurs a loss of precision', signaling an arithmetic operation on a pointer address. This message is now emitted by Value itself.
• The arguments of an invalid shift operation are now reduced so that they belong to the proper range.
• Message 'extracting bits of a pointer' is no longer emitted, as it was redundant with the warnings about garbled mix.
• Better precision when a scalar value is written through a garbled mix.
• Reduce arguments of a function according to the possible values of the formal at the end of the call.
• Arguments of functions that give rise to an alarm are now reduced when possible.
• Indeterminate bits copied when option -val-warn-copy-indeterminate is active now cause a reduction in the source location.
• Logic ranges are now evaluated using a dedicated lattice. Results are almost always more precise, and the analysis faster.
• Per-callstack results are now always computed. Option -val-callstack-results is deprecated.
• Option -slevel-merge-after-loop renamed to -val-slevel-merge-after-loop. Now takes a set of kernel functions as an argument.
• Removed message "assigning non-deterministic value from the first time".
• Accesses to '*(foo *)p' may now reduce p according to the validity of the access, when useful.
• Accesses to locations that contain garbled mix now cause the garbled mix to be reduced to the set of valid locations.
• Special functions CEA_ are deprecated. Use Frama_C_show_each or Frama_C_dump_each instead.

Bug Fixes

• Dividing an integer value by a memory address requires the address to be comparable to NULL.
• Fix evaluation of '/' in the logic, that silently ignored the presence of the value 0 in the divisor.
• Text-only alarms that used the '\defined' predicate (to warn about dereferencing pointers to out-of-scope variables) are now emitted with the '\dangling_contents predicate.
• When for missing '\from' clause for '\result' when result is used in a postcondition. Fixes bug #1908.
• Fix bug when writing precise values at too many locations in packed arrays.
• Improved precision for variables that are reduced (but not written) during a call memorized by option -memexec-all

Developers Only

• Major API change in directories src/ai and src/memory_state. Functions no longer take ~with_alarms arguments. Instead, they return booleans, that indicate an alarm occurred.
• Function Cvalue.Model.find does *not* signal its result is indeterminate anymore. Use function Cvalue.Model.find_unspecified instead.
• Multiple low-level functions have been removed from modules Cvalue.V and Cvalue.Model, and are no longer available.
• Argument ~conflate_bottom to Cvalue.Model.find is now optional. The documentation has been updated to better explain its meaning.
• Some functions of modules Offsetmap, Lmap, Cvalue.V_Offsetmap and Cvalue.Model now require a separate Locations.Location_Bits.t and (integer) size, instead of a Locations.location. This avoids errors when the case was Int_Base.Top.
• Functions find_base and find_base_or_default in modules Lmap and Cvalue.Model now return an optional type, to account for invalid bases (that may not be present in the map).
• Improve and clarify the return conventions of modules Offsetmap, Lmap, Cvalue.V_Offsetmap and Cvalue.Model, by returning three cases: `Bottom, `Top and `Map. The latter case indicates the operation succeeded precisely'.
• API of module Cvalue.V_Or_Uninitialized is now type-safe. Replace all occurrences of 'get_flags v' by 'v'.
• Most iterators of module Lmap and Cvalue.Model now accept only the non-bottom and non-top cases.
• Value 'empty' is no longer exported in module Offsetmap. The API should prevent any accidental creation.
• Garbled mix (constructor Top in modules Location_Bits/Bytes) now explicitly mention the NULL base.
• Remove experimental support for periodic bases.

Plugin WP

New Features

• [Cmd]  Added option -wp-filename-truncation to truncate proof obligation filenames.
  
  
• [Typed]  Simplification of assigns and separated.
• [WP]  Some improvements on bitwise operators.
• [WP]  Next to the new way the kernel handles command line options, -wp-include +dir has to be replaced by -wp-include ++dir. Forward and backward compatibilities are broken.
• [WP]  Drivers for min/max.

Bug Fix

• [GUI]  Fixed bug #1688 (recover results from cmdline).

Plugin E-ACSL

New Features

• [E-ACSL]  Compatibility with new Frama-C Sodium option -frama-c-stdlib.
• [E-ACSL]  Search .h in the E-ACSL memory model by default (easier to use declarations like __memory_size).
• [E-ACSL]  Support of \freeable. Thus illegal calls to free (e.g. double free) are detected.

Bug Fixes

• [E-ACSL]  Add a missing cast when translating an integral type used in a floating point/real context in an annotation.
  
  
• [E-ACSL]  Fix bugs #1636 and #1837 about scoping of literal strings.
• [E-ACSL]  Fix bug when using fopen.
• [E-ACSL]  Fix types of \block_length and \offset.

Developers Only

• [E-ACSL]  Export a minimal API for other plug-ins.

Frama-C General

New Features

• [Configure]  New option --disable-local-ocamlgraph to disable the use of the OcamlGraph version provided by Frama-C.
• [Journal]  By default, the journal is now generated into the Frama-C session directory.
• [Kernel]  Support parsing and printing "asm goto" from gcc 4.6. Added a component to Cil_types.Asm constructor.
• [Kernel]  The annotation 'loop pragma UNROLL "done", n;' disables the unrolling of the annoted loop. Option -ulevel-force has to to used for enabling the transformation of such a loop. This pragma is introduced by the unrolling process in order to prevent unrolling on source code obtained by a previous frama-C run.
• [Kernel]  Better strategy when -save is set and Frama-C crashes (bts #1388).
• [Kernel]  Renamed argument ~cache of functions cached_fold into ~cache_name. The previous integer is no longer used.
• [Kernel]  An 'unknown' local status is set on assigns generated from the C prototype of leaf functions
• [Kernel]  Add -aggressive-merging option to merge two inline functions if they are equal modulo alpha conversion.
• [Kernel]  Support for static evaluation of the __builtin_compatible_p GCC specific function.
• [Kernel]  Generate more aggressive assigns clauses for unspecified library functions that arguments with type pointer to void or char
• [Kernel]  Support for binary literal constants in C and in logic denoted by '0[bB][01]+' (common ISO/C extension).
• [Kernel]  "-machdep help" now specifies the default machdep (bts #1558).
• [Kernel]  FRAMAC_PLUGIN may now specify a list of comma-separated directories instead of a single one.
• [Kernel]  Assigns clauses generated by the kernel for functions with neither a specification nor a body receive an 'Unknown' status.
• [Logic]  Improve localisation of error messages during logic typing.

Bug Fixes

• [Cil]  Do not pretty-print while(1) into while(c) when the 'break' branch is not reduced to a single break, or contains an annotation
• [Cil]  Fixes issue #1589 (do not drop access to volatile lvals in pure expressions).
• [Kernel]  Fix pretty-printing of comments in ghost code (bts #1378 and #1404).
• [Kernel]  Fix incorrect dot output of consolidation graph of property statuses.
• [Kernel]  Fix consolidation algorithm of property statuses which possibly occurs on cycles involving an unproved property (bts #1443).
• [Kernel]  implicit annotation status is not lost through code transformations anymore. Fixes bug #1442
• [Kernel]  more informative error message. Fixes bug #1352
• [Kernel]  Tmp vars created during typecheck all have a description. Fixes bug #1387
• [Kernel]  designated initializers are correctly pretty-printed. Fixes issue #1457
• [Kernel]  More clever merge of function contracts. Fixes issue #1455
• [Kernel]  Fixes binding of formals when linking static prototypes. Fixes issue #1475
• [Kernel]  Fixes issue #1451 about -unicode which was not taken into account by -load-script.
• [Kernel]  Reject identifiers in the same namespace and same scope, according to C standard's rules. fixes bug #1330.
• [Kernel]  Statements with a label attached to them are never erased during elaboration. Fixes #1502.
• [Kernel]  Correctly distinguish typenames and declared identifiers in declarations. Fixes #1500
• [Kernel]  Do not generate invalid assigns clauses when some formals are pointers to arrays
• [Kernel]  Do not consider array variable as read lval in unspecified sequence. It can't be written anyway. Fixes #1519
• [Kernel]  Do not fail on nested ternary operators whose value is dropped, as in #1503
• [Kernel]  Fixes loop unrolling having in their body 'switch' with 'continue' stmts.
• [Kernel]  The parsed value could be wrong and the warning for inexact decimal floating-point constants be wrongly omitted for constants smaller than the smallest subnormal.
• [Kernel]  Fix bug which may occur when pretty printing range of terms.
• [Kernel]  Fixed parsing bug with decimal single-precision floating-point literals representing numbers above MAX_FLOAT.
• [Kernel]  Fix typing of variadic arguments.
• [Kernel]  Fix -machdep help in presence of other actions (bts #1643).
• [Logic]  Conversion from C array to pointers do not lose cast on pointed types. Fixes issue #1469
• [Logic]  Disallow cyclic logic type definitions
• [Logic]  Accept struct with same name as typedef in specs. Fixes #1518
• [Logic]  Do not remove labels out of scope of annotations too quickly. Fixes #1536
• [Logic]  -check checks that C and associated logic variable agree on their type. transfer completion of type up to associated logic var and term when needed. Fixes #1538
• [Logic]  do not cast an enum value toward its associated integral type when comparing to an enum constant. Fixes #1546
• [Logic]  Support for _Bool in ACSL formulas
• [Project]  Fix messages about projects.

Developers Only

• [Cil]  Rename function sizeOf_int into bytesSizeOf.
• [Cil]  Statements containing calls to va_start can now be printed outside of a function
• [Cil]  Terms containing ACSL keywords are now properly parsed by function Logic_lexer.lexpr
• [Doc]  Fix ugly display of documentation of dynamic plug-ins API (bts #1394).
• [Kernel]  adding a category do not set debugging level to 1. Conversely debug ~dkey "..." (without ~level) will output "..." if dkey is requested by the user, even if debugging level is 0.
• [Kernel]  Add hook builders for hooks that can have dependencies. See src/lib/hook.mli
• [Kernel]  Add hooks to register transformation to be performed on a freshly computed AST. See src/kernel/file.mli
• [Kernel]  Added StringList.append_{before,after} for manipulating options (both static and dynamic API)
• [Kernel]  Added hooks when registering/removing a property
• [Kernel]  Cil.mkEmptyStmt gets a valid_sid argument in order to generate valid statements.
• [Kernel]  Fixed buggy function Property.location.
• [Kernel]  Alpha.{new,register}AlphaName: transform labelled argument 'undolist' with option type into optional argument.
• [Kernel]  Plug-ins may now have their own session directory in which they can generate project-dependent files during a Frama-C session.
• [Kernel]  Plug-ins may now have their own configuration directory in which they can generate configuration files during a Frama-C session.
• [Kernel]  parameters can be preserved across project creation through copy visitor (do_not_reset_on_copy function). fixes do_not_projectify and do_not_reset_on_copy status of Kernel's options.
• [Kernel]  Plug-ins may now have a non-empty .mli interface. It deprecates the old way to register them through module Db or Dynamic (this last one may remain useful for mutually recursive plug-ins).
• [Kernel]  For building a datatype, you now need to use smart constructors provided in Structural_descr.
• [Kernel]  Removed Db.Dominators. Use the Dominators kernel module instead.
• [Kernel]  Changes to the signatures in lattice_type: top and bottom are now optional, a join_and_is_included function is required, and Upper_Semi_Lattice was renamed to Join_Semi_Lattice.
• [Kernel]  The module Parameter_sig now contains the signatures of command line options (was in module Plugin).
• [Kernel]  Parameter is now called Typed_parameter.
• [Kernel]  The module Parameter_customize now contains the functions to customize command line options (was in module Plugin).
• [Kernel]  The module Parameter_state now contains the functions to select group of parameters (was in module Plugin).
• [Lib]  Filepath.normalize can replace paths by a symbolic name.
• [Logic]  Better specification and more checks on Annotations.{add,remove}_* functions (fixes bug #1635).
• [Makefile]  Split Makefile.common in two parts in order to include generic rules (new Makefile.generic file) at the end of main Makefile, so specialized patterns will be considered first in make < v3.82
• [Ptests]  add the possibility to define macros in configurations. See developer documentation.
• [Ptests]  Use ptests.opt whenever possible.

Frama-C GUI

• [Gui]  the configuration file .frama-c-gui.config is now put in the GUI config directory and named frama-c-gui.config.

Plugin From

New Features

• Slowndowns in the analyses can be mitigated using higher values for option -memory-footprint
• Better precision when querying information about a zone that has the same dependencies as its neighbors.
• Separately compute data dependencies and indirect (address, control) dependencies with option -show-indirect-deps
• Fix possibly invalid dependencies for functions that return partially-written structs.

Bug Fixes

• Position the 'and SELF' flag when an assigns clause z1 and z2 overlap in an assigns clause z1 \from z2 .
• Fix incorrect dependencies with code of the form 'f(); x = 1; f();' when f assigns a value with a right-hand side that depends on x.

Developers Only

• Results of From cannot be intercepted by Log.add_listener anymore. Use Db.From.{pretty,display} to print them.

Plugin Impact

• More generic dynamic function impact_statement_gui. The set of nodes impacted can now be filtered by a memory zone.

Plugin Inout

• Inputs of an instruction whose evaluation fails now include the sub-expressions for which evaluation succeeds

Plugin Metrics

• More precise information about coverage
• ACSL statistics

Plugin Obfuscator

New Features

• Print the category which each symbol belongs to (bts #1566).
• Obfuscate labels (bts #1562).
• Obfuscate (most of) logical constructs (bts #1563).
• Handle literal strings in a separate dictionary (bts #1564).
• Warn about unobfuscated symbols.
• New option -obfuscator-dictionary to generate the dictionary into a file.
• New option -obfuscator-string-dictionary to generate the dictionary of literal strings into a separated file.

Bug Fix

• Now properly handle option -ocode.

Plugin PDG

• Function Db.Pdg.find_stmt_and_blocks_nodes returns a correct result on partially dead composite statements

Plugin Pdg

• Fix possible non-termination during the computation of the control dependencies (bug #1436)
• Shorter output when outputting results
• Results of Pdg cannot be intercepted by Log.add_listener anymore. Use Db.Pdg.get and Db.Pdg.pretty instead.

Plugin Report

• New option -report-untried

Plugin RTE

• Better normalization when using -rte-precond.
• Remove limitation about alarms which do not fit into 64 bits (bts #1391).

Plugin Rte

• No assertions are generated for unsigned left-shift that may overflow, regardless of whether -warn-unsigned-overflow is set. Fixes issue #1555.

Plugin Scope

• Option -inout-callwise can be used to improve the precision of computations, including the effects of option -remove-redundant-alarms. Option -calldeps is no longer necessary
• Functions registered in Db now return Stmt.Hptset values instead of Stmt.Set

Plugin Semantic Constant

• Folding Fixes error when folding fct pointer resulting in two distinct kf for the same function.

Plugin Slicing

New Features

• Better slicing of complex logical assertions (bug #690).
• -slice-calls main only selects the calls to the main function, nothing more.

Bug Fixes

• Fix crash in presence of assertions involving sizeof(t), where t is an array. Fixes similar bug with option -remove-redudant-alarms
• Slicing on a composite statement containing dead code now works properly
• Slicing is now compatible with option -val-use-spec

Plugin Syntactic_callgraph

• Remove option -cg-services-only which was unused since a while.

Plugin Value

New Features

• Frama_C_show_foo functions now display struct arguments in extenso.
• Distinguish unreachable state and invalid location when printing the value of a l-value in the GUI
• Basic support for \inter logical predicate (treated as an union).
• Evaluation of \base_addr, \offset and \block_length logic predicates.
• Preliminary support on \forall and \exists quantification when the introduced variables have a C type.
• Assertions on dead code now get a "true because unreachable" status.
• The name of an evaluated property is now displayed in the log message. Fixes wish #1415.
• Option -memory-footprint now accepts much bigger arguments. The size allocated to each cache is multiplied by 2 between each increment.
• Better documentation of module Hptmap. Some incompatible API changes.
• Better widening bound for signed 32 bits integers
• Fewer and better widening bounds for pointer addresses: try the frontier of the block
• Warn for missing '\from' or 'assigns \result \from' clauses. Fixes wish #1448
• More aggressive evaluation of \initialized(p) when p points to a memory zone containing both bottom and non-bottom values
• Value analysis can now be aborted while keeping intermediate results, by sending SIGUSR1 to Frama-C
• Degeneration points are now shown in the GUI
• Syntactic loops (ie. 'for', 'while' and 'do ... while') are now always used to perform widening, regardless of whether they are reducible
• Evaluation of left-values such as t[i][j] or p->arr[i] is now more precise when the total number of locations to read or write is less than the value of -plevel option
• No alarms are emitted for overflowing unsigned left shift operations.
• Pointer subtraction now requires that the pointers refer to the same allocated block, and returns the pointwise difference between the corresponding offsets. Use -no-val-warn-pointer-subtraction to obtain the previous behavior.
• The option -val-left-shift-negative-alarms has been renamed into -val-warn-left-shift-negative
• Passing a struct containing uninitialized fields or padding bits to a function without a body no longer raises an alarm.
• Copies of non-struct left-values that contain indeterminate bits can now be reported using option -val-warn-copy-indeterminate.
• Improve precision of bitwise conversion from floating-point value to integers
• Experimental option -slevel-merge-after-loop
• Volatile pointers are now modeled as the base addresses that are stored into the pointer, shifted by an unspecified offset.
• Display information about temporaries when emitting an alarm
• Ensure convergence in presence of some non-natural loops
• Improve precision of treatment of: if ((int)floatvar == intexpr)
• Improve precision of treatment of x = e1 & e2;
• Replace mostly-inoperant option -memory-footprint by an environment variable FRAMA_C_MEMORY_FOOTPRINT
• Fix spurious messages about integer overflow when an arithmetic operation is guaranteed to result in an undefined behavior.
• For functions for which only the specification is available, non-invalid statuses are no longer reported when evaluating a postcondition. Invalid statuses are reported, and usually indicate a specification error.

Bug Fixes

• Failure during a memory zone copy is now properly notified. Alarms were emitted, but a non-bottom result was simultaneously returned.
• Fix crash when the creation of the initial state encounters a completely invalid compound initializer.
• Fix crash when evaluating \valid(p->off) when p is NULL or a valid pointer, and p->off is itself only partially valid (bug #1486).
• Fixed bug involving the conversion to float of a double expression e s.t. 0 < fabs(e) <= 0x1.0p-150.
• Prevent GUI crashes when options -no-results or -obviously-terminates are set and some functions have ACSL preconditions
• Ensures that sqrt(-0.) is -0., even with buggy MSVC runtime. Fixes bug #1396
• Fix potentially invalid source line number in origin of Merge garbled mix values.
• Fix rare crash during widening operation in C union intensive code
• Fix possible unsoundness in presence of &. (unsoundness never observed in practice)
• Fix crash on analyses involving very imprecise pointers and a partially valid absolute memory range
• Fix missing read/written zones and dependencies when accessing a completely imprecise pointer (garbled mix) and using option -absolute-valid-range. Impacts the results of plugins Inout, From, Pdg, Impact and Slicing.
• Fixed spurious warning about floating-point values containing addresses.
• Remove support for ACSL \inter operator, which could lead to unsoundness with predicates involving the empty set (fixes bug #1624)
• Fix potential unsoundness in the operation testing the inclusion of two memory states (never observed in practice)
• Fix bug when writing imprecisely in a struct containing a 1-bit wide bitfield (bug #1671)

Developers Only

• Remove functions Cvalue.Model.pretty_without_null and Db.Value.display_globals. Function Db.Value.display is now a reference to the real function. Removed last argument of Cvalue.Model.pretty_filter.
  
  
• Results of Value cannot be intercepted by Log.add_listener anymore. Use Db.Value.display to print them
• Do not crash when printing arrays or structs containing abstract structs (bug #1416).
• API change in module Base. Use script bin/fluorine2neon.sh for automatic migration.
• Function Cvalue.Model.find_unspecified now requires one additional argument ~conflate_bottom
• Fix bug in which two distinct memory states could be erroneously made equal
• Minor signature change for widening functions
• Function Map_Lattice.Make requires a new argument
• Type Base.string_id is now concrete. No more need for function Base.cstring_of_string_id
• Functions previously required by some functors in directories src/ai and src/memory_state are no longer needed. Use script bin/fluorine2neon.sh for partially automatic migration.
• Harmonisation and simplifications of functions related to memory states in Cvalue.Model. Different functions are now available for updating, refining and creating a state

Plugin WP

New Features

• [Driver]  Refactoring of prover external libraries. (consult driver section in manual).
• [GUI]  Consistent icons with status.
• [GUI]  Edition of current proof script (right-click).
• [WP]  More type constraints in typed memory model.
  
  
• [WP]  Clever assigns everything with formals and locals.
• [WP]  Better integration with Why-3 and Coq.
• [WP]  Many improvements on bitwise operators.
• [WP]  Many improvements on reals and floats.

Bug Fixes

• [WP]  Major speed-up for huge functions.
• [WP]  Important bug-fix in CFG (missing hyps in goals).

Plugin E-ACSL

New Features

• [E-ACSL]  Remove a spurious warning when an annotated function is first declared, then defined.
• [E-ACSL]  Remove spurious warnings when using type real numbers.

Bug Fixes

• [E-ACSL]  Fix bug #1700 about non-ISO empty struct.
  
  
• [E-ACSL]  Fix bug #1715 about -e-acsl-full-mmodel which generates incorrect code.
• [E-ACSL]  Fix bug #1716 with annotations in while(1).
• [E-ACSL]  Fix bug #1717 about instrumentation of labeled statements.
• [E-ACSL]  Fix bug #1692 about wrong localisation of some messages.
• [E-ACSL]  Fix bug #1782 about incorrect URL in the documentation.
• [E-ACSL]  Fix bug #1695 about using some part of the (Frama-C) libc which prevents linking of the generated C code.
• [E-ACSL]  Fix bug #1836 about one-off error when computing the block which a pointer points to.
• [E-ACSL]  Fix bug #1831 about argc and argv.
• [E-ACSL]  Fix bug #1696 by clarifying the manual.
• [E-ACSL]  Fix bug #1818 about initialization of globals.
• [E-ACSL]  Fix bug #1838 about memset.

Plugin E-ACSL

• [E-ACSL]  Fix bug #1634 occuring in presence of static addresses.
• [E-ACSL]  Fix incorrectness which may occur in presence of aliasing.
• [E-ACSL]  Some loop invariants were tagged as "assertions".
  
  

Plugin Value

• Add missing C library files.
  
  

Plugin E-ACSL

New Features

• [E-ACSL]  Fewer unknown locations.
• [E-ACSL]  Support of loop invariants.
• [E-ACSL]  Use GMP still less often.
• [E-ACSL]  More precise message for unsupported contract clauses.
• [runtime]  Improve ACSL contracts of the E-ACSL C library.

Bug Fixes

• [E-ACSL]  Fix -e-acsl-debug n, with n >= 2.
  
  
• [E-ACSL]  Fix bug when generating RTEs on the E-ACSL generated project.
• [E-ACSL]  Fix crash with typedef on pointer types.
• [E-ACSL]  Fix bug when mixing -e-acsl-prepare and running E-ACSL in another project (bts #1473).
• [E-ACSL]  Fix bug when monitored global variables have initializers (bts #1478).
• [E-ACSL]  Fix bug which may occur with divisions and modulos.

Frama-C General

• [Kernel]  Fixed Type.pp_ml_name for polymorphic types with 3 and 4 type variables (bug #1127).
• [Makefile]  Fixed installation directory of the doc in plug-in's Makefile (bug #1278).
  
  

Plugin RTE

• Fix off-by-one error in alarms on overflowing unsigned unary minuses.

Plugin Value

• Better precision for ^ (bitwise xor) operator when applied on intervals of positive integers
• Catch evaluation errors when selecting a logic l-value in the GUI.

Plugin WP

• [Provers]  Fixed various bugs with drivers and provers.
• [Typed]  Better trigger generation for arrays with Alt-Ergo.
• [Typed]  Fixed bug on address differences and offsets.
  
  
• [WP]  Fixed various bugs on floats.

Frama-C General

New Features

• [Cil]  The type of fields that are bit-fields now carry an informative attribute FRAMA_C_BITFIELD_SIZE.
• [Cil]  Handles interpretation of linemarker ending by // and cleanup file paths.
• [Kernel]  Assumptions and axioms now get consolidated status "Considered valid" instead of "Valid".
• [Kernel]  Option -enums for choosing representation of enums.
• [Kernel]  When printing the AST, display the emitter name of generated annotations and also the origin of annotations corresponding to an alarm.
• [Kernel]  Better frama-c.top (fixed issue #1287).
• [Kernel]  Syntactic constant folding is done once by AST (fixed bug #1306).
• [Kernel]  The level of verbose is at least the level of debug.
• [Kernel]  Print signed downcast alarms as 'signed_downcast'
• [Kernel]  Signed downcast alarms are no longer emitted by default. Use option -warn-signed-downcast to activate them.
• [Kernel]  Signed overflow alarms are now emitted by default.
• [Logic]  Extended syntax for naming terms and predicates ("string":pred and "string":term are now allowed).
• [Logic]  Improved merge strategy for assigns, and report the presence of different assigns clauses between two files.

Bug Fixes

• [Kernel]  Fixed bug with Type.pp_ml_name for pairs, triples and quadruples which can lead to incorrect journal generation (new occurrence of bts #1127).
• [Kernel]  Do not attempt to merge unrelated anonymous enum that have been given the same name by Cil (fixes #1283).
• [Kernel]  Do not print help of negative options when the positive one is invisible (fixed #1295).
• [Kernel]  Fixed discrepancy between compare_type and hash_type. Added new datatype TypNoUnroll.
• [Kernel]  Fixed bug #1347 about accessing to a consolidated status of a property which depends on removed hypotheses.
• [Kernel]  Add lv_kind field to trace origin of logic variables. Cil_const.make_logic_var is deprecated in favor of specialized.
• [Kernel]  Ghost status is appropriately propagated in statements (instead of only instructions) and pretty-printed accordingly. Fixes issue #1328.
• [Logic]  Fixes various type-checking issues in presence of polymorphism and implicit conversions (including #1146).
• [Makefile]  Compile OcamlGraph less often: fixes issue #1343.

Developers Only

• [Cil]  Remove unused 'alignof_char_array' machdep field.
• [Cil]  Renamed function Cil.alignOf_int into bytesAlignOf.
• [Cil]  Clean up registering of new machdeps. Some machdep options have been integrated into Cil_types.mach, or removed from Cil.theMachine (as they were already in Cil_types.mach).
• [Cil]  Remove Cil pretty-printer. Use module Printer instead. The script bin/oxygen2fluorine.sh may be used to automatically convert your code.
• [Kernel]  Fixed consistency check of descriptor when building polymorphic datatypes (fixed bts #1277).
  
  
• [Kernel]  Provide Datatype.triple and Datatype.quadruple (bts wish #1277).
• [Kernel]  Optional argument 'reorder' to File.* functions creating an AST in a new project from a visitor.
• [Kernel]  Fixes incorrect visitor behavior with JustCopy (issue #1282).
• [Kernel]  New API for module Alarms.
• [Kernel]  New function 'get' for projectified counters.
• [Kernel]  Renamed Kernel_function.self to Kernel_function.auxiliary_kf_stmt_state to avoid confusion.
• [Kernel]  Get rid of useless rooted_code_annotation datatype.
• [Kernel]  New function Annotations.model_fields.
• [Kernel]  Signature change for constructor LReal.
• [Kernel]  Remove unintuitive ?prj argument from Cil visitors, and first argument of Visitor.generic_frama_c_visitor. Information is now stored inside the type Cil.visitor_behavior.
• [Kernel]  Added TLogic_coerce constructor to mark explicitly a conversion from a C type to a logical one (in particular floating point -> real and integral -> integer). Fixes issue #1309.
• [Kernel]  Various types whose names started by t_ in PDG/slicing related modules are now unprefixed.
• [Kernel]  Remove Cilutil's pretty printing helpers. Use Pretty_utils' ones instead.
• [Kernel]  Reorganize AST's pretty-printers. You must now use module Printer. Use the script oxygen2fluorine.sh to upgrade your plug-in.
• [Kernel]  Module Cilutil has been removed. Previously used list functions can now be found in Extlib (use script oxygen2fluorine.sh for migration). Functions related to configuration files are now Cilconfig.
• [Kernel]  Added type modules Cil_datatype.Wide_string and Datatype.List_with_collections.
• [Kernel]  Added pp_field and pp_model_field in Printer_api.
• [Kernel]  New methods videntified_term and videntified_predicate for the visitor.
• [Kernel]  Remove method is_annot_before from visitors (it return only 'true').
• [Kernel]  Visitor no longer crashes when a non-function global is replaced by a list containing at least one function or prototype (fixes bug #1349).
• [Kernel]  redesign of message categories. See detailed changelog for more information.
• [Kernel]  Must register keywords introducing new clauses of ACSL contracts. Fixes issue #1358.
• [Logic]  Change Property_status.Consolidation_graph.dump now takes a formatter instead of a file name.
• [Makefile]  Fix installation directory of API documentation (fixed bts #1278).

Frama-C GUI

• [Gui]  In some cases, after a crash of an analyzer, the GUI was not fully restored, became inconsistent and could crash.

Plugin Aorai

• Adds locations modified by Aorai to existing loop assigns (fixes issue #1290).

Plugin From

• Fix rare bug in presence of involved control-flow graphs and non-terminating calls.
• Fix absence of effect of option -calldeps after a save/load cycle.

Plugin Impact

• Prevent crash when a caller or callee function has been imprecisely analyzed.
• Prevent crash when considering a function with an unreachable first statement.
• Function Db.Impact.compute_pragmas now returns a list of statements.

Plugin Inout

• Fix absence of effect option -inout-callwise after a save/load cycle.
• Indirect reads (for example 'p' for '*p') are now automatically added to inputs when evaluating assigns.

Plugin Metrics

• Global variables both declared and defined were counted twice.
• Option -value-metrics now report a correct location for function referenced by an initializer. Fixes #1361.

Plugin Obfuscator

• Hide variables that do not appear in the output from the dictionary.

Plugin Pdg

• Ignore inline asm statements (previous behavior was to generate Top Pdgs).
• InCtrl nodes are no longer displayed in Dot graphs.
• Fix display for control dependencies in PDG graphs.

Plugin Rte

New Features

• Remove option -rte-print. Use -print instead.
• Generate Value-compatible alarms and annotations.
• Removed options -rte-signed, rte-unsigned-ov, -rte-downcast and -rte-unsigned-downcast. They are replaced by -warn-signed-overflow, -warn-unsigned-overflow, -warn-signed-downcast and -warn-unsigned-downcast respectively.

Bug Fix

• Added missing alarm for casts from overly large floating-point numbers to integer. Fixes #1318.

Developers Only

• Export function "exp_annotations" to get RTEs of a C expression as annotations.

Plugin Scope

• Prevent crash in defs computation when a lvalue is a formal.

Plugin Slicing

• Fix incorrectness in presence of assertions involving \initialized predicate. User predicates are no longer treated.
• Fix options -slice-assert and -slice-threat (-threat did nothing, -assert selected all alarms).
• Remove no longer used ~ai argument.
• Alarms are now removed in the generated project (regardless of option -slicing-keep-annotations).

Plugin Sparecode

• Alarms are now ignored during the analysis.
• RTE or Value-generated alarms are now removed in the generated project.

Plugin Value

New Features

• Reduce more aggressively on accesses *p where p is imprecise but contains only one valid value.
• New option -val-callstack-results to record and display in GUI the results split by callstacks.
• More precise line numbers for statuses of assertions and loop invariants.
• Improve handling of conditionals when option -val-ilevel is used.
• Evaluation of assigns now include indirect reads (ie 'assigns *p' depends on p) automatically.
• More agressive analysis of statements with improperly sequenced accesses when option -unspecified-access is used.
• More aggressive reduction in presence of write through partially invalid pointers. Warn if the pointer is completely invalid.
• Alarms emitted by Value are no longer evaluated during analysis (unlike user assertions).
• Value more aggressive evaluation of construct '//@ for b: assert p' when b is guaranteed to be active. Harmonize behaviors-related messages.
• Improved support for abstract structs.
• Improve reduction by conditions that involve '&' and '|' operators.
• Suppress superfluous warning when passing as argument a struct that contains pointers.
• Offsets in misaligned values that repeat themselves are now always printed relatively to the beginning of the binding.
• Renamed options -initialized-padding-globals and -no-no-results into -uninitialized-padding-globals and -val-store-results respectively.
• Improved support for va_arg variadic macro.
• Option -val-ignore-recursive-calls now uses the assigns clauses of the recursive function to treat the call.
• Emit proper alarms for completely imprecise floating-point values, and for casts from float to int.
• Removed option -val-signed-overflow-alarms. Use -warn-signed-overflow instead.
• Signed overflows now cause an alarm. Option -no-warn-signed-overflow can be used to get 2's complement.
• Consolidated states are now stored before 'assert' clauses are evaluatued.
• Optionally warn against unsigned overflows according to option -warn-unsigned-overflow.
• The first element of a -lib-entry allocated array, or of an array passed as an argument to main, is now valid regardless of option -valid-context-pointers.
• Better precision for postconditions in functions with multiple return analyzed without slevel.
• The location in which the result of a call is stored is now evaluated before the call. A warning is emitted if this location has changed after the call.
• Highlight non-terminating calls.

Bug Fixes

• Fix "Semantic level unrolling superposing up to" messages. The number displayed was sometimes lower than the actual number of superposed states.
• A bug causing the number of superposed states to be slightly underestimated has been fixed. As a result, it may be necessary to up the -slevel argument a little bit for existing proof scripts.
• Correct potentially incorrect reduction on l-values of the form *(p+off) or *(p-off).
• Fix soundness bugs for comparisons with logic constants that are not representable as 64 bits double.
• Fix evaluation of logic constant characters above 127.
• Option -absolute-valid-range can now be changed between two executions of Value.
• Various changes in the way undefined functions returning pointers are handled.
• Ignore 'const' qualifier on extern globals in lib-entry mode. Previously, those globals were initialized to 0.
• Fix erroneous casting operating when interpreting logic casts.
• Fix validities of degenerate variables, which were too big considering the size of the memory.
• Improved again support for abstract structs.
• In -lib-entry mode, void* fields or pointers now point to something potentially valid.
• Initial state of Value does not depend on -main option, but depends on -context-<...>.
• Fix incorrect reduction in integers containing pointers address when option -warn-signed-overflow is set.
• Option -memexec is now correct in presence of RTE alarms.
• Fixed misleading "after statement" state on statements followed by an assertion.
• Fix incorrectness of option -remove-redundant-alarms in presence of '\initialized(...)' alarms.
• Fix incorrect interpretation of \valid{L}(P) when L is not Here label.

Developers Only

• Remove various instances of Top_Param, which were all equal to Base.SetLattice.
• Builtins must now warn if their results should not be cached (signature change in Db.Value.builtin_result).
• Removed Base.All validity. Use big validities with unknown flag instead. Improved signature of Base.Unknown.
• Renamed Locations.valid_enumerate_bits into Locations.enumerate_valid_bits.
• Generic types of Value are now in Value_types (previously Value_aux). Implies a signature change for Db.Value.register_builtin. Value_aux.accept_base is now in Db.Semantic_Callgraph.

Plugin WP

New Features

• [Cmd]  Using -wp-prover instead of -wp-proof (kept for compatibility).
• [Cmd]  Added option -wp-skip-fct to exclude functions.
• [Cmd]  Removed now useless options -wp-huge, -wp-dot, -wp-trace.
• [GUI]  New Why3 provers selection, added -wp-detect to force detection.
• [Typed]  Extensions of Typed model (unsafe-casts).
• [Why] 3 Why3 output (-wp-proof why3:xxx).
• [WP]  Drivers for linking ACSL symbols to external libs (-wp-driver).
  
  
• [WP]  'Typed' becomes the default model.
• [WP]  'Store' and 'Runtime' models abandoned.
• [WP]  Experimental float and machine-integer models.
• [WP]  New interface to model selection (unique -wp-model option).
• [WP]  New simplification engine (specific options).
• [WP]  Added support for string literals (-wp-literals).

Bug Fix

• [Makefile]  Fixed bug #1385 about ocamllex.opt.

Plugin E-ACSL

New Features

• [E-ACSL]  Use GMP arithmetics only when required (i.e. mostly never in practice).
  
  
• [E-ACSL]  Support of bitwise complementation.
• [E-ACSL]  Nicer generated variable names.
• [E-ACSL]  Continue to convert the other pre/post-conditions even if one fails.
• [E-ACSL]  Support of \base_addr.
• [E-ACSL]  Support of \offset.
• [E-ACSL]  Support of \block_length.
• [E-ACSL]  Support of \initialized.
• [E-ACSL]  Support of \valid.
• [E-ACSL]  Support of floats in annotations. Approximate reals by floats.
• [E-ACSL]  Prevent runtime errors in annotations, except uninitialized variables.
• [E-ACSL]  Support of \valid_read.
• [E-ACSL]  Support of ghost variables and statements.
• [E-ACSL]  Support of undefined function with a contract.
• [E-ACSL]  New option -e-acsl-valid. By default, valid annotation are not translated anymore.
• [runtime]  Function e_acsl_assert now consistent with standard assert.
• [runtime]  Improve ACSL spec of E-ACSL' C library.

Bug Fixes

• [E-ACSL]  Fix bug with conditional and GMP integers.
• [E-ACSL]  Fix bug with negation and GMP integers.
• [E-ACSL]  Fix bug with boolean.
• [E-ACSL]  Fix bug with lazy operators in term position.
• [E-ACSL]  Fix bug with very long ACSL integer constants.
• [E-ACSL]  Fix bug with complex term left-values.
• [E-ACSL]  Fix bug when translating a postcondition of a function where the init state is the same than the final state (bts #1300).
• [Makefile]  Fix compilation bug when configuring with --enable-external.

Frama-C General

New Features

• [Cil]  In debug mode, pretty-print numerical constants instead of displaying the source file strings.
• [Cil]  Functions returning a value cannot let control flow falling through the closing '}' Fixes #685.
• [Cil]  New option -warn-undeclared-callee for calls to functions that have not been previously declared.
• [Journal]  Better journalisation of command line options setting a list of arguments (e.g. -slevel-function): avoid quadratic complexity in the generated code (fixed bts #1123).
• [Kernel]  Adding supports for clause allocates and frees and their version for loops.
• [Kernel]  Sets generated assigns clauses into the default behavior.
• [Kernel]  Adding some more supports for built-in related to memory blocks.
• [Kernel]  Support for model fields
• [Kernel]  Keep all prototypes with a spec, even if not referenced.
• [Kernel]  New option -<plugin>-share for plug-ins to customize their specific share directories.
• [Kernel]  Use Zarith whenever possible (bts #983).
• [Kernel]  when printing help, display the name of the opposite boolean option (bts #1085).
• [Kernel]  Consolidation from call-site preconditions to original precondition now handle calls through function pointers
• [Kernel]  improve 'reachable' properties.
• [Kernel]  New option -keep-unused-specified-functions.
• [Kernel]  A negative value given to -ulevel option hides all UNROLL_LOOP pragmas.
• [Kernel]  linker checks that the ghost status of two merged declaration is the same, and raises an error otherwise.
• [Kernel]  C constant expressions are now allowed as UNROLL level into loop pragmas.
• [Kernel]  The annotation 'loop pragma UNROLL "completly", n;' unroll 'n' times the annoted loop and then add it a clause 'loop invariant \false;'. The remaining loop should be death code.
• [Kernel]  All globals with attribute FC_BUILTIN are preserved even if unused.
• [Kernel]  Remove useless negative options -no-help, -no-version, -no-print-share-path, -no-print-lib-path and -no-print-plugin-path.
• [Logic]  Better label inference in axiomatics (see bts #1068).
• [Logic]  LoopEntry and LoopCurrent built-in labels.
• [Logic]  Cleaner generated assertions in presence of multiple pointer casts.
• [Logic]  Better error messages when parsing logic.
• [Project]  Accept to load inconsistent project by setting to default the inconsistent states and their dependencies.

Bug Fixes

• [Cil]  Fail when encountering a lvalue of type void (#1013).
• [Cil]  Go to new line more often when printing sequence of statements. Fixes issues #1021.
• [Cil]  Correct sharing bug on widening pragmas. Fixes #1090.
• [Cil]  Improve label positions in presence of loop unrolling (bug #1100).
• [Cil]  Preserve typedefs on global variables with an initializer
• [Cil]  Better propagatation of volatile, const and restrict type qualifiers through typedefs on arrays
• [Journal]  Fixed bug #1080: better generated journal in case of missing internal data preventing it of being runable.
• [Journal]  Fixed bts #932 about journalization of dynamic plug-ins in some corner cases.
• [Kernel]  Better linking behavior (fixes #672).
• [Kernel]  Link error aborts Frama-C (fixes #990).
• [Kernel]  empty list in complete/disjoint is expanded by logic type-checker to the list of behavior name of current contract. Fixes issue #1006. See bts comments for the differences that can appear in the treatment of specs.
• [Kernel]  keep track of local variables even in presence of annotation + do not silently lose statement contract. Fixes issue #1009.
• [Kernel]  Fixed bug about property statuses and setting parameters after -load (statuses were not cleared when required).
• [Kernel]  Initialization of locals is correct for all sizes; uses bzero to 0 + contract (directly validated by Kernel)
• [Kernel]  Fixed bug #1135 and bug #1139 about loop unrolling.
• [Kernel]  Fixes issue in loop unrolling and annotations.
• [Kernel]  Strict checking of type compatibility when merging an already called prototype without arg list and a full prototype (fixes issue #728, #109).
• [Kernel]  Introduce more temporaries for a call [lv = f()] if the return type of f and the type of lv do not match. Fix issue #1024.
• [Kernel]  Fixed bug with Type.pp_ml_name for generic sets which can lead to incorrect journal generation (bts #1127).
• [Kernel]  Fix graph of consolidation statuses when several properties get the same name.
• [Kernel]  Fixes bug #840 (inaccurate position in presence of -pp-annot).
• [Kernel]  Fixed bug with save/load: loading a file <f>, then quitting Frama-C can no longer modify <f> (bts #1269).
• [Kernel]  Fixed #1267 (adds explicit casts for default argument promotions).
• [Kernel]  Do not accept spurious '}'. Fixes bts #1273.
• [Kernel]  Fixed missing undefined behavior for multiple write accesses (fixes bts #1059).
• [Kernel]  Fine tuning AST dependencies. See developer guide.
• [Kernel]  Identical messages emitted in two different projects will now be visible in both projects. Fix bug #1104.
• [Logic]  Fixes issue #1005 (earlier detection of duplicated axiom name avoids Kernel.fatal).
• [Logic]  Fixes sizeof("string_literal") in logic.
• [Logic]  Fixed bts #1253: IndexPI and PlusPI are equivalent.

Developers Only

• [Cil]  Add method pFile in printers. Signature change for Cil.d_file (but you should use !Ast_printer.d_file).
• [Cil]  Fixed off-by-one error in foldLeftCompound ~implicit:true.
• [Cil]  Ast changed: Unrool_level renamed into Unroll_specs and its argument becomes a list for next evolutions.
• [Cil]  Fixed bts #1254: incorrect documentation of Cil.d_plaininit.
• [Cil]  Remove type Cil_type.typeSig. Use the functions in Cil_datatype.Typ and Cil_datatype.Logic_typ to compare types.
• [Cil]  Split constants of logic and C (fixes bts #745).
• [Kernel]  Logic_preprocess.file takes an additional parameter, as gcc pre-processor treats differently .c and .cxx files, and this must be reflected in annotation pre-processing.
• [Kernel]  Plugin.Register defines a new option -plugin-debug-category that allows to enable debugging for sub-categories of messages (See Log.set_debug_keys for more info).
• [Kernel]  New File.init_from_project function.
• [Kernel]  Added Property.location function.
• [Kernel]  Kernel.CppExtraArgs now gets type Plugin.String_list and not Plugin.String_set (fixed bts #1132).
• [Kernel]  Plugin.set_optional_help is now deprecated.
• [Kernel]  Fix implementation of Datatype.Triple and Datatype.Quadruple (bts #1133).
• [Kernel]  Kernel.Functions.get does not silently create a kernel function if it does not already exist. This behavior is kept for Cil builtins.
• [Kernel]  New API for Annotations which merges old Annotations, Globals.Annotations and operations of Kernel_function over function contracts.
• [Kernel]  Remove module Inthash. Use Datatype.Int.Hashtbl instead, or directly carbon2nitrogen.sh migration script.
• [Kernel]  Correct (albeit slow) hash function for terms and term lvalues.
• [Kernel]  Hook for handling for loop components in Cabs.
• [Kernel]  -check verifies if vdefined flag is coherent with status of variable in Globals tables and AST. Fixes one of the issues of #1241.
• [Kernel]  Add function [stmt_can_reach] to the arguments of Dataflow.Backwards, which is used to speed up the analysis. See dataflow.mli for good possible values.
• [Kernel]  Changes in interface of StringHashtbl options.
• [Kernel]  API of dynamic plug-ins is now documented as well as static plug-ins (fixed bts #171).
• [Kernel]  Operations that silently mutate AST should now call Ast.mark_as_changed to clear states depending on it (fixes #1244).
• [Kernel]  Fixed bts #1250: setting formals of visited function is not delayed until fill_global_tables anymore.
• [Kernel]  Remove obsolete constructors Cabs.TRANSFORMER and Cabs.EXPRTRANSFORMER and related parsing rules.
• [Kernel]  Datatype with structural comparison for exp and lval fixes bts #1263.
• [Kernel]  Correct hash function for Sets created by Datatype.Make_with_collections or Datatype.With_collections.
• [Kernel]  Improve signature of State_builder.Set_ref.
• [Makefile]  Fixed bug #1082 about wrong link in generated code documentation.
• [Makefile]  'make doc' did not work when GUI disabled (bts #1014).
• [Makefile]  Fix bug #1145 about PLUGIN_LINK_GUI_OFLAGS.
• [Makefile]  Use ocamldoc.opt whenever possible.
• [Makefile]  plugin is distributed iff PLUGIN_DISTRIBUTED and PLUGIN_ENABLE are not 'no' (instead of PLUGIN_DISTRIBUTED == yes).
• [Makefile]  Added variables PTESTS_OPTS and PLUGIN_PTESTS_OPTS to pass options to ptests through make tests. See dev manual.

Frama-C GUI

• [Gui]  Display global annotations in the filetree.
• [Gui]  Add filters for properties' consolidated statuses.
• [Gui]  Removing 'add assert before' from contextual menu. Uses ACSL_Importer plugin for such a feature.
• [Gui]  Display all properties in 'Properties' panel, including generated ones without location.
• [Gui]  Fixed bugs when the consolidation graph cannot be displayed (fixed bts #1122).

Plugin Aorai

• Aorai gets a real Dataflow analysis for contract generation + various logic simplifications.

Plugin From

• Better precision for code of the form 'if (c) stop(); else y = x+1;', where stop does not terminate
• More sharing between identical values when printing results.
• Major precision improvements when evaluating library functions whose assigns contains ranges.
• The interpretation of explicit assigns clauses for library function "assigns *p \from x;" was wrong: every possible location was assumed to have been overwritten.

Plugin Impact

• Complete rewrite. Improved precision and computation time. Fixes wishes #5 and #6.

Plugin Inout

• Major precision improvements when evaluating library functions whose assigns contains ranges.
• Option -inout-callwise to compute callsite-wise operational inputs. Improves precision of -inout, of the "Modifies" clause in the gui, and of the slicing.
• Operational inputs are now more precise for function with only an ACSL prototype.
• Better precision for 'if' in which only a side is reachable.
• Option -inout-callwise restarts Value when it is newly set

Plugin Metrics

• Fixes count of pointer accesses.

Plugin Occurrence

• Results can be filtered to display only occurrences in read or write positions.
• Fix bug where some occurrences were silently ignored in big asts; improve performance.

Plugin Pdg

• Improve precision in presence of provably dead code branches. Fixes issue #1194.
• Rename option -dot-pdg into -pdg-dot
• Improve performance, typically on arrays of structs.
• Option -pdg did nothing if -pdg-print was not set.

Plugin Report

• Display unreachable properties in a special way; identify unreachable statement more clearly.

Plugin Rte

New Features

• Emit \valid_read alarms instead of \valid for read accesses.
• Reuse behaviors names when -rte-precond is used on fonctions with multiple behaviors.
• Generate simpler assertions for accesses to arrays, and discard trivial ones; improve ordering of assertions. Honor option -unsafe-arrays.
• Rename option -rte-const into -rte-no-trivial-annotations (set by default).

Bug Fix

• Prevent generation of incorrect alarms on statements whose order of execution is not completely specified.

Plugin Scope

• Improved computation of defs. Statements are categorized between direct and indirect accesses.
• Improve precision of Defs computation (wish #1079).

Plugin Slicing

• No more blank between -slicing-project-name and -slicing-exported-project-postfix (from #1249 entry).
• More precise slicing when -calldeps is used (fixes wish #107).

Plugin Syntactic_callgraph

• Fix bug #989 about difference of display between GUI and dot output.
• Fix tricky bug while computing services when a cycle depends on another cycle (most part of the fix is actually in OcamlGraph itself).

Plugin Value

New Features

• Improve evaluation of logic when option -val-signed-overflow-alarms is active.
• Improve interpretation of ACSL annotations in presence of typedefs.
• Evaluate more precisely statements of the form if (*p == 1) {...} when *p is reused within the if block. This also improves the handling of switches.
• New option -no-val-left-shift-negative-alarms to treat left shift of negative integers as defined.
• Better evaluation of \initialized predicate when only some parts of the location are initialized.
• New builtin Frama_C_assert. Take advantage of existing assertions with "#define assert Frama_C_assert".
• Suppressed confusing message "all target addresses were invalid. This path is assumed to be dead.".
• After emitted an alarm \initialized(lv), the value analysis tries to remember that lv is initialized. This suppresses redundant alarms that were emitted further on.
• Minor improvements related to single-precision floating-point handling.
• In index out-of-bounds alarms, do not generate 'assert 0 <= i' part when 'i' is always greater than 0.
• During evaluation, reduce indexes that are detected as out-of_bounds.
• Reduce more aggressively invalid pointers: { p->f1 = v1; p->f2 = v2 } will usually raise at most one alarm.
• FRAMA_C_MALLOC_INDIVIDUAL modelization now properly treats allocated blocks as uninitialized.
• Aesthetic fix: do not display {{ &NULL }} and {{ &"foo" + {2} }} but rather {{ NULL }} and {{ "foo" + {2} }}.
• Improve precision for code with pointer casts (fixes bug #1074).
• Assertions of the form \valid(p+i) and \valid(&p->f) are now used to reduce p whenever possible.
• Evaluation of \separated predicate
• New message for functions with only a specification. Changed old message for functions with neither code nor specification to "No code nor specification for function ...".
• Improved handling of *(p+i) (or equivalently p[i]) when p is a known pointer and i is unknown.
• Improved handling of conditions involving the conversion to int of a floating-point variable.
• Support for \valid_read predicate; evaluation of \at(p,Pre) and \initialized{Pre}(...).
• Errors during evaluation in the logic are now reported.
• Old "Evaluate expression" menu in the GUI replaced by "Evaluate ACSL term"; value of term lval is now displayed. Evaluations that may fail are flagged.
• Allow comparison of invalid pointers in the logic.
• New option -val-ilevel, to change the frontier between sets of integers and intervals.
• Add bzero builtin. A precise destination and size are required (wish #915).
• Position call-site statuses for function preconditions, instead of the previous global status.
• More thorough checks for calls through a function pointer: warn when the function type and the pointer are not compatible, and stop when they cannot be reconciled.
• Statutes 'Invalid' are now positioned on 'for behav:' assertions even when 'behav' is not the only active behavior.
• Assertions such as \valid(p) now evaluate to Invalid when p is not initialized or an escaping address.
• Warn when 'assigns *p' points to a completely invalid location.
• Clarified message about completely indeterminate memory.
• Print misaligned values in a simpler way. Fixes wish #1271.

Bug Fixes

• Fixed spurious alarm \valid(p) in *p = e; when e is completely invalid. Soundness was not affected (the alarm for whatever made e invalid was present).
  
  
• Fixed crash when a library function is called in a state where the function's precondition cannot be true.
• Improve warnings and evaluation in presence of possibly infinite floats (fixes #997).
• Generate correct assertions when using memcpy builtin. Fix #1000.
• Fixed #1001: do not warn for unsigned shifts, do not end propagation on signed left shift of an address.
• Prevent potentially incorrect assertions from being emitted when the result a call must be cast. Fixes #997 and #1024.
• Fixed soundness bugs involving lval = lval; assignments targeting literal strings and automatically created S_... memory zones.
• Fix wrong hash function, which could cause memory overuse and worse.
• Evaluate ACSL && and || when they appear as terms (fixes bug #1072).
• Allocate a finite space for malloc builtins; fixes some bugs when a pointer refers to a non-yet allocated space.
• Fix crashes and/or missing alarms when evaluating *p=(cast)f() with p invalid (bug #1097).
• Fix bug in evaluation of pointers to start of array.
• Fixed bug where user assertions accessing uninitialized variables got the wrong status.
• Handle 'assigns *p' where p has a typedef type
• Fix incorrect initialization of volatile fields or globals in presence of initializers (bts #1112).
• Fix possible typing bugs when evaluating logic expressions with non-integral types (bts #1175).
• Re-emit alarms when Value options are changed and an analysis is restarted.
• Better time and space complexity for initialization of big arrays in -lib-entry mode (bts #1026).
• In lib-entry mode, honor 'const' attributes that appear deep inside the type (bts #759).
• Calls (*p)() where p resolves to both valid functions and invalid addresses are now properly handled.
• Fix crash when an undeclared function returned a pointer to a function that was later called.
• Fix crash when evaluating *((int*)0+x)=v when the NULL base is invalid.

Developers Only

• shift_left and shift_right functions now take an optional signedness boolean in addition to the optional size.
• Moved contents of memory_state/Abstract_value into ai/Lattice_Interval_Set. Use bin/nitrogen2oxygen for automatic migration.
• Lmap.paste_offsetmap now handles imprecise destinations.
• Fix option -absolute-valid-range being reset by project copies.
• Made type Ival.tt private.
• Rename Db.Value.assigns_to_zone_inputs_state to Db.Value.assigns_inputs_to_zone. Add new functions Db.Value.assigns_outputs_to_zone and Db.Value.assigns_inputs_to_locations.
• Signature change for function Db.Value.register_builtin: builtins can now return multiple states.

Plugin WP

New Features

• [Cmd]  Extended support for external libraries: Options -wp-coq-lib, -wp-why-lib and now -wp-alt-ergo-lib.
  
  
• [Cmd]  Extended selection language: -wp-prop [+|-][@]id to add or remove property category or name.
• [GUI]  Graphical version of Alt-Ergo (altgr-ergo) can be launched from the 'Proof Obligation Panel'.
• [WP]  Limited support for triggers in axioms and lemmas.
• [WP]  Better elimination of let constructs for -wp-norm Eqs option.
• [WP]  Enhanced statistics for -wp-report (see manual).
• [WP]  Truncating too long log filenames.
• [WP]  Experimental simplifier with new 'Typed' model (see manual).

Bug Fixes

• [Coq]  Better translation in Coq for floats and reals (fixed bugs #1174 and #1176).
• [WP]  Fixed issue about -ulevel option (bug #1244).

Developers Only

• [WP]  Enhanced Ocaml API (see manual). Old bindings are preserved, but now emit a deprecated warning.

Frama-C General

New Features

• [Cil]  Enumerated constants are kept in the AST.
• [Cil]  Implement precise dataflow on switch constructs. As side effect, improve precision of value analysis.
• [Cil]  Fixed #720 (incorrect simplification of switch).
• [Cil]  Support for &"constant_string" in parser.
• [Cil]  Normalization of lval: T+1 ==> &T[1] when T is in fact an array (implies *(T+1) ==> T[1])
• [Cil]  Pretty-printing lval and term_lval the same way
• [Cil]  Cache results of offsets computations.
• [Cil]  Add support for GCC specific cast from field of union to union
• [Kernel]  Exit status on unknown error is now 125. 127 and 126 are reserved for the shell by POSIX.
• [Kernel]  Better error message when plug-in crashes on loading (bts #737).
• [Kernel]  Big integers can now be displayed using hexadecimal notation.
• [Kernel]  \at(p,Old) is pretty-printed as \old(p).
• [Kernel]  Some messages may be printed several time for the same line if they refer to different columns.
• [Kernel]  Better handling of comments with -keep-comments and new API. See Cabshelper.Comments and Globals.get_comments_*
• [Kernel]  Better pretty printing of lists of any elements
• [Kernel]  Current pragmas no longer give rise to code annotations (as they do not contain anything that can be proven).
• [Kernel]  Improve space complexity of function stmt_can_reach.
• [Kernel]  New kind of command-line parameter, for commands that do heavy output. Used for Value, Pdg and Metrics.
• [Logic]  Added support for bitwise operators --> and <--> into ACSL formula.

Bug Fixes

• [Cil]  Fixed bug #725 (type-checking && operator).
• [Cil]  Fix bugs #780 and #791: use ids unique between projects for varinfos, statements and expressions.
• [Cil]  Fix bug #785: promotion between long long and an unsigned same-sized type.
• [Cil]  Fixes wrong precedence of not in predicate when pretty-printing.
• [Cil]  Fixes bug #771 (spurious warning for read/write accesses in undefined order).
• [Cil]  Fixes bug #832 (spurious warning for read/write accesses in undefined order)
• [Cil]  Fixes bug #857 (problem with some C enum value and Ocaml 32 bits 3.11.0).
• [Cil]  Correct obscure Cil bug linked to the removal of trivial unspecified sequences or blocks. Fixes bug #882.
• [Cil]  Fix conversion bug for f(i++) or f(++i) when i has size less than int, and f expects an int (bug #911).
• [Cil]  Fix merging bug (#948).
• [Cil]  Correctly handle casts in switch. Fixes #961.
• [Configure]  Fix bug #262: --disable-plugin works for external plugins compiled from within Frama-C kernel.
• [Kernel]  Bug fixed in pretty printer. (incorrect precedences leading to missing parenthesis).
• [Kernel]  Bug fixed in File.create_project_from_visitor potentially impacted programs transformation.
• [Kernel]  Fixed bug #775. Large octal and hexadecimal constants are now correctly typed.
• [Kernel]  Fixed bug #770 and #769, part 1. Fixed typo in anonFieldName (was annonFieldName).
• [Kernel]  Fix bug #769: merging issue for declared struct.
• [Kernel]  Fix 'make clean' of plug-ins.
• [Kernel]  Support for GCC packed and aligned attributes and for GCC pack pragmas. Fixes #719.
• [Kernel]  Fixed typing of bitfields whose size is equal to the size of int (bugs #823, #817).
• [Kernel]  Support GCC like typing of enums.
• [Kernel]  Fixed macros in limit.h.
• [Kernel]  Correct syntactic loop unrolling in presence of switch. Fixes bug #861.
• [Kernel]  Add parameter ~declarations to Globals.FileIndex.get_functions. Prevent duplication bug in properties navigator of the GUI.
• [Kernel]  Fixes visitor bug + properly refresh ids of properties in code transformation (in particular loop unrolling).
• [Kernel]  Fixes various performance issues when parsing very large functions. Fixes #965.
• [Kernel]  New exception for Ast.UntypedFiles.get when no untyped AST is available. Fixes #954.
• [Kernel]  Treat long bitfields the same way as gcc and clang. Fixes #959.
• [Kernel]  Do not normalize Pre in Old, especially where Old is not allowed.
• [Kernel]  Warn when the plug-in specified by -load-module or -load-script is not found (used to remain silent)
• [Logic]  Fixed bug #714 about lexing ACSL characters and strings.
• [Logic]  Fixed bug #744 (comparison between arithmetic types is done in the smallest possible type).
• [Logic]  \at(t,L) when t is a C array is now a logic array whose content is the one of t at L, not the address of the first element of t (which stays the same between L and Here anyway). partial fix of bug #761.
• [Logic]  Fix bug #501: volatile clauses are handled by the kernel.
• [Logic]  Fix bug #761: adding \old in ensures clause for parameters does not capture terms in associated offset.
• [Logic]  Fixed issue with -pp-annot (fix bug #691 and #812).
• [Logic]  Fixed overloading resolution (fixes bug #655).
• [Logic]  can have a local binding for a predicate (even a constant one) without spurious warnings from typechecker. (fixes #848)
• [Logic]  Normalization of assigns clause: \result and \exit_status only appear if a \from is specified. Fixes #557, #845
• [Logic]  Fixed issue #866 (merging specs included twice)
• [Logic]  Fixes bug #887 (merging logic constants).
• [Logic]  Fixes bug #885 (wrong insertion of cast).
• [Logic]  Fix bug #501: volatile clauses relative to partially volatile lvalues are handled by the kernel.
• [Project]  Fix sharing bug when copying project.

Developers Only

• [Cil] /Logic New functions Clexer.is_c_keyword and Logic_lexer.is_acsl_keyword.
• [Cil]  AST changed: 'a before_after type is deleted. All annotations are now attached before.
• [Cil]  AST changed: removing Told and Pold constructs.
• [Cil]  Remove incorrect Cil_const.Build_Counter; use State_builder.SharedCounter instead.
• [Cil]  Various smart constructors and ast helper functions.
• [Cil]  Support for large constants in programs. My_bigint is now used instead of Int64.t in the AST. Fixes #858.
• [Cil]  Improve performances of Cil_datatype.Typ.{compare, equal, hash}.
• [Cil]  Removing types about validity status from the AST. Use module Property_status instead.
• [Kernel]  module Service_graph: function entry_point in input and output of functor Make now returns an option type.
• [Kernel]  Bts #729: calling function Plugin.is_visible (resp. Plugin.is_invisible) forces to display (resp. prevents from displaying) the corresponding parameters in an help message.
• [Kernel]  Extlib.temp_file_cleanup_at_exit and Extlib.temp_dir_cleanup_at_exit may now raise exception Temp_file_error. They may raise an unspecified exception before.
• [Kernel]  Change semantics of ChangeDoChildrenPost for vstmt_aux. See developer's manual for more precision.
• [Kernel]  Fixed bug #727 (visiting a GFun spec in frama-c visitor was not done in the appropriate context).
• [Kernel]  New function File.create_rebuilt_project_from_visitor
• [Kernel]  Remove several kernel functions: Ast_info.pretty_vname: use Cil_datatype.Varinfo.pretty_vname Cil.print_utf8: use module Parameters.UseUnicode- Clexer.keep_comment: use module Parameters.PrintComments Cabshelper.continue_annot_error_set: Cabshelper.continue_annot_error_set: use Parameters.ContinueOnAnnotError.off all Cil, Cilmsg and CilE functions for pretty printing: use Kernel ones instead.
• [Kernel]  Following items are now deprecated: function Kernel_function.pretty_name: use Kernel_function.pretty module UseUnicode: use module Unicode.
• [Kernel]  Makefile.plugin and .dynamic more robust wrt external plugins (can make doc clean depend more easily; fixes bug #754, improves bug #742).
• [Kernel]  get rid of bin/sed_inplace (use ISED from share/Makefile.common where needed, which was the recommended way from the beginning).
• [Kernel]  Alternative signature for dataflow initial state. A few IntHash replaced by Stmt.Hashtbl.
• [Kernel]  Removed type Log.source. From now on all locations have type Lexing.position.
• [Kernel]  Fix bug #790: AST integrity checker issue.
• [Kernel]  Remove Db_types module. All types are now in Cil_types. Moved type Alarms.t to Cil_types.alarm.
• [Kernel]  Kernel now accepts declarations as main entry point.
• [Kernel]  Kernel_function.find_return may now raise exception Kernel_function.No_Statement.
• [Kernel]  Module Parameters is dead. Each module corresponding to a parameters is moved to Kernel. Module Parameters.Dynamic is now Dynamic.Parameter while Parameters.get_selection_context is now Plugin.get_selection_context. You can use the script bin/carbon2nitrogen to perform the translation (almost) automatically.
• [Kernel]  New function File.new_machdep in order to register a new machdep dynamically.
• [Kernel]  Cil_datatype.LogicLabel implemented
• [Kernel]  Structural_descr.pack is now a private type. Use smart constructors instead.
• [Kernel]  New function Dynamic.is_plugin_present.
• [Kernel]  Most types of module Property are now private. Use smart constructors instead.
• [Kernel]  Remove Kernel_datatype (merge with Cil_datatatype).
• [Kernel]  new function Kernel_function.set_spec which must be called whenever the spec of a kf is modified.
• [Kernel]  Remove function CilE.update_gotos.
• [Kernel]  New way for handling abstract type in the type library.
• [Kernel]  Fix dynamic access to function [is_default] of parameters.
• [Kernel]  Dynamic.load_module searches in plugin path as advertised in its documentation
• [Kernel]  Exporting Property_status.self state
• [Kernel]  Ensures that a unique kf is generated per function in each project, avoid using kf for project A in project B.
• [Kernel]  Modification of Log.print_on_console. No more based on Format.kfprintf to avoid deadlock when error are raised by plugin pretty printers.
• [Kernel]  Adding option ~dkey to Log.debug functions. See Log.Messages for details.
• [Kernel]  Properties_status is now called Property_status. Fully new interface.
• [Kernel]  Add IPLemma, IPNotacsl and IPConjunction as new constructors of Property.t; remove IPBehavior.
• [Kernel]  Annotations.replace and Globals.Annotations.replace_all are removed.
• [Kernel]  Signature of Plugin renamed for consistency. Use carbon2nitrogen for automatic translation.
• [Kernel]  Add Kernel.Unicode.without_unicode, which applies a function without upsetting the Unicode option in the gui.
• [Kernel]  Getters of Dynamic.Parameter now get an extra argument of type unit. May improve efficiency a lot.
• [Kernel]  Export datatype Varinfo.Hptset. Signature change in functor Abstract_interp.Make_Hashconsed_Lattice_Set.
• [Kernel]  Add parameter ~with_locals to Db.accept_base (prior this, ~with_locals was implicitly false)
• [Kernel]  Quadruple datatype.
• [Kernel]  Map_common_interface to have a merge function for Ocaml < 3.12.
• [Kernel]  Copy visitor creates new kf before visiting a function, allowing to use it for creating Property.t items in the new project during visit (fixes #942).
• [Logic]  Implementation of statement contracts for function behaviors.
• [Logic]  Add possibility to cast integer to C integral type when type-checking (Changes parameter of Logic_typing.Make)
• [Logic]  Fixes bug #751 (Cil.lconstant now returns terms of type integer and not int).
• [Makefile]  Add target to launch the tests of a specific dynamic internal plugin from Frama-C's main Makefile.
• [Ptests]  Ptests adds filename of current test before the options given to frama-c (see #736).

Frama-C GUI

New Features

• [Gui]  Hide empty plugins columns in the filetree. Add support for hiding globals entirely.
• [Gui]  Automatically show the main function at launch.
• [Gui]  Menu to configure what is displayed in the filetree.
• [Gui]  Add history for navigating source code.
• [Gui]  Support to display the state of the absolute memory.
• [Gui]  Double-clicking on a warning now displays the pretty-printed source location
• [Gui]  Improve labels under the icons of the toolbar. Smart constructors in Menu_manager now require a label and a tooltip.

Developers Only

• [Gui]  Signature change for Filetree#append_pixbuf_column.
• [Gui]  Signature change for Filetree#add_select_function, Filetree#select_global and Menu_manager.entry. Deprecate Design.apply_on_selected.
• [Gui]  Menu_manager now support check menus and toggle buttons

Plugin Aorai

New Features

• Deterministic automata.
• Automaton is handled by contract of leaf functions.

Bug Fixes

• State names used as enum constant are checked to be admissible fresh C identifiers.
• Fix issue in translation of guards + better error messages.
• Existing assigns are augmented with the locations corresponding to the instrumentation of the automaton.
• Generation of loop invariant for intermediate counter + fixes various issues

Developers Only

• Redefinition of internal structures before enabling Ya extensions for sequences

Plugin Dataflow

• Improve precision of backwards dataflow algorithm and of postdominators on 'if' with a missing branch

Plugin Dominators

• ,Postdominators No feedback by default. Use -dominators-verbose 2 or -postdominators-verbose 2 if you need it.

Plugin From

• Display results function by function, instead of as one big block (may lower memory consumption considerably).
• Fix #781: handling of function calls with an implicit cast for the assignment of the result.
• Display name of called function when displaying results of option -calldeps.
• Minor interface changes in From. Replace some meaningless kinstr by stmt, and make the callbacks lazy.

Plugin Impact

• Correct a journalisation bug in gui mode.
• Bug fixed when plug-in `Security_slicing' cannot be loaded or is incompatible with Impact.
• Bug fixed with '-impact-pragma f' on an unknown function f.

Plugin Inout

New Features

• Improved precision of the computation of operational inputs in presence of function calls.
• Improved messages in presence of recursive calls
• Correctness in presence of recursive calls. See issue #733.
• Operational inputs and outputs are now more precise for library functions: assigns clause are evaluated at each call.

Developers Only

• Db.InOutContext becomes Db.Operational_inputs.
• Interface change. Non_contextual renamed to Cumulative_analysis.

Plugin Metrics

• New command-line options to compute the functions potentially called from a given function, and the percentage of functions analyzed by the value analysis.
• Improves efficiency of metrics computation.

Plugin Occurrence

• Better pretty-printing: do not display internal ids anymore.
• Fixed bug when journalising.

Plugin Pdg

• Pdg can now be saved on disk.
• Improved time and space complexity on big functions.
• Better precision in the dependencies. Fix bug #787, #789 and #802 : infinite loops creation in slicing.
• Fix bug #787 but leads to less precise dependencies.

Plugin Postdominators

• Add Db.PostdominatorsValue: postdominators taking into account value analysis results

Plugin Rte

• No longer position 'Don't know' statuses
• Correct plug-in name for dynamically registered RTE functions.
• Option -rte-precond is not entailed by -rte-all anymore (precontion annotations must now be required explicitly).

Plugin Scope

• "Show Defs" is now an interprocedural analysis.

Plugin Security_slicing

• Fixed bug #768 about exception raised when analysing variadic functions. A warning is now emitted: the function is ignored by the analyzer, thus the result is potentially incorrect.

Plugin Semantic Constant

• Folding All options are prefixed by "scf". Use -scf-help for the details. Fixed #946. Compatibility is preserved thanks to option aliases.

Plugin Slicing

New Feature

• Option -slice-print is now deprecated: use instead <normal slicing command> -then-on 'Slicing export' -print

Bug Fixes

• Fixed bug #709: missing statements in sliced program.
• Fixed bug #774: journalisation works again.
• Fix bug #786: missing label in sliced program.
• Fix bug #799: missing label in sliced program.
• Fix incorrect simplification of single-statement block in presence of label.
• Use correct function during generation of sliced project. Fixes #950.

Plugin Syntactic Callgraph

• Fixed issue #723: syntactic callgraph does not require an entry point anymore. If no entry point, services are less precise yet.

Plugin Users

• Calls to this plug-in are now written in the journal.

Plugin Value

New Features

• Uniformized message displayed when no information is available for a function.
• Take Flush-To-Zero possibility into account for single-precision floats.
• Improved informative messages about addresses of locals escaping their scope.
• Improved option -subdivide-float-var when used without -all-rounding-modes. Improvement marginal for double computations and significant for float ones.
• Each precondition can get a specific validity status.
• Use hash-consed sets of statements, making many analyses faster and leaner for large functions or idioms that make functions large at normalization (e.g. large initialized local arrays).
• Improved results for operation % by zero. Removed message about binary operators raising exceptions.
• Option -val-after-results to control the recording of post-statement states. Active by default in the GUI.
• Alarms may pretty print the abstract value culprit for the potential violation. This is particularly informative for certain alarms.
• New option -no-val-show-progress
• More aggressive state reduction when emitting pointer_comparable assertions. Use option -undefined-pointer-comparison-propagate-all if you liked the old behavior better.
• Literal strings are now read-only.
• Emit \pointer_comparable alarm for unspecified. equality test between literal strings such as "foo" == "foo".
• New builtin Frama_C_dump_each_file, which dumps the entire memory state into successive files.
• Option -val-builtin: experimental support for builtins that can fail (by calling a fallback C function).
• More precise when an alarm is emitted in a loop.
• Postconditions containing \old are now handled.
• Uses "complete behaviors" information.
• Loop invariants are now used to improve analysis.
• Improve behavior in presence of errors during the computation of the initial state. Allow non ISO global initializers using the value of constant globals defined earlier.
• Improve handling of assigns in library functions.
• Remove non-relevant variables from the 'Modifies' clauses of the GUI.
• Wide strings more supported.
• Better message when interpretation stops for a function argument.
• Improved precision when using -all-rounding-modes.
• Improved precision of &.
• New informative message when not using. -val-signed-overflow-alarms "2's complement assumed for overflow"
• Raised cut-off limit between sets and intervals from 7 to 8 elements.
• Improved precision of if (x!=c) when the value set of x is an interval of 9 elements.
• New alarm, for programs that do not respect C99 6.5.16.1:3 (overlapping assignment from lvalue to lvalue). Partially supported (not emitted in some cases).
• New option -remove-redundant-alarms for removing redundant alarms. This was previously done by default. Use this option if you are going to inspect alarms emitted by Value.
• Do not continue evaluating successive 'requires' or 'ensures' clauses if one of them is false.
• New alarm for left shift of negative values. Minor other changes related to shift operation alarms.

Bug Fixes

• Changes related to 0., +0., -0., sort of thing. Unwarranted loss of precision fixed.
  
  
• Fixed representation of unknown single-precision floats in initial context (it used to be the same as for an unknown double).
• Fixed crash when passing invalid argument to function, found by John Regehr using random testing (jrrt).
• Fixed correctness bug involving nested structs (jrrt).
• Fixed forgotten warning when passing completely undefined lvalue as argument to function. (jrrt)
• Fixed bug when passing bitfield as argument to function. (jrrt)
• Fixed bug when passing struct as argument to function with a big-endian target architecture.
• Fixed bug #732: Synthetic results were partial when -slevel was set not high enough to unroll loops completely.
• Fixed correctness bug when bitfield initializer exceeds range (bug #721) (jrrt).
• Fixed crash with ACSL assertions involving floating-point variables (bug #752).
• Some floating-point alarms could be printed several times. Fixed.
• Fixed bug #689. Each postcondition can get a specific validity status.
• Correctly emit \pointer_comparable(...) alarms.
• Fix bug #798: calls to functions that return a value with latent conversion.
• Fixed crash for high values of -subdivide-float-var
• Fixed bug when bitfield receives the result of a function call (bug #819).
• Fixed undocumented builtin is_base_aligned.
• Remove some uneeded warnings when comparing function pointers with NULL. Fixes bug #855.
• Much more clever when interpreting logic terms, including those containing \old (eg. formals in postconditions)

Developers Only

• Minor interface changes in Value. Replace some meaningless kinstr by stmt, and make the callbacks lazy.
• Defunctorized Lattice_Interval_Set.
• Changed representation of bases for literal strings in preparation of related checks.
• Functions valid_* now take an argument ~for_writing Pass true when the lvalue being considered is used for writing in the program. Pass false when unsure.
• Add argument "exact" to Lmap.paste_offsetmap (which was preciously supposed to be always true).
• Module Cvalue_type renamed to Cvalue. Module Relations_type removed. Use Cvalue instead.
• Add some missing ~with_alarms arguments, notably to offsetmaps copy and paste.
• Signature change in CilE: plugins that want to emit Value analysis alarms must define their own emitters.
• Changed the representation of Ival.t. If an external plug-in matches "Ival.Set s", a simple fix is to add "let s = Ival.set_of_array s in" as first line of that case.

Plugin WP

• [Cmd]  Adding support for reporting with option: -wp-report.
• [Cmd]  Adding support for external proof libraries. See options -wp-include, -wp-tactic, -wp-coq-lib and -wp-why-lib.
• [Cmd]  Adding support for multi-provers in command line.
  
  
• [GUI]  Changes into Gui panel.

Plugin WP

New Features

• [Cmd]  New engine to compute proof obligations for arbitrary invariants. See option -wp-invariants.
• [Cmd]  Added option -wp-proof-trace to obtain more informations from provers when available (option 'Trace' in GUI).
• [Cmd]  Optimization of arguments passing by reference with option: -wp-byreference.
• [Ergo]  Alt-Ergo 0.93 now required.
• [Ergo]  Alt-Ergo is always used with builtin arrays. Removed option -wp-arrays.
• [GUI]  Removed 'Refresh' button from WP panel.
• [GUI]  Enhancement of Proof-Obligation panel.
• [GUI]  Default output directory is set to <home>-.frama-c-wp in Gui.
• [GUI]  New menu options to prove preconditions at one or all call sites.
• [GUI]  Feedback for proof of preconditions at call sites.
• [Hoare]  New Hoare model (now implemented on top of logic variables).
• [Vampire]  Support for Vampire as back-end prover.
• [WP]  No more logic generic pointers. Pointer arithmetics moved to memory models.
• [WP]  Better representation of records and unions in logic.
• [WP]  Alt-Ergo is now selected (and run) by default.
• [WP]  Handling partial initializers in C global variables.
• [WP]  Translation of axioms with labels (removed option -wp-axioms).
• [WP]  Print of formula change.
• [WP]  Optimization of arguments passing by reference.
• [WP]  Improvements of conversion between C-integers and Z-integers.
• [WP]  A warning is now emitted for missing assigns clauses.
• [WP]  Further improvement for proof of assigns clauses.

Bug Fixes

• [GUI]  Fixed bug #711 (cyclic dependencies).
  
  
• [GUI]  Fixed bug on PO status (wrong PO identification).
• [Store]  Better representation of pointers (issue #796).
• [WP]  Fixed problems with -wp-out <dir>.
• [WP]  In some cases, a proof attempt could silently failed. It is now properly reported.

Plugin E-ACSL

• [E-ACSL]  First public release.
  
  

Frama-C General

New Features

• [Configure]  Frama-C does not require Apron anymore (Why does for Jessie). Thus fix bug #647.
• [Kernel]  Improve performance on platform with dynami.c loading. Mainly impact value analysis (for developers: improve efficiency of Dynamic.get).
• [Kernel]  Handle errors better when they occur when exiting Frama-C. Slight semantic changes for exit code: - old code 5 is now 127; - code 5 is now: error raised when exiting Frama-C normally; - code 6: error raised when exiting Frama-C abnormally.
• [Logic]  Fix priority bug in parser.
• [Logic]  Mentioning a formal on the left-hand side of an assigns clause is now an error when type-checking logic annotations.
• [Makefile]  Fixed bug #638. By default, warnings are no more errors when compiling a public Frama-C distribution and plug-ins. SVN versions of Frama-C are still compiled with "-warn-error A".

Bug Fixes

• [Kernel]  Fixed #313. Entry point with a specification is no longer wiped out.
• [Kernel]  Fixed bug if an empty string is given on the command line while an option name is expected. There is now a proper error message.
• [Makefile]  Fixed bug #637: "make install -n" did wrongly create directories.
• [Makefile]  Fixed bug #660 related to a default Frama-C-compatible ocamlgraph installation under Cygwin (i.e. in a Win32 path containing the ':' character).

Developers Only

• [Cil]  Fixed bug #645. Ast_info.constant_expr, Cil.[zero,one,new_exp,makeZeroInit,mone,kinteger64_repr, kinteger64,kinteger,integer,constFoldBinOp,mkAddrOf, mkAddrOrStartOf,mkString,parseInt,sizeOf] no longer use an optional argument ?loc. It is now a non optional labeled argument. Previous default value of loc was ~loc:Cil_datatype.Location.unknown which is most of the time not accurate.
  
  
• [Kernel]  Remove API function Messages.enable_collect: please let the kernel do the job.
• [Kernel]  Remove Messages.disable_echo (can be done using Log module) and Messages.depend (can be done using Messages.self).
• [Kernel]  New function in API: Kernel_function.find_syntactic_callsites.
• [Kernel]  Fix bug #677. As a side-effect, function Plugin.add_alias is now deprecated and replaced by Plugin.add_aliases.
• [Kernel]  New syntactic context for memory accesses with user-supplied validity range.
• [Logic]  Refactoring of assigns and from AST representation and of Property.identified_property.

Frama-C GUI

New Features

• [Gui]  Gui options start by -gui and not -GUI
• [Gui]  Implement feature #635: display messages in the messages panel while loading a batch session in the GUI. The batch session must have been previously executed with the new option -collect-messages.
• [Gui]  Display more precise state after statement (http://blog.frama-c.com/index.php?post/2011/01/11/Seven-errors-game).

Bug Fixes

• [Gui]  Fixed 100% cpu load while external command are launched.
• [Gui]  Fixed bug #666. Do not display misleading "After statement".

Developers Only

• [Gui]  Added support for icons in Gtk_helper.Icon.

Plugin Inout

• Return statement dependencies were forgotten in operational input computations. Fixed.

Plugin Report

• Option -report no longer survive after -then.

Plugin Slicing

• Fixed bug #673.
• New options added for fixing bug #668.

Plugin Sparecode

• API modified for fixing #668.

Plugin Value

New Features

• Improved precision of | operator.
• New alarm for float -> int cast overflows.
• Added check that denormals work correctly on host computer (correction would be affected otherwise).
• Improved precision of & operator.
• Interpretation of ==> in ACSL annotations.
• Disabled incorrect interpretation of ACSL statement contracts.
• Improve performance of callbacks.
• Various minor speed improvements.
• More aggressive handling of if(x>e) where x has type double.
• Change in initial states generated by -lib-entry Much smaller. Perhaps more representative.
• Generate independent assertions for signed overflow and signed underflow. In many cases only one is generated (win!).
• Is is now possible to call Frama_C_show_each without ..._x.
• Changes in Frama_C_memcpy built-in. Still not perfect.

Bug Fixes

• Fixed obscure crash that could happen during very imprecise analyses.
• Fixed correctness bug involving pointers to signed integer pointing to memory locations containing unsigned integers or vice versa.

Developers Only

• New callback for recording the state after a statement.
• Renamed copy to copy_offsmap in Offsetmaps. The name "copy" clashed with Datatypes.

Plugin WP

• Plug-in WP removed from kernel-releases (now an independent plug-in).

Plugin WP

New Features

• [Cmd]  Clarification of -save/-then effect on WP
• [Cmd]  Options -wp-status-xxx to refine goal selection
• [Cmd]  Option -wp-warnings to display additional informations for 'Stronger' and 'Degenerated' goals.
• [Cmd]  Adding version in -wp-help.
• [Runtime]  Optimization of effect-assigns.
• [WP]  When -rte-precond is not used, wp generates a separate proof obligation for each call site.
• [WP]  New spliting algorithm. See option -wp-split. Option -wp-split-dim <n> to limit spliting up to 2**n sub-goals.

Bug Fixes

• [Coq]  Fixed bug #702 on Coq output with large integers.
• [Coq]  Fixed bug #740 for Coq on Windows. WP now uses directly coqtop -compile instead of coqc.
• [GUI]  Fixed incorrect property status refresh in the GUI.
• [Store]  Fixed bug #766 about offsets in assigns.
• [WP]  Proof of requires of the main entry point (bug #675).
  
  

Plugin WP

• Fixed bug #639: no more Coq compilation to shared directory.
• Accessibility of all provers from gui.
  
  

Plugin WP

• [Coq]  Fixed bug #639: no more compilation to shared directory.
• [GUI]  Accessibility of all provers from gui.
  
  

Frama-C General

New Features

• [Cil]  Be less aggressive during inline function merge. Alpha equivalent function are now kept separate.
• [Cil]  Clean up local variables handling and pretty-printing modified pBlock method interface (unified pBlock and pInnerBlock)
• [Cil]  Cil normalization takes care of abrupt clauses
• [Configure]  Better detection of native dynlink support.
• [Kernel]  Feature #484 about requires into named behaviors
• [Kernel]  Fixed bug #548: limit.h now syntactically correct. Architectures other than x86_32 still unsupported.

Bug Fixes

• [Cil]  Extended grammar of pragma lines.
• [Cil]  Fixed bugs #451 (break outside of loop/switch) and #452 (spurious 'body of f call falls through' warnings)
• [Cil]  Fixed bug #440 (remove spurious block generation at parsing time that clashed with label scoping rule in ACSL)
• [Cil]  Fixed #542 (now raises parse error when C function call dot not provide correct number of arguments)
• [Configure]  Fixed bug in configuration of external plug-ins
• [Configure]  get rid of known_plugins.ac (fix #462)
• [Configure]  Always configure OcamlGraph local version (if used) when configuring Frama-C.
• [Kernel]  Fixed bug in handling of -cpp-command
• [Kernel]  Tried to fix all permissions on *.{c,h} files
• [Kernel]  CL options for cabs2cil flags (fix #506)
• [Kernel]  Fixed #620 (default assigns generation).
• [Logic]  fix bug #454 (multiple labels in same statement)
• [Logic]  Fixed wrong precedence of <==>
• [Logic]  Checking for loop variant position
• [Logic]  Fix bug #498 (behaviors within same scope must now have unique names)
• [Logic]  ACSL identifiers starting with a \ are not replaced by pre-processing when a macro of the same name exists (fix #541)
• [Logic]  Better error messages for logic parser and other fix (fix #512, #538, #553, #560)
• [Logic]  Fixed #549 (Arrays in the logic)
• [Logic]  Fixed #570 (implicit conversion to void*) and fixes issue in overloading resolution
• [Logic]  Priority is used for pretty printing predicates.
• [Makefile]  Fixed potential generation of corrupted .o
• [Makefile]  Fix bug #460 when using a non-local ocamlgraph
• [Makefile]  Fix bug #461 when installing the GUI on a bytecode-only architecture
• [Makefile]  Fix bug #528 when building a dynamic plug-in in a sandbox.

Developers Only

• [Cil]  Remove deprecated annotation_status of AAssert in the AST
• [Cil]  Fix bug #489: constant literal present in original source are preserved in the AST. NB: this implies that they might be explicitly cast when an integer conversion occur.
• [Cil]  Support for custom extension in grammar of behaviors. See Logic_typing.register_behavior_extension.
• [Cil]  Preliminary support for function calls in UnspecifiedSequence
• [Cil]  Cil.makeLocalVar now inserts the variable into one of the function's local blocks.
• [Cil]  global_annotation has location information
• [Cil]  Removed function varinfo_from_vid. You can use maps or hashtables indexed by varinfos directly instead.
• [Cil]  Cil and Cabs expression have now a location.
• [Cil]  Changed ignored pure exp hook + hook for conditional evaluation of side-effects
• [Cil]  Extending logic label for plugin purpose.
• [Cil]  Changed type of doGuard in forward dataflow
• [Kernel]  Ptmap (resp. Ptset) is renamed into Hptmap (Hptset)
• [Kernel]  Fix bug #441 (keep track of original names in AST)
• [Kernel]  Deprecate Globals.Functions.find_englobing_kf. Use Kernel_function.find_englobing_kf which has a much better complexity instead.
• [Kernel]  Added field b_extended in behaviors to support grammar extensions
• [Kernel]  New implementation of module Properties_status
• [Kernel]  Major changes in the kernel. Mainly merge the old modules Datatype and Type into a single most powerful library called Type. The API of these libraries changes.
  
  Consequently, some other API changes. By side effect, a lot of functions of module Cilutil has been removed and replaced by their counterpart in module Cil_datatype.
  
  The script bin/boron2carbon.sh fixes most changes automatically. Feel free to use it to upgrade your plug-in.
  
  In the process, some minor bugs found and fixed in the Frama-C kernel.
• [Kernel]  File.check_file takes a new argument, allowing to describe which AST fails integrity check in case of trouble.
• [Kernel]  New Task module: a monadic library for calling asynchronous commands from the toplevel and the gui.
• [Kernel]  Remove function Globals.has_entry_point. Use Globals.entry_point instead.
• [Logic]  Parameterize search of field in logic typing functor in a similar way to search of other C symbols
• [Logic]  Fix bug #505 (Associate default label for predicates with a single label parameter and no argument)
• [Project]  Reimplementation of the project library (the contents of directory src/project). New API.
• [Ptests]  Slightly changed semantics of CMD and STDOPT. See developer manual for more info

Frama-C GUI

New Features

• [Gui]  Better graph display. Require ocamlgraph > 1.4
• [Gui]  First support for persistent GUI configuration. GtkPaned ratios, main and launcher window dimensions are saved to file frama-c-gui.config in the user's home directory.
• [Gui]  In expressions 't[v]', allow to select 't' (when it is a variable). To select the entire expression 't[v]', click on the ']' on the right.
• [Gui]  One tooltip by parameter in the launcher
• [Gui]  New graph viewer, requires ocamlgraph > 1.5

Bug Fixes

• [Gui]  Fix bug with toolbar button 'duplicate project'
• [Gui]  Fixed parsing of floats in frama-c-gui.config

Plugin From

• Improved interpretation of assigns clauses

Plugin Inout

New Features

• Improved precision of -inout with possibly invalid pointers.
• New option -inout-with-formals similar to -inout but without locals and with formals
• Improve option -inout-with-formals: cleanup local variables that come from out of call tree functions.
• Improved precision for option -inout-with-formals
• Clean local variables passed by address to callees from results of -input, -out, -deps
• Improve printing of -out -input -deps

Bug Fix

• Fixed bug in -inout where operational inputs of called library function were improperly inferred from assigns

Plugin Obfuscator

• Option -obfuscate is now part of a new dynamic plug-in `Obfuscator' (fixed issue #265). The behaviour of this option is now journalized and may be run by other plug-ins.

Plugin Occurrence

• Fix bug #550: crash when selecting an occurrence if the entry point set by "-main" is incorrect.

Plugin Security_slicing

• Only use the GUI; does not require it anymore

Plugin Slicing

• Fixed bug #448 about -keep-annotations option

Plugin Syntactic callgraph

• Fixed bug #587: proper error message when the entry point is invalid.

Plugin Value

New Features

• Optimization in the handling of library functions
• More optimization of library functions
• Yet more small improvements in value analysis of large programs.
• Variables now uninitialized by default. Improves -deps, -input, -output when addresses of local variables are passed as arguments of called functions.
• Tweak in -slevel* options. A little slower for some programs, much faster for others.
• More consistent naming scheme for generating shorter names when using -lib-entry. "star_" becomes "S_".
• Improved Frama_C_memcpy built-in.
• Improved precision of analysis for program short s[]= {0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1};main(){return((int*)s)[u()];}
• Structures passed as function arguments now precisely handled.
• Abort analysis when recursion is encountered.
• Clean local variables passed by address to callees from results of -val.
• Lowered memory consumption slightly.
• "assert(TODO)", used when a property to check in the analyzed code cannot be expressed as ACSL and the user should read the English explanation (e.g. "accessing uninitialized left-value") instead, could look unprofessional to the superficial onlooker. "assert(Ook)" will now be used instead.
• Do not emit alarm for uninitialized arguments to non-library functions. Necessary for structs. Relevant messages changed a little.
• Improved speed of options -slevel* for arguments in the thousands. Synthetizing results remains slow, so consider options -no-results* if you take advantage of them.
• Emit alarm for uninitialized arguments to library functions.
• Preliminary support for interpreting C type float as IEEE 754 single-precision.
• New option named -undefined-pointer-comparison-propagate-all
• Removed undocumented option -float-digits
• New option -float-normal (undocumented)

Bug Fixes

• Fixed bug with extern variables of incomplete type
• Fixed correctness bug involving the comparison of a variable of type float or double.
• Do not emit an alarm for the comparison of function addresses to NULL.
• Some "Misaligned" imprecision origins were wrongly classified as "Arithmetic". Fixed.
• Fixed bug involving typedefs when using option -val-signed-overflow-alarms.
• Fixed performance bug that could lead to "stack overflow" error during large analyses.
• Fixed memory leak.
• Disappearance of non termination messages from the log. The messages were inconsistent.
• Emit alarm for overflowing floating-point constants instead of crashing.
• Emit proper ACSL alarm for overflowing floating-point binary and unary operators. Fixed #259.
• Do not evaluate annotations right after propagation is stopped.
• Fixed bug that could happen in programs casting address of floating-point type to address of integer type

Developers Only

• There was one too many function called "find_ival". One was renamed to "project_ival".
• Function Cvalue_type.V.is_top rebaptized is_imprecise
• Renamed Int.eq into Int.equal. Removed Int.neq

Plugin WP

• [WP]  New WP plugin.
  
  

Frama-C General

New Features

• [Cil]  Extend logic pretty printer to handle all specific clauses
• [Configure]  Dynamic plug-ins are now statically linked by default whenever native dynlink is not usable (bts #301).
• [Configure]  Compiling the GUI now requires LablGnomeCanvas.
• [Kernel]  Add status for all clauses
• [Kernel]  Clarification of the multiple accesses warning. Becomes "undefined multiple accesses in expression".
• [Kernel]  Better error messages when a dynamic plug-in cannot be loaded.
• [Kernel]  Better -*-help.
• [Kernel]  New option -no-dynlink in order to prevent loading of dynamic plug-ins.
• [Kernel]  The journal is generated only if the GUI is crashing, or if the option -journal-enable is explicitly set (fixed issue #330).
• [Kernel]  Backtrace when Frama-C is crashing (only if Frama-C is compiled with caml >= 3.11.0)
• [Kernel]  New option "-plugin-h" as an alias for option "-plugin-help"
• [Kernel]  Preliminary standard C library in $FRAMAC_SHARE/libc
• [Logic]  Better error message when using = in annotations
• [Logic]  ordering of clauses in contracts
• [Logic]  If a C typedef integer, real or boolean exists, it takes precedence over corresponding logic type. The logic type remains accessible through its utf-8 denomination.
• [Logic]  Support for type abbreviation in logic
• [Logic]  Support for "reads \nothing"
• [Logic]  Adding "\pi" as built-in symbol

Bug Fixes

• [Cil]  Bug fixed with incompatible declarations of C functions
• [Cil]  Fix crash in parser when double definition of variable in two different files, in some order (fixed bug #213)
• [Configure]  Fixed bug with -help.
• [Kernel]  -kernel-debug and -kernel-verbose did not work as expected (bts #343).
• [Kernel]  -load-script did not clean up compiled files after exiting (fixed bug #371)
• [Logic]  Support for abrupt clauses; Modifies AST
• [Logic]  Fixed bug #272 (complete behaviors wo name)
• [Logic]  Fixed bug #228, #327 (syntax garbage at end of contracts)
• [Logic]  More utf-8 identifier accepted (fixes bug #366)
• [Logic]  Default label is "Old" inside \old(...)
• [Logic]  complete/disjoint behaviors do not accept undefined behaviors anymore (fixed bug #364)
• [Logic]  Full support for \let (fixed bug #344)
• [Logic]  Arrays and pointers are distinct in the logic, as per ACSL reference. Fixes bug #396
• [Makefile]  Fixed bug #305: make did not terminate when all plug-ins were disabled.
• [Makefile]  Fixed bug #310: improve robustness against new ocaml warnings.
• [Makefile]  Some GUI library files was not installed
• [Makefile]  Fixed 'make clean' in plug-in directory (bug #407)
• [Makefile]  Fix bug for generating .o files through recursive calls to Make in quiet mode (VERBOSEMAKE unset)

Developers Only

• [Cil]  pAssigns now prints directly a whole list of assigns
• [Cil]  New hook after Cabs elaboration (fix bug #446)
• [Configure]  Improved dependencies handling (fix #54)
• [Kernel]  Add unique id for elements in Db.Properties.Status tables.
• [Kernel]  Function Db.Properties.predicate_on_stmt and Db.Properties.get_user_assert does not exist anymore.
• [Kernel]  Module Db.Properties.Status replaced by module Properties_status.
• [Kernel]  Extlib now contains various functions to replace Sys.command but with portability and efficiency in mind.
• [Kernel]  Use of global logic constants is now a TLval (TVar _,TNoOffset) instead of TApp(_,[])
• [Kernel]  Support for dynamic uses of StringSet parameters
• [Kernel]  New implementation of save/load with small changes in the project API. Loading is now rid of its previous allocation peak and faster.
• [Kernel]  Type.register is more robust but gets a modified interface (fixed issue #276)
• [Kernel]  Major changes in API of module Annotations: add possible dependencies from/to a single annotation of a statement
• [Kernel]  Log.protect is replaced by Cmdline.protect
• [Kernel]  Kernel_function.Set now implemented with Patricia.
• [Kernel]  Type changes in Db.Properties.Interp. Use ~result:None to get your plug-in to compile again.
• [Kernel]  Dynamic.register and Dynamic.get are more robust, but take an extra parameter
• [Kernel]  Slight modification of Hook API
• [Project]  Project.register_todo_on_clear is deprecated and replaced by Project.register_todo_before_clear

Frama-C GUI

New Features

• [Gui]  Assigns clauses are now localizable in GUI
• [Gui]  Extend type Pretty_source.localizable
• [Gui]  Options *-verbose, *-debug and -quiet are now settable via the launcher dialog box (bts #317).
• [Gui]  New shortcut buttons.
• [Gui]  Now possible to delete the current project.
• [Gui]  Drop gtksourceview 1.x dependency and replace it with gtksourceview 2.x.
• [Gui]  View property status in GUI. Fixed a bug on reset with strange reactive zones in default buffer.
• [Gui]  Now possible to save/load a single project (fixed issue #9)
• [Gui]  Plug-in panels can be detached with drag and drop.
• [Gui]  New menu entries for loading ocaml scripts and ocaml object files (fixed issue #318)
• [Gui]  Add a menu entry for setting C source files of the current project

Bug Fixes

• [Gui]  Instantaneous actions are no longer cancelable but are as fast as possible now.
• [Gui]  Fixed bug while choosing 'New project' if -cpp-command is set (fixed bug #374)

Developers Only

• [Gui]  Methods protect and full_protect of main_window_extension_points now have an additional arguments.
• [Gui]  New implementation for the menubar and the toolbar. API fully changed for adding an item in these bars.

Plugin Impact

• In the GUI filetree, for each function, a bullet shows if some statements are highlighted

Plugin Inout

• -out and -out-external now obey -inout-verbose option Generated logs re-ordered a little.

Plugin Security

• No more distributed.

Plugin Security_slicing

• New experimental and quite undocumented plug-in. Sub-part of the old plug-in security. Only usable through the GUI.

Plugin Slicing

• Assigns clauses was missing from the sliced program (fixed bug #393)

Plugin Syntactic_callgraph

• Big speedup for showing the callgraph in the GUI. Require ocamlgraph >= 1.4.
• Fixed bug in services computation.

Plugin Value

New Features

• Improved treatment of "assigns p[..]" clauses in -input
  
  
• Handling of behavior-specific assertions now correct (albeit imprecise).
• New option -all-rounding-modes (floating-point) New dependency on C99 functions to control the FPU.
• Improved precision of floating-point operations
• Take into account all known flush-to-zero floating-point variants. No option seems necessary for now.
• Preliminary support of post-conditions for library functions.
• New display option -float-relative
• Clarified progress messages
• Improved precision when loop index has type char or short. Fixes bug #325
• Interpreting post-conditions about \result in contracts for functions that have implementations.
• New option -slevel-function f:n for fine-tuning semantic unrolling.
• Suppressed undocumented option -klr
• New options -no-results and -no-results-function, improved replacements for undocumented option -klr
• Experimental new option -subdivide-float-var
• Experimental new option -val-signed-overflow-alarms

Bug Fixes

• Synthetic validity status for assertions.
• Some "loss of precision" messages were duplicated and failed to be localized. Fixed.
• Fixed bug #372
• Fixed uncaught exception that could happen in analysis of programs with floating-point operations.

Developers Only

• Changed type of functions Db.Value.*_to_kernel_function. These functions now return a Kernel_function.Set.t. Use Kernel_function.Set.elements to transform this set into a list.

Frama-C General

New Features

• [Configure]  Detection of dot if required.
• [Journal]  Better handling of exceptions.
• [Kernel]  Slightly less false alarms with -warn-unspecified-order
• [Makefile]  Why is no longer a compilation dependency. It is required only at runtime for the experimental WP plugin.
• [Makefile]  Now possible to build custom binaries for plug-ins. Roughly these binaries are frama-c[.byte] + the plug-in statically-linked. The goal is called "static" in the plug-in's makefile.

Bug Fixes

• [Makefile]  Fixed compilation error occurring on a platform which does not support native dynlink and with ocaml >= 3.11 (bts #224).
  
  
• [Makefile]  Frama-C compiles even if ocamlopt is not available.
• [Makefile]  Fixed bug #236. Require ocamlgraph version > 1.2.
• [Project]  Fixed bug involving loading and options previously set while saving.

Developers Only

• [Cil]  Deprecated Cil.get_status. Use Db.Properties.Status.* instead.
• [Cil]  New pIdentifiedPredicate method in pretty-printer
• [Makefile]  Fixed bugs with the use of PLUGIN_EXTRA_BYTE and PLUGIN_EXTRA_OPT by plug-ins.

Frama-C GUI

• [Gui]  Elimination of repeated messages (bts #237).
• [Gui]  Release the terminal when the splash window is deleted.

Plugin Jessie

• Is no longer built within Frama-C. It becomes part of Why.

Plugin Obfuscator

• obfuscator does not lose links between logic and C variables anymore (bts #250). Obfuscator now gives a specific name to formal parameters.

Plugin Syntactic callgraph

• Improvement of the GUI of syntactic callgraph. Require ocamlgraph > 1.2.

Plugin Syntactic_callgraph

• Better implementation for computing the service graph: faster + correctly handle cycles.
• -cg-services-only is not relevant anymore.

Plugin Value

• Computed values not displayed on -load. Use -val-load to force display of computed values. Use -val -quiet to compute without printing results.
• Stopped displaying temporary variables introduced by normalization of source code, and block-local variables.
• Fixed display bug when logging the call stack introduced in Beryllium.
• Improved treatment of "assigns p[..]" clauses in value analysis. Other plug-ins (outputs,...) have not had the same improvement yet.

Frama-C General

New Features

• [Kernel]  New options -kernel-help, -kernel-verbose and -kernel-debug (bts #205).
• [Logic]  "reads" clauses on logic functions and predicates, which disappeared with the introduction of axiomatic blocks, have been ressurrected. Beware that the semantics is slightly different from before: see ACSL document for details. It is used to automatically generate footprint axioms.

Bug Fixes

• [Configure]  Fixed bug with --disable-gui in configure.in
  
  
• [Journal]  Fix generation of invalid variable name in journal
• [Kernel]  Restore compatibility with ocaml 3.10.2
• [Makefile]  Fixed bug with static linking of plug-ins using external libraries (bts #200)
• [Project]  Fixed bug with save/load in multi-project contexts (bts #161)
• [Project]  Fixed bug causing delays with -load (bts #180)

Developers Only

• [Cil]  Added 2 components to Cil_types.typ to optimize bitsSizeOf. The proper way to get a default value is Cil.empty_size_cache. The added value must not be shared by types. No one should need to read this value directly.
• [Project]  Preliminary support for direct unmarshalling. Datatypes must define value descr. Using Unmarshal.Direct is okay for now.

Frama-C GUI

• [Gui]  Graphical customization now uses Gtk rc files. A default file is loaded from FRAMAC_SHARE/frama-c.rc. The end user can provide its custom FRAMAC_SHARE/frama-c-user.rc to override defaults.
• [Gui]  Redesign the dialog box for running analysis
• [Gui]  New message panel
• [Gui]  Possible to stop the GUI while computing analysis
• [Gui]  Improved display of summary information when selecting a file.

Plugin Semantic Constant

• Folding Fix bad journalisation

Plugin Syntactic_callgraph

• New design of the callgraph in the GUI. Frama-C now requires ocamlgraph 1.2.
• New option -cg-services-only to only computes the graph of services

Plugin Value

• Improved treatment of conditions involving char or short variables.
• Improved integer division. Now returns best effort results when 0 is among the possible values for the divisor.

Frama-C General

New Features

• [Configure]  For each dynamic plug-in P, a new option --with-P-static is added to configure.in for linking P statically with Frama-C.
• [Configure]  New option -with-all-static in order to statically link all plug-ins, except those explicitly specified as dynamic (bts '430').
• [Configure]  better message when a plug-in isn't enable by default.
• [Configure]  Auto-detection of lablgtk2's custom tree model.
• [Journal]  Journalisation of plug-ins slicing, sparecode, impact and security done.
• [Journal]  Journalisation of functions with labels is now possible (bts '427').
• [Journal]  Operations on projects (bts '436') and code outputs are journalised.
• [Journal]  Option -journal-loader-run does not exist anymore. Use -load-module instead.
• [Journal]  Journal disabled by default in batch mode
• [Kernel]  New implementation of command line parsing
• [Kernel]  Syntax "-option-name=value" is now valid on the command line. In such a case, [value] may begin by '-', which is forbidden for the usual syntax "-option-name value".
• [Kernel]  Better message for errors on the command line.
• [Kernel]  New alias "-h" and "--help" for "-help" (bug #61).
• [Kernel]  Each boolean option now has an opposite.
• [Kernel]  New option -load-script to dynamically compile and load an ocaml script.
• [Kernel]  When loading a module via -load-module, the dynamically registered options are now recognized on the command line.
• [Kernel]  New environment variable FRAMAC_LIB
• [Kernel]  New options -no-type and -no-obj
• [Kernel]  By default, Frama-C stops on annotation errors. Option -continue-annotation-error
• [Kernel]  FRAMAC_DYN_PATH is now called FRAMAC_PLUGIN
• [Logic]  Support for concrete type definition.
• [Logic]  Overloaded logic symbols.

Bug Fixes

• [Cil]  Fixed parsing of global initializers like "(3>0)?0:1" when Cil.lowerConstants is false.
• [Cil]  Fixed some localization problems with frontc visitor.
• [Cil]  Keep track of variables that have block scope (bts '218') uninitialize them at the exit of corresponding block.
• [Configure]  Fixed bug with --disable-* options (except when '*' was a plug-in name).
• [Configure]  Fixed issues in configure and makefile if lablgtk2 is not enabled.
• [Journal]  Fixed bug in journalisation of non-functional values.
• [Journal]  Fixed bug with -disable-journal and type with no pretty-printer.
• [Kernel]  Frama-C has now a very early initialisation step. That's fixed minor issues with -journal-disable (bts #14 and #16).
• [Logic]  Fixed bug in type-checking of polymorphic functions.
• [Logic]  Allow \ as first letter of identifier.
• [Logic]  Changed \result_finite_float into \is_finite_float. Alarm generation is still untyped.
• [Logic]  Fixed predicate typing of \pointer_comparable.
• [Logic]  Fixed bugs in type unification.
• [Makefile]  Fixed bug in compilation of dynamic plug-ins with a GUI.
• [Makefile]  Fixed bug whenever all plug-ins should be static.
• [Project]  Fixed bug #113: loading a session containing a project p referring to another project generated a new incorrect project p.

Developers Only

• [Cil]  C expressions now have a unique ID. See frama-c-commits for details.
• [Configure]  No longer require to modify the end of configure.in when you add a new plug-in.
• [Configure]  Explicitly require >= OCaml 3.10.0
• [Kernel]  Some changes in API of module Type (bts '410'). In particular: 1) module FunTbl no longer exist. Replaced by Type.Tbl 2) Merge of pretty printer registration with type registration. No more in module Journal. Only in module Type.
• [Kernel]  Dynamic plug-ins can now register their own types (abstract from the outside) and operations on such types (bts '413').
• [Kernel]  File.pretty does not take anymore a formatter as argument. The default output is the one specified by option -ocode.
• [Kernel]  Type of Db.register changed in order to be able to say that a function call must never be written in the journal.
• [Kernel]  Dynamic plug-ins have to take care about journalisation.
• [Kernel]  Cil_state is now called Ast and Cil_state.file is now called Ast.get.
• [Kernel]  Possibility to define alias for options.
• [Kernel]  Moved lightweight annotation support from Jessie to Kernel. They are now available for all plugins. Support for lightweight global invariants on globals has been dropped.
• [Kernel]  Db.Main.extend is now of type unit -> unit
• [Logic]  Merge terms and tsets in the AST.
• [Logic]  Tresult has a type attached to it
• [Makefile]  New implementation of (un)verbose mode (bts '442').
• [Makefile]  Fixed "dist" and "bdist" targets that had been broken on 02/27.
• [Makefile]  Independent Makefile for dynamic plug-ins.
• [Project]  Remove functions Project.save and Project.load: cannot ensure their correctness.

Frama-C GUI

New Features

• [Gui]  Add 2 separate pages for stdout and stderr redirections .
• [Gui]  Code annotation and all globals are now reactive to selections (bts '359' and '387').
• [Gui]  Environment variables FRAMAC_MONOSPACEFONT and FRAMAC_GENERALFONT.
• [Gui]  Change the warning to panel to preserve decent performance. This imposes lablgtk 2.12 at least.

Bug Fixes

• [Gui]  Fix a bug with broken UTF-8 output on stdout (bts '420').
• [Gui]  Reentrancy fix with left panels.
• [Gui]  Fixed bug with some utf8 strings.
• [Gui]  Changes having to do with dependencies between computations. Hopefully less problems exist now than before.

Developers Only

• [Gui]  Add function Design.main_window_extension_points#help_message.
• [Gui]  The plug-in GUI is now packed with the core plug-in

Plugin Aorai

• Aorai is now a dynamic plug-in.

Plugin From

• Improved dependencies + bug fixes

Plugin Impact

New Features

• Slicing after impact is now possible (bts '301').
• Do not select anymore the selected statements except if they are effectively impacted themselves (bts '411').
• In the GUI, highlight the selected statement in cyan.

Bug Fixes

• Bug fixed in the GUI (on project switching).
• In the GUI, fixed bug while the analysis raised an exception. It is now properly caught and displayed on stderr.

Plugin InOut

• Add -out-external option.

Plugin Inout

• -input_with_formals is now called -input-with-formals

Plugin Jessie

New Features

• Jessie is now a dynamic plug-in (bts '419').
• GUI mode is now the default, options -jessie-gui and -jessie-goals do not exists anymore
• Option for launching jessie is now -jessie, not -jessie-analysis

Bug Fixes

• Support constant sizeof and alignof in logic terms (bts '396').
• proper message when \lambda is encountered (bts '7528').
• fixed bugs #63 and #71 (labels and \at)
• Fix bug #8, compilation of jessie with Apron
• Support for loop assigns, partially fixes bug #41 see tests/jessie/bts0041-bis.c for details
• Full support for loop assigns, including those implicitly generated from function's assigns, fixes bug #41
• Support for label Post in assigns clauses. Fixes bug #160
• Fixed contract for strchr() and strrchr() in string.h

Plugin Pdg

• The functions that return nodes from an annotations now also return a list of the variables declarations nodes.

Plugin Semantic_callgraph

• small change in the computation of services: the roots are now the same as the syntactic callgraph (while there is no function pointer).
• new options -scg-dump and -scg-init-func consistent with the options -cg-dump and -cg-init-func of the syntactic callgraph.

Plugin Slicing

• New option "-slicing-keep-annotations"

Plugin Sparecode

• Selected an annotation attached to a function call made a wrong propagation in the visibility of the call (bts #3).
• The generated project lost some useful parameters like the entry point (bts #10).

Plugin Syntactic_callgraph

• Fixed bug when the callgraph is computed twice
• Separate services are now created for callees of the entry point.

Plugin Users

• Users are now computed on need while calling !Db.Users.get

Plugin Value

New Features

• Improved support for state reduction on a memory read.
  
  
• Minor changes in floating-point handling.
• Adjustments in the appearance of some alarms
• Improved results for char ones[] = "11111111"; col_ones = 1 + * (int*) ones;
• Trivially redundant alarms are now automatically discharged.
• Improved reduction for (ptr-ptr) expressions.

Bug Fixes

• Miscellaneous fixes and tuning.
• Fixed correctness bug that had a tiny chance to manifest itself when analyzing code that dereferences casted pointers.
• Fixed performance bug.
• Fixed bug that could appear with assignments like t[5] = t[4]; where t[4] is not a singleton.
• Fixed bug with the interpretation of "==>".

Developers Only

• New constructor Signed_overflow_alarm for type Alarms.t

Frama-C General

New Features

• [Kernel]  Changed the definition of non-determinist functions in builtin.c. These functions no longer rely on a volatile variable. Analysis logs may change slightly as a result.
• [Logic]  Added support for (wide) string constants in ACSL formula.

Developers Only

• [Cil]  New methods for visiting compinfo, enuminfo, fieldinfo and enumitem (prevents potential misuse of copy visitor for these types).
• [Cil]  enum items now have their own type and are shared between declaration and use.
• [Cil]  New methods current_function and current_kf methods (bts '406').
• [Cil]  Modified typeForInsertedCast hook to take as arguments the expression and its original type in addition to the destination type.
• [Makefile]  Support for native compilation in Makefile.template (require ocaml >= 3.11).
  
  
• [Makefile]  Fixed various bugs in Makefile.template.

Frama-C GUI

• [Gui]  Improved consistency of some information messages.

Plugin Impact

• In the GUI, new panel to manage impact analysis actions.

Plugin Jessie

• Fixed bug with multiple labels in axiomatic definitions.
• Added example tests/jessie/minimum_sort.c in Jessie tutorial.
• Fixed problem with array in logical annotations.
• Fixed problem with memory model preventing the proof of some pointer programs. The solution is to require pointers that are compared to belong to the same allocated memory block, which can be expressed in logical annotations using equality of \base_addr constructs.

Plugin Slicing

• Unused global variables and types are now removed in sparecode analysis and slicing results.

Plugin Sparecode

• New option -rm-unused-globals to remove unused global variables and types.

Plugin Value

• Abstract structs are now supported in conjunction with option -lib-entry, and invalid to access.
• Removed outdated warning about uninitialized const variables.
• Introduced preliminary support for state reductions on a memory read access. This should eliminate some redundant alarms.

Frama-C General

New Features

• [Journal]  Journalization available (only Cmdline and Occurrence are done yet).
• [Journal]  New options available -load-journal, -journal-name, -journal-disable for user management of journals.
• [Kernel]  Dynamic linking of plugin available (experimental).
• [Kernel]  Added option -warn-unspecified-order to display a warning for each unspecified sequence containing writes.
• [Logic]  Support for \separated.
• [Logic]  Basic support for sets as first-class value.
• [Logic]  Support for address-of operator (&) in tsets.
• [Project]  Projectification of machdep (bts '101').

Bug Fixes

• [Logic]  Fixed bug "0 can be seen as pointer to any type" (bts '338').
• [Logic]  Fixed typing error of pointer lval hidden by typdefs.

Developers Only

• [Cil]  AST changes for unspecified sequences (experimental).
• [Kernel]  Refined UnspecifiedSequence information.
• [Ptests]  Added config option STDOPT (see developer's manual for details).

Frama-C GUI

• [Gui]  Lower the bound on maximum number of displayed globals to 20 (bts '342').

Plugin Deps

• In the GUI, the "Dependencies" contextual menu provides the old "Scope" and "Show Def" features in addition to the new "Zones" feature. These three actions can be launch together with the "All" button.

Plugin Inout

• New option -input_with_formals.

Plugin Jessie

• Fixed path problems with binary distributions.
  
  

Plugin Pdg

• Fixed bugs for CAT/AF evaluation.

Plugin Semantic_callgraph

• New option -scg-dump to dump a semantic callgraph to stdout.

Plugin Slicing

New Features

• In the GUI, request related to read/write accesses to lvalues is available from the contextual submenu.
• In the GUI, implemented feature request related to highlighting when the source function is called, for CAT/AF evaluation.
• In the GUI, new panel to manage slicing actions.
• In the GUI, slicing request related to values returned by functions is available from the contextual submenu.

Bug Fix

• In the GUI, fixed bugs related to enabling/disabling conditions of the slicing submenu.

Plugin Value

New Features

• Added option -no-unspecified-access to disable alarm above.
• Raise alarm for undefined behavior caused by side-effects in UnspecifiedSequence (except for function calls).
• Changed behavior of option -context-valid-pointers to make it more like the documentation says it is.

Bug Fixes

• Fixed huge bug in the computation of the dependencies of an expression. Differences are most visible in the results of options -input and -deps, and of course all she slicing options that make use of these.
• Fixed a bug introduced with the "value concatenation" feature where an imprecise value obtained by reading misaligned data would have the origin "Arithmetic" instead of "Misaligned".

Developers Only

• Removed argument ~skip_base_deps from all functions in Db.Value that had one. This argument did not make sense.