--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on April 2016 ---
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>