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

[Frama-c-discuss] Problem running frama-c in Windows



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>