--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on May 2012 ---
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>