--- layout: fc_discuss_archives title: Message 109 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Non-terminating loops



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