--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on May 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Some unproved VCs occur while using wp



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>