Frama-C General

New Features

• Feature #484 about requires into named behaviors
• [Cil]  Be less agressive during inline function merge. Alpha equivalent function are now kept separated.
• [Configure]  Better detection of native dynlink support.
• [Makefile]  Fix bug #528 when building a dynamic plug-in in a sandbox.

Bug Fixes

• Checking for loop variant position
• Fixed bug in handling of -cpp-command
• Tried to fix all permissions on *.{c,h} files
• [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)
• [Configure]  Fixed bug in configuration of external plug-ins
• [Logic]  fix bug #454 (multiple labels in same statement)
• [Logic]  Fixed wrong precedence of <==>
• [Logic]  Fix bug #498 (behaviors within same scope must now have unique names)
• [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

Developpers Only

• Deprecate Globals.Functions.find_englobing_kf. Use Kernel_function.find_englobing_kf which has a much better complexity instead.
• Ptmap (resp. Ptset) is renamed into Hptmap (Hptset)
• Fix bug #441 (keep track of original names in AST)
• Added field b_extended in behaviors to support grammar extensions
• Remove deprecated annotation_status of AAssert in the AST
• Refactoring of properties_status.ml, part I
• [Cil]  Fix bug #489: constant literal present in original source are preserved in the AST. NB: this implies that they might be explicitely cast when an integer conversion occur.
• [Cil]  Support for custom extension in grammar of behaviors. See Logic_typing.register_behavior_extension.
• [Cil]  Cil.makeLocalVar now inserts the variable into one of the function's local blocks.
• [Cil]  Preliminary support for function calls in UnspecifiedSequence
• [Cil]  global_annotation has location information
• [Cil]  Removed function varinfo_from_vid. You can use maps or hashtables indexed by varinfos directly instead.
• [Logic]  Fix bug #505 (Associate default label for predicates with a single label parameter and no argument)
• [Logic]  Parameterize search of field in logic typing functor in a similar way to search of other C symbols
• [Project]  Reimplementation of the project library (the contents of directory src/project). New API.

Frama-C GUI

New Features

• Better graph display. Require ocamlgraph > 1.4
• 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.
• 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.
• One tooltip by parameter in the launcher
• Fixed parsing of floats in frama-c-gui.config

Bug Fix

• Fix bug with toolbar button 'duplicate project'

Plug-in From

• Improved interpretation of assigns clauses

Plug-in 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

Bug Fix

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

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

Plug-in Security_slicing

• Only use the GUI; does not require it anymore

Plug-in Slicing

• Fixed bug #448 about -keep-annotations option

Plug-in 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.
• 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()];}

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.

Developpers 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

Frama-C General

New Features

• Add status for all clauses
• Clarification of the multiple accesses warning. Becomes "undefined multiple accesses in expression".
• Better error messages when a dynamic plug-in cannot be loaded.
• Better -*-help.
• New option -no-dynlink in order to prevent loading of dynamic plug-ins.
• Backtrace when Frama-C is crashing (only if Frama-C is compiled with caml >= 3.11.0)
• New option "-plugin-h" as an alias for option "-plugin-help"
• Preliminary standard C library in $FRAMAC_SHARE/libc
• The journal is generated only if the GUI is crashing, or if the option -journal-enable is explicitely set (fixed issue #330).
• [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.
• [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]  Adding "\pi" as built-in symbol
• [Logic]  Support for type abbreviation in logic
• [Logic]  Support for "reads \nothing"

Bug Fixes

• -kernel-debug and -kernel-verbose did not work as expected (bts #343).
• -load-script did not clean up compiled files after exiting (fixed bug #371)
• [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.
• [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]  Support for abrupt clauses; Modifies AST
• [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)

Developpers Only

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

Frama-C GUI

New Features

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

Bug Fixes

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

Developpers Only

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

Plug-in Impact

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

Plug-in Inout

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

Plug-in Security

• No more distributed.

Plug-in Security_slicing

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

Plug-in Slicing

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

Plug-in Syntactic_callgraph

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

Plug-in 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
• 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
• Clarified progress messages

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.

Developpers 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

• Slightly less false alarms with -warn-unspecified-order
• [Configure]  Detection of dot if required.
• [Journal]  Better handling of exceptions.
• [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.

Developpers 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

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

Plug-in Jessie

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

Plug-in Obfuscator

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

Plug-in Syntactic

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

Plug-in Syntactic_callgraph

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

Plug-in Value

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

Frama-C General

New Features

• 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

• Restore compatibility with ocaml 3.10.2
• [Configure]  Fixed bug with --disable-gui in configure.in
• [Journal]  Fix generation of invalid variable name in journal
• [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)

Developpers 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

• 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.
• Redesign the dialog box for running analysis
• New message panel
• Possible to stop the GUI while computing analysis
• Improved display of summary information when selecting a file.

Plug-in Semantic

• Constant Folding Fix bad journalisation

Plug-in Syntactic_callgraph

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

Plug-in 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

• 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".
• Better message for errors on the command line.
• New alias "-h" and "--help" for "-help" (bug #61).
• Each boolean option now has an opposite.
• New option -load-script to dynamically compile and load an ocaml script.
• When loading a module via -load-module, the dynamically registered options are now recognized on the command line.
• New environment variable FRAMAC_LIB
• New options -no-type and -no-obj
• By default, Frama-C stops on annotation errors. Option -continue-annotation-error
• New implementation of command line parsing
• FRAMAC_DYN_PATH is now called FRAMAC_PLUGIN
• [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 explicitely 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]  Journal disabled by default in batch mode
• [Journal]  Option -journal-loader-run does not exist anymore. Use -load-module instead.
• [Logic]  Support for concrete type definition.
• [Logic]  Overloaded logic symbols.

Bug Fixes

• Frama-C has now a very early initialisation step. That's fixed minor issues with -journal-disable (bts #14 and #16).
• [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.
• [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.

Developpers Only

• Dynamic plug-ins can now register their own types (abstract from the outside) and operations on such types (bts '413').
• Possibility to define alias for options.
• 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.
• File.pretty does not take anymore a formatter as argument. The default output is the one specified by option -ocode.
• Type of Db.register changed in order to be able to say that a function call must never be written in the journal.
• Dynamic plug-ins have to take care about journalisation.
• Cil_state is now called Ast and Cil_state.file is now called Ast.get.
• 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.
• Db.Main.extend is now of type unit -> unit
• [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
• [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

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

Bug Fixes

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

Developpers Only

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

Plug-in Aorai

• Aorai is now a dynamic plug-in.

Plug-in From

• Improved dependencies + bug fixes

Plug-in Impact

New Features

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

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.

Plug-in InOut

• Add -out-external option.

Plug-in Inout

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

Plug-in 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

Plug-in Pdg

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

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

Plug-in Slicing

• New option "-slicing-keep-annotations"

Plug-in 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).

Plug-in Syntactic_callgraph

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

Plug-in Users

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

Plug-in 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 "==>".

Developpers Only

• New constructor Signed_overflow_alarm for type Alarms.t

Frama-C General

New Features

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

Developpers Only

• [Cil]  New methods for visiting compinfo, enuminfo, fieldinfo and enumitem (prevents potential misuse of copy visitor for these types).
• [Cil]  New methods current_function and current_kf methods (bts '406').
• [Cil]  enum items now have their own type and are shared between declaration and use.
• [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

• Improved consistency of some information messages.

Plug-in Impact

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

Plug-in Jessie

• Added example tests/jessie/minimum_sort.c in Jessie tutorial.
• Fixed bug with multiple labels in axiomatic definitions.
• 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.

Plug-in Slicing

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

Plug-in Sparecode

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

Plug-in Value

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

Frama-C General

New Features

• Dynamic linking of plugin available (experimental).
• Added option -warn-unspecified-order to display a warning for each unspecified sequence containing writes.
• [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.
• [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.

Developpers Only

• Refined UnspecifiedSequence information.
• [Cil]  AST changes for unspecified sequences (experimental).

Frama-C GUI

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

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

Plug-in Inout

• New option -input_with_formals.

Plug-in Jessie

• Fixed path problems with binary distributions.

Plug-in Pdg

• Fixed bugs for CAT/AF evaluation.

Plug-in Ptests

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

Plug-in Semantic_callgraph

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

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

Plug-in 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".

Developpers 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

• Do not remove unused static functions.
• Change -lib-entry option into a boolean. "-lib-entry foo" becomes "-lib-entry -main foo"
• [Configure]  ./configure will not emit so many warning when gui is not available (bts '296').
• [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]  Enforce correct return type of logic functions.
• [Logic]  Typing of recursive logic functions.
• [Logic]  Support for constant predicates and functions (breaks 0-argument old syntax).
• [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.
• [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

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

Developpers Only

• [Logic]  AST changes for invariants.

Frama-C GUI

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

Plug-in Constfold

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

Plug-in Impact

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

Plug-in Metrics

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

Plug-in Occurrence

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

Plug-in Pdg

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

Plug-in Slicing

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

Plug-in Sparecode

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

Plug-in Value

• New implicit context generation with a fixed width of 6 (an option will be available later).
• Some partial builtin_va_start support
• New option -context-width for auto-allocated context pointer width. Defaults to 2.
• 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.
• Removed last top from merging leaf functions returns.
• 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

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

Frama-C General

New Feature

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

Bug Fixes

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

Developpers Only

• [Project]  Warnings are project compliant.

Frama-C GUI

New Features

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

Bug Fixes

• Prefs/Execute bugs fixed.
• Win32 default fonts fixed.

Developpers Only

• Project management redesigned for older Gtk and for the best.

Plug-in Impact

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

Plug-in Scope

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

Plug-in Value

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

Frama-C General

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

Frama-C GUI

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

Plug-in Occurrence

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

Plug-in Slicing

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

Plug-in First

• release