--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on September 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Release Beryllium 20090901



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
= 
= 
= 
= 
= 
= 
= 
========================================================================