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] Value Analysis Carbon patchlevel 1

  • Subject: [Frama-c-discuss] Value Analysis Carbon patchlevel 1
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Wed, 23 Feb 2011 20:53:16 +0100
Frama-C Carbon has been released earlier this month.
It is the most powerful, usable and stable version of
Frama-C so far.

A lot remains to be done, however, and a new
development cycle has already begun. During
this new cycle what needs to be fixed will be fixed
with, we admit, little regard for compatibility.
The next release will require from
external plug-ins the same kind of small adaptations
that each previous version has historically brought.

Still, the creation of binary packages does not seem
to have started yet. Meanwhile, several bugs have been
fixed in the value analysis. Some are rare
bugs that have been there for a long time without
bothering anyone yet. Some are related to
improvements introduced in Carbon (handling of
floating-point, faster propagation algorithms). And
a good number of these bugs were contributed
by John Regehr. We will come back on those later.

I have isolated these fixes in the attached patch,
that applies to the Carbon 20110201 release.
I would like to recommend that packagers and
users of the value analysis who compile from source
use this patch.

You can ignore this message if you do not use
the value analysis either directly or indirectly,
or if you are a collaborator with access to the
development version.

Use commands such as:
$ mv frama-c-Carbon-20110201 frama-c-Carbon-20110201-value_pl1
$ cd frama-c-Carbon-20110201-value_pl1/
$ patch -p1 < ../value_Carbon_patchlevel1

You should get:
patching file src/ai/abstract_interp.ml
patching file src/ai/abstract_interp.mli
patching file src/ai/ival.ml
patching file src/ai/ival.mli
patching file src/ai/lattice_With_Isotropy.mli
patching file src/memory_state/cvalue_type.ml
patching file src/memory_state/hptset.ml
patching file src/memory_state/hptset.mli
patching file src/memory_state/lmap.ml
patching file src/memory_state/locations.ml
patching file src/memory_state/locations.mli
patching file src/memory_state/offsetmap.ml
patching file src/memory_state/offsetmap.mli
patching file src/value/builtins.ml
patching file src/value/current_table.ml
patching file src/value/eval.ml

Use the standard compilation instructions from that point.

The list of changes is below.

Pascal
__

-  Value      [2011/02/23] Improved informative messages about addresses
	      of locals escaping their scope.
-  Value      [2011/02/22] Take Flush-To-Zero possibility into account
	      for single-precision floats.
-* Value      [2011/02/20] Bug #732: Synthetic results were partial
	      when -slevel was set not high enough to unroll loops
	      completely.
-* Value      [2011/02/15] Fixed bug when passing struct as argument to
	      function with a big-endian target architecture.
-* Value      [2011/02/14] Fixed bug when passing bitfield
	      as argument to function. (jrrt)
-* Value      [2011/02/12] Fixed forgotten warning when passing completely
	      undefined lvalue as argument to function. (jrrt)
-* Value      [2011/02/12] Fixed correctness bug involving nested structs
	      (jrrt)
-* Value      [2011/02/12] Fixed crash when passing invalid argument to
	      function, found by John Regehr using random testing (jrrt)
-* Value      [2011/02/09] Fixed representation of unknown single-precision
	      floats in initial context (it used to be the same as for
	      an unknown double).
-* Value      [2011/02/09] Changes related to 0., +0., -0., sort of thing.
	      Unwarranted loss of precision fixed.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: value_Carbon_patchlevel1
Type: application/octet-stream
Size: 63577 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110223/39c41e3e/attachment-0001.obj>