Plugin Value

• Add missing C library files.
  
  

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]  'do {...} while(0);' are now translated as '{...}'.
• [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 consilodated 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 in 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 Alarm's.
• [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 explicitely 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 was returning 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.

Plugin Pdg

• 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 agressively 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 splitted 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 agressive 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 that 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 abandonned
• [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

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.

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 implict 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 Ptests

• Ptests adds filename of current test before the options given to frama-c (see #736).

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 agressive state reduction when emiting 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 emited 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

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

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

New Features

• Plug-in WP removed from kernel-releases (now an independent plug-in).
• [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.
  
  
• [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 agressive 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 asynchroneous 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.

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 infered 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 Ptests

• Slightly changed semantics of CMD and STDOPT. See developer manual for more info

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 againts 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 occuring 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 resurected. 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 lightweigth 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 catched 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 implictly 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.

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 Ptests

• Added config option STDOPT (see developer's manual for details).

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.

Frama-C General

New Features

• [Configure]  ./configure will not emit so many warning when gui is not available (bts '296').
• [Kernel]  Do not remove unused static functions.
• [Kernel]  Change -lib-entry option into a boolean. "-lib-entry foo" becomes "-lib-entry -main foo"
• [Logic]  Support for constant predicates and functions (breaks 0-argument old syntax).
• [Logic]  Better error messages for logic typing errors.
• [Logic]  Typing of terms: implement ACSL semantics for integral/real promotions.
• [Logic]  Pretty printing of pointer accesses in terms and tsets are now much nicer. For example *(T+(0+i..j)) becomes T[0+i..j].
• [Logic]  Quantification over arrays are interpreted as quantification over pointers to be consistent with predicates and C function calls.
• [Logic]  \valid* predicates rejects void pointers.
• [Logic]  Merge predicates and logic functions when linking multiple c files.
• [Logic]  Enforce correct return type of logic functions.
• [Logic]  Typing of recursive logic functions.
• [Makefile]  Prefix install directories by the value of DESTDIR (patch contributed by Igor Galic).
• [Project]  Loading works even if the configuration while saving is not exactly equal to the one while loading.

Bug Fixes

• [Kernel]  -machdep was ignored (bts '309').
  
  
• [Kernel]  Correct promotion rules from bitfields to integers.
• [Logic]  Correct typing for predicates: no more dangerous promotions.
• [Makefile]  Fixed bug in "make distclean" (bts '308').

Developers Only

• [Logic]  AST changes for invariants.

Frama-C GUI

• [Gui]  Enforce lablgtksourceview dependency and suppressed camlp4 need.
• [Gui]  First rehighlight support.
• [Gui]  Invalidate display cache on project switching.
• [Gui]  Improve speed of configuration menu.

Plugin Constfold

• Semantic constant folding does not introduce casts by default.
• New option -cast-from-constant has been added to allows cast introductions.

Plugin Impact

• Fixed bug when a function is undefined (bts '322').

Plugin Metrics

• Number of syntactic calls by functions and potential entry points.
• New option -metrics-dump.

Plugin Occurrence

• Occurrences of a variable can be computed from any occurrence of the program (not only from its declaration).

Plugin Pdg

• Improvement of the precision of interprocedural analysis (bts '179').
• Fixed bug in interprocedural analysis (bts '324').

Plugin Slicing

• In the GUI, slicing contextual submenu available.
• Some slicing requests are available from the GUI.

Plugin Sparecode

• New option -sparecode-no-annot (bts '331' and '334').

Plugin Value

• Separate warnings for uninitialized and addresses escaping their scopes (these used to be grouped together as "unspecified" alarms)
• Remove remaining TOP in value analysis: WELL at amx-valid-depth and for leaf functions.
• New implicit context generation with a fixed width of 6 (an option will be available later).
• Some partial builtin_va_start support
• Removed last top from merging leaf functions returns.
• New option -context-width for auto-allocated context pointer width. Defaults to 2.
• Do not emit imprecision tracing warning when a lval=lval is optimized.

Frama-C General

• [Makefile]  Fixed bug in "make clean-doc" (and "make distclean").

Frama-C GUI

• [Gui]  All internal options are available in the GUI preferences pannel.
  
  

Frama-C General

New Feature

• [Kernel]  Option -no-unicode : do not print Unicode chars.
  
  

Bug Fixes

• [Kernel]  Various Win32 path fixes.
• [Project]  Inconsistent data with multiple projects and while removing projects.
• [Project]  Fixed bug in save/load with duplicated computations.

Developers Only

• [Project]  Warnings are project compliant.

Frama-C GUI

New Features

• [Gui]  Large improvements in reactivity
• [Gui]  No file selection on startup.
• [Gui]  Persistent position.
• [Gui]  Buffer memoization for speedup.
• [Gui]  Progress added in existing plugins.
• [Gui]  Project names are pairwise different in the GUI.

Bug Fixes

• [Gui]  Prefs/Execute bugs fixed.
• [Gui]  Win32 default fonts fixed.

Developers Only

• [Gui]  Project management redesigned for older Gtk and for the best.

Plugin Impact

• Available from toplevel through -impact-pragma and -impact-print.

Plugin Scope

• First release of the plug-in (bts '191').

Plugin Value

• Display a warning whenever an unitialized value causes the death of a branch.
• In the GUI, function level information displayed in Information panel.

Frama-C General

• [Makefile]  Fixed bug with GUI compilation.
• [Project]  Fixed bug with checksum computation during save/load.

Frama-C GUI

• [Gui]  GUI no longer frozen during computations.
• [Gui]  'New' menu entry.

Plugin Occurrence

• New option -occurrence.
• First release of the plug-in.

Plugin Slicing

• Fixed bug in interprocedural slicing (bts '201').
  
  

Plugin First

• release