--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on January 2014 ---
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>