--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on June 2010 ---
Hi David, Yes, that was exactly the problem! I added \forall integer i; 0<=i && i<n ==> -2147483647 <= v[i] <= 2147483647; to both the contractum and the loop invariant and now all my VCs are verified. Thank you Ricardo On Mon, Jun 21, 2010 at 10:07 PM, David MENTRE <dmentre at linux-france.org>wrote: > Hello, > > 2010/6/21 Ricardo Almeida <ricardoalmeida1985 at gmail.com>: > > and in order to complete what I'm trying to do, that would be more useful > to > > me than to set gwhy working. I should add that I actually know the code > line > > that causes 1 VC not to be verified, it is > > > > v[i] = -v[i] > > If your 'v' is a int array, that you might stumble on the same issue > as Viktoriia about ten days ago, i.e. you cannot do y=-x if x==-2^31 > because positive C ints are limited to 2^31-1. > > http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-June/002107.html > > Best regards, > d. > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100622/d43d59a8/attachment-0001.htm>