--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on April 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Single (Trivial?) Assertion Not Verified -- What's Wrong?



Hello, all.

Attached follows a simple function which I was trying to verify with WP 
(Magnesium), as well as the console output generated by

   frama-c-gui -wp -wp-rte neg_to_zero.c

All annotations are verified except one, namely A3. It surprises me that 
WP proves

   //@ assert A1: i <= i < n;  (first inequality obvious, I know)

   //@ assert A2: \forall integer j; i <= j < n ==> v[j] == \at( v[j], 
Pre );

but does not prove

   //@ assert A3: v[i] == \at( v[i], Pre );

Any clue about what is going on here?

Thanks in advance,

-- 
Pablo
http://lia.ufc.br/~pmsf/
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: neg_to_zero.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160404/76224774/attachment.c>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: console_output.txt
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160404/76224774/attachment.txt>