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] Some unproved VCs occur while using wp

  • Subject: [Frama-c-discuss] Some unproved VCs occur while using wp
  • From: naveugene at mail.ru (Евгений Головко)
  • Date: Mon, 07 May 2012 01:35:35 +0400
Hi!
I'm new Frama-C and wp- user. So my question can have some simple answer but I can't find it by myself.
I try to write a procedure which summs elements of two different arrays to the third (c[i] = a[i] + b[i]) with corresponding annotations. It looks like
 /*@ 
 predicate Equal{Q}(int* a, int* b, int* c, int n) = \forall int k; 0 <= k < n ==> \at(c[k], Q) == \at(a[k], Q) + \at(b[k], Q);
*/ 
 /*@ requires \valid(a +(0..n-1));
 requires \valid(b +(0..n-1));
 requires \valid(c +(0..n-1));
 requires \separated(a+(0..n-1), b+(0..n-1), c+(0..n-1));
 requires n <= 2147483647;
 requires n >= 0;
 
 assigns *(c+(0..n-1));
 ensures Equal{Old}(a, b, c, n);
 @*/ 
void cisapb (const int* a, const int* b, int c[], int n)
{
 /*@ loop invariant 0<=i<=n;
?loop invariant Equal{Here}(a, b, c, i);
 
?loop assigns i, c[0..n-1]; 
?loop variant n-i;
 @*/ 
for (int i=0; i < n; i++) c[i] = a[i] + b[i];
}but when I try to verify this calling 'frama-c -wp -wp-rte -wp-proof alt-ergo cisapb.c -then -report', I have
[wp] [Alt-Ergo] Goal store_cisapb_assert_6_rte : Timeout
[wp] [Alt-Ergo] Goal store_cisapb_loop_inv_2_preserved : Timeout

and at the report
[ Unknown ] Function 'cisapb' loop invariant Equal{Here}(a, b, c, i);
[ Unknown ] Function 'cisapb' assert?rte: (a[i]+b[i] ? 2147483647) ??(a[i]+b[i] ? (-0x7FFFFFFF-1));
Then I try to add annotationrequires \forall int k; 0 <= k <= n ==> (a[k] + b[k] <= 2147483647 && a[k] + b[k] >= -2147483647);

But no effect occurs

What I do wrong??

Regards, Eugene
?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120507/7f703634/attachment.html>