--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on September 2009 ---
Hello, On Sep 7, 2009, at 4:26 PM, Hollas Boris (CR/AEY1) wrote: > Can you please summarize the most significant changes to the Lithium > version? Have you seen the file frama-c-Beryllium-20090901/Changelog and if yes, how should we present the information to make it more useful (keeping in mind that making a Frama-C release is already a lot of work, enough work that we do it reluctantly and not quite as often as would be useful)? Pascal __ Preliminary notes: ------------------ Mark "*": bug fixed. Mark "-": change with an impact for users. Mark "o": change with an impact for developers only. Mark "!": change that can break compatibility with existing development. = = = = = = = ======================================================================== = = = = = = = ======================================================================== Open Source Release Beryllium_20090901 = = = = = = = ======================================================================== - Syntactic Callgraph [2009/08/27] New design of the callgraph in the GUI. Frama-C now uses ocamlgraph 1.2. - 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. - Gui [2009/08/18] Improved display of summary information when selecting a file. - Kernel [2009/08/05] New options -kernel-help, -kernel-verbose and -kernel-debug - Syntactic Callgraph [2009/08/04] New option -cg-services-only to only computes the graph of services - Value [2009/07/29] Improved treatment of conditions involving char or short variables. - Gui [2009/07/28] Possible to stop the GUI while computing analysis o Kernel [2009/07/26] Preliminary support for direct unmarshalling. Datatypes must define value descr. Using Unmarshal.Direct is okay for now. -* Kernel [2009/07/24] Fixed bug with static linking of plug-ins using external libraries (bts#200) - Value [2009/07/22] Improved integer division. Now returns best effort results when 0 is among the possible values for the divisor. -* Kernel [2009/07] Fixed bug causing delays with -load (bts #180) - GUI [2009/07/08] New message panel -* Kernel [2009/07/07] Fix generation of invalid variable name in journal -* Semantic Constant Folding [2009/07/07] Fix bad journalisation - GUI [2009/07/03] Redesign the dialog box for running analysis o! CIL [2009/06/24] 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. -o GUI [2009/06/24] 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. -* Kernel [2009/06/24] Fixed bug with save/load in multi-project contexts (bts #161) -* Kernel [2009/06/24] Restore compatibility with ocaml 3.10.2 -* Kernel [2009/06/24] Fixed bug with --disable-gui in configure.in = = = = = = = ======================================================================== Open Source Release Beryllium_20090601 = = = = = = = ======================================================================== o Value [2009/06/23] new constructor Signed_overflow_alarm for type Alarms.t -! Jessie [2009/06/23] option for launching jessie is now -jessie, not -jessie-analysis - Jessie [2009/06/23] Fixed contract for strchr() and strrchr() in string.h -* Jessie [2009/06/23] Support for label Post in assigns clauses. Fixes bug #160 -! Jessie [2009/06/18] GUI mode is now the default, options - jessie-gui and -jessie-goals do not exists anymore -* Jessie [2009/06/18] Full support for loop assigns, including those implictly generated from function's assigns, fixes bug #41 -o GUI [2009/06/18] Change the warning to panel to preserve decent performance. This imposes lablgtk 2.12 at least. - Semantic callgraph [2009/06/15] small change in the computation of services: the roots are now the same as the syntactic callgraph (while there is no function pointer). -! Semantic callgraph [2009/06/15] new options -scg-dump and -scg-init- func consistent with the options -cg-dump and -cg-init-func of the syntactic callgraph. o Users [2009/06/15] Users are now computed on need while calling !Db.Users.get - Kernel [2009/06/15] Journal disabled by default in batch mode -! Kernel [2009/06/10] FRAMAC_DYN_PATH is now called FRAMAC_PLUGIN -* GUI [2009/06/10] Changes having to do with dependencies between computations. Hopefully less problems exist now than before. -* Jessie [2009/06/09] Support for loop assigns, partially fixes bug #41 see tests/jessie/bts0041-bis.c for details o! Kernel [2009/06/09] Db.Main.extend is now of type unit -> unit - Kernel [2009/06/08] By default, Frama-C stops on annotation errors. Option -continue-annotation-error o Kernel [2009/06/05] The plug-in GUI is now packed with the core plug-in -* Jessie [2009/06/05] Fix bug #8, compilation of jessie with Apron - Kernel [2009/06/05] Fixed issues in configure and makefile if lablgtk2 is not enabled. o! Kernel/Jessie [2009/06/03] 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 [2009/06/03] Fixed bug #113: loading a session containing a project p referring to another project generated a new incorrect project p. o! Kernel [2009/06/03] Remove functions Project.save and Project.load: cannot ensure their correctness. - Kernel [2009/05/29] New options -no-type and -no-obj - Kernel [2009/05/29] New environment variable FRAMAC_LIB - Kernel [2009/05/29] When loading a module via -load-module, the dynamically registered options are now recognized on the command line. - Kernel [2009/05/29] New option -load-script to dynamically compile and load an ocaml script. -! Kernel [2009/05/29] Option -journal-loader-run does not exist anymore. Use -load-module instead. !o Logic [2009/05/29] Tresult has a type attached to it -* Jessie [2009/05/22] fixed bugs bts #63 and #71 (labels and \at) - Slicing [2009/05/20] New option "-slicing-keep-annotations" o Pdg [2009/05/20] The functions that return nodes from an annotations now also return a list of the variables declarations nodes. - Kernel [2009/05/18] Each boolean option now has an opposite. - Kernel [2009/05/15] New alias "-h" and "--help" for "- help" (fixed bug#61). o Kernel [2009/05/15] Possibility to define alias for options. - Kernel [2009/05/14] Better message for errors on the command line. - Kernel [2009/05/14] 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". -* Value [2009/05/11] Fixed bug with the interpretation of "==>". - Value [2009/05/04] Improved reduction for (ptr-ptr) expressions. - Value [2009/04/28] Trivially redundant alarms are now automatically discharged. - Value [2009/04/28] Improved results for char ones[] = "11111111"; col_ones = 1 + * (int*) ones; o Configure [2009/04/21] Explicitly require >= OCaml 3.10.0 -! Inout [2009/04/17] -input_with_formals is now called -input- with-formals -o! Kernel [2009/04/15] New implementation of command line parsing -* Kernel [2009/04/08] Frama-C has now a very early initialisation step. That's fixed minor issues with -journal-disable (bts#14 and 16). o! Kernel [2009/04/07] Cil_state is now called Ast and Cil_state.file is now called Ast.get. -* Sparecode [2009/04/07] Selected an annotation attached to a function call made a wrong propagation in the visibility of the call (bts#3). -* Sparecode [2009/04/07] The generated project lost some useful parameters like the entry point (bts#10). o Makefile [2009/04/03] Independent Makefile for dynamic plug-ins. - Configure [2009/04/01] Auto-detection of lablgtk2's custom tree model. -* Configure [2009/04/01] Fixed bug with --disable-* options (except when '*' was a plug-in name). - Logic [2009/03/27] Overloaded logic symbols. -* Jessie [2009/03/27] proper message when \lambda is encountered (forge-bts#7528). - Configure [2009/03/27] better message when a plug-in isn't enable by default. -* Syntactic_callgraph [2009/03/26] Fixed bug when the callgraph is computed twice -* Logic [2009/03/24] Fixed bugs in type unification. -* Value [2009/03/23] Fixed bug that could appear with assignments like t[5] = t[4]; where t[4] is not a singleton. o* Makefile [2009/03/20] Fixed "dist" and "bdist" targets that had been broken on 02/27. -* Value [2009/03/20] Fixed performance bug. - Gui [2009/03/20] Environment variables FRAMAC_MONOSPACEFONT and FRAMAC_GENERALFONT. o! Cil [2009/03/19] C expressions now have a unique ID. See frama-c-commits for details. -* From [2009/03/17] Improved dependencies + bug fixes -* Gui [2009/03/17] Fixed bug with some utf8 strings. -* Value [2009/03/13] Fixed correctness bug that had a tiny chance to manifest itself when analyzing code that dereferences casted pointers. -* Logic [2009/03/11] Fixed predicate typing of \pointer_comparable. -* Logic [2009/03/11] Changed \result_finite_float into \is_finite_float. Alarm generation is still untyped. * Logic [2009/03/11] Allow \ as first letter of identifier. o Makefile [2009/02/27] New implementation of (un)verbose mode (old- bts#442). -* Value [2009/02/24] Miscellaneous fixes and tuning. -* Cil+Value [2009/02/23] Keep track of variables that have block scope (old-bts#218) uninitialize them at the exit of corresponding block. - InOut [2009/02/18] Add -out-external option. * Cil [2009/02/18] Fixed some localization problems with frontc visitor. o! Logic [2009/02/13] Merge terms and tsets in the AST. - Value [2009/02/09] Adjustments in the appearance of some alarms * Cil [2009/02/03] Fixed parsing of global initializers like "(3>0)?0:1" when Cil.lowerConstants is false. o Gui [2009/01/29] Add function Design.main_window_extension_points#help_message. o! Kernel [2009/01/28] Dynamic plug-ins have to take care about journalisation. o! Kernel [2009/01/26] Type of Db.register changed in order to be able to say that a function call must never be written in the journal. - Kernel [2009/01/23] Operations on projects (old-bts#436) and code outputs are journalised. o! Kernel [2009/01/23] File.pretty does not take anymore a formatter as argument. The default output is the one specified by option -ocode. - Journal [2009/01/23] Journalisation of functions with labels is now possible (old-bts#427). - Journal [2009/01/21] Journalisation of plug-ins slicing, sparecode, impact and security done. - Value [2009/01/20] Minor changes in floating-point handling. -* Journal [2009/01/19] Fixed bug with -disable-journal and type with no pretty-printer. - Configure [2009/01/19] New option -with-all-static in order to statically link all plug-ins, except those explicitely specified as dynamic (old-bts#430). -* Journal [2009/01/19] Fixed bug in journalisation of non- functional values. -* Makefile [2009/01/19] Fixed bug whenever all plug-ins should be static. -* Makefile [2009/01/19] Fixed bug in compilation of dynamic plug-ins with a GUI. -* Logic [2009/01/09] Fixed bug in type-checking of polymorphic functions. - Logic [2009/01/09] Support for concrete type definition. - Aorai [2009/01/08] Aorai is now a dynamic plug-in. - Jessie [2009/01/08] Jessie is now a dynamic plug-in (old- bts#419). - Configure [2009/01/08] For each dynamic plug-in P, a new option --with-P-static is added to configure.in for linking P statically with Frama-C. o Configure [2009/01/08] No longer require to modify the end of configure.in when you add a new plug-in. o Kernel [2009/01/06] Dynamic plug-ins can now register their own types (abstract from the outside) and operations on such types (old-bts#413). o! Kernel [2009/01/05] Some changes in API of module Type (old-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. -* GUI [2008/12/22] Reentrancy fix with left panels. -* Impact [2008/12/22] In the GUI, fixed bug while the analysis raised an exception. It is now properly catched and displayed on stderr. - Impact [2008/12/22] In the GUI, highlight the selected statement in cyan. -! Impact [2008/12/22] Do not select anymore the selected statements except if they are effectively impacted themselves (old-bts#411). -! GUI [2008/12/21] Code annotation and all globals are now reactive to selections (old-bts#359 and #387). -* Jessie [2008/12/20] Support constant sizeof and alignof in logic terms (old-bts#396). -* GUI [2008/12/20] Fix a bug with broken UTF-8 output on stdout (old-bts#420). - GUI [2008/12/20] Add 2 separate pages for stdout and stderr redirections . - Syntactic callgraph [2008/12/20] Separate services are now created for callees of the entry point. - Impact [2008/12/19] Slicing after impact is now possible (old- bts#301). -* Impact [2008/12/19] Bug fixed in the GUI (on project switching). - Value [2008/12/18] Improved support for state reduction on a memory read. = = = = = = = ======================================================================== Open Source Release Lithium_20081201 = = = = = = = ========================================================================