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

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