--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Proving Memory Safety of String Algorithms without Providing Loop Invariants



On Mon, Jan 20, 2014 at 8:10 AM, Juergen Giesl <
giesl at informatik.rwth-aachen.de> wrote:

> We would like to let Frama-C generate loop invariants by itself. To this
> end, we also installed apron 0.9.10. We tried to compile Why (including
> Jessie) with the option --enable-apron which would in turn allow us to
> start Jessie with the option -jessie-infer-annot. But unfortunately, we did
> not manage to compile Why with this option. The output of the compiler is
> attached in why.err. Indeed, Yannick Moy told us that the code for loop
> invariant generation was most likely removed from Why2.
>

Try the attached patch, which I apply to the Fedora Linux build of why to
fix this build error.  Regards,
-- 
Jerry James
http://www.jamezone.org/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140120/0b42c74b/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: why-2.33-hashtbl.patch
Type: text/x-patch
Size: 2169 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140120/0b42c74b/attachment.bin>