--- layout: fc_discuss_archives title: Message 44 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



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.