Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Release Beryllium 20090901


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)?


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  
	      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
-  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  
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  
	      external libraries (bts#200)
-  Value      [2009/07/22] Improved integer division. Now returns best  
	      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  
-* 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  
	      bitsSizeOf. The proper way to get a default value is
	      Cil.empty_size_cache. The added value must not be shared by  
	      No one should need to read this value directly.
-o GUI        [2009/06/24] Graphical customization now uses Gtk rc  
	      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
Open Source Release Beryllium_20090601

o Value	      [2009/06/23] new constructor Signed_overflow_alarm for  
-! Jessie     [2009/06/23] option for launching jessie is now -jessie,  
- Jessie      [2009/06/23] Fixed contract for strchr() and strrchr() in
-* 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  
	      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  
	      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- 
	      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
-  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  
	      Option -continue-annotation-error
o  Kernel     [2009/06/05] The plug-in GUI is now packed with the core  
-* 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 and  
	      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  
	      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  
               now also return a list of the variables declarations  
- Kernel      [2009/05/18] Each boolean option now has an opposite.
- Kernel      [2009/05/15] New alias "-h" and "--help" for "- 
help" (fixed
o Kernel      [2009/05/15] Possibility to define alias for options.
- Kernel      [2009/05/14] Better message for errors on the command  
- Kernel      [2009/05/14] Syntax "-option-name=value" is now valid on  
	      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- 
-o! Kernel    [2009/04/15] New implementation of command line parsing
-* Kernel     [2009/04/08] Frama-C has now a very early initialisation  
	      That's fixed minor issues with -journal-disable (bts#14 and 16).
o! Kernel     [2009/04/07] Cil_state is now called Ast and  
	      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  
-* 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  
-* Configure  [2009/04/01] Fixed bug with --disable-* options (except  
	      '*' was a plug-in name).
-  Logic      [2009/03/27] Overloaded logic symbols.
-* Jessie     [2009/03/27] proper message when \lambda is encountered
-  Configure  [2009/03/27] better message when a plug-in isn't enable by
-* 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  
	      broken on 02/27.
-* Value      [2009/03/20] Fixed performance bug.
-  Gui        [2009/03/20] Environment variables FRAMAC_MONOSPACEFONT  
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
-* Logic      [2009/03/11] Fixed predicate typing of  
-* Logic      [2009/03/11] Changed \result_finite_float into  
	      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- 
-* 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
-  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  
	      when Cil.lowerConstants is false.
o  Gui        [2009/01/29] Add function
o! Kernel     [2009/01/28] Dynamic plug-ins have to take care about
o! Kernel     [2009/01/26] Type of Db.register changed in order to be  
	      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  
	      possible (old-bts#427).
-  Journal    [2009/01/21] Journalisation of plug-ins slicing,  
	      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  
-* 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  
-  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- 
-  Configure  [2009/01/08] For each dynamic plug-in P, a new option
	      --with-P-static is added to for linking P
	      statically with Frama-C.
o  Configure  [2009/01/08] No longer require to modify the end of 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  
	      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
-  GUI	      [2008/12/20] Add 2 separate pages for stdout and stderr
	      redirections .
-  Syntactic callgraph [2008/12/20] Separate services are now created  
	      callees of the entry point.
-  Impact     [2008/12/19] Slicing after impact is now possible (old- 
-* 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