Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Single (Trivial?) Assertion Not Verified -- What's Wrong?
  • From: pmsf at lia.ufc.br (Pablo M. S. Farias)
  • Date: Mon, 04 Apr 2016 18:53:15 -0300
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>