--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on June 2010 ---
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.