--- layout: fc_discuss_archives title: Message 70 from Frama-C-discuss on February 2011 ---
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>