--- layout: fc_discuss_archives title: Message 109 from Frama-C-discuss on May 2010 ---
On Thu, 2010-05-27 at 21:38 +0200, Pascal Cuoq wrote: > > NB: this is all using Frama-C 20100401 with a patched version > > of Why 2.23. > > I was confused and I meant a patched version of Why 2.24. According to > http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-April/001877.html > the pragma that I used was not yet available in Why/Jessie 2.23. > The workaround suggested by Claude March? in that message is to > ignore the unprovable VCs for termination. The example you sent me works with my Frama-C Beryllium (2) 20090902 distribution with Why-2.21. -Boris