--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on May 2012 ---
Hello Eugene, 2012/5/6 ??????? ??????? <naveugene at mail.ru>: > /*@ > 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 With the above program I have in fact 3 timeouts: """ [wp] [Alt-Ergo] Goal store_cisapb_assert_6_rte : Timeout [wp] [Alt-Ergo] Goal store_cisapb_post_1 : Timeout [wp] [Alt-Ergo] Goal store_cisapb_loop_inv_2_preserved : Timeout """ Goal store_cisapb_post_1 cannot be proved. You probably meant "ensures Equal{Post}(a, b, c, n);", i.e. equality on Post state. Equality in Pre state is obviously invalid. With this modification this VC is proved. For store_cisapb_loop_inv_2_preserved goal, I have used a slightly different loop invariant: """ loop invariant \forall integer k; 0 <= k < i ==> c[k] == a[k] + b[k]; """ For store_cisapb_assert_6_rte goal, I used the same assumption as you, only limiting the assumption to 0 <= k < n. I also used a longer timeout, 20s instead of WP's default 10s. Overall, it gives: """ /*@ 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 \forall integer k; 0 <= k < n ==> (a[k] + b[k] <= 2147483647 && a[k] + b[k] >= -2147483647); requires n <= 2147483647; requires n >= 0; assigns *(c+(0..n-1)); ensures Equal{Post}(a, b, c, n); @*/ void cisapb (const int* a, const int* b, int *c, int n) { /*@ loop invariant 0<=i<=n; loop invariant \forall integer k; 0 <= k < i ==> c[k] == a[k] + b[k]; loop assigns i, c[0..n-1]; loop variant n-i; @*/ for (int i=0; i < n; i++) c[i] = a[i] + b[i]; } """ With result: """ $ frama-c -wp-timeout 20 -wp-rte -wp -wp-proof alt-ergo cisapb.c -then -report [kernel] preprocessing with "gcc -C -E -I. cisapb.c" [rte] annotating function cisapb [wp] [WP:simplified] Goal store_cisapb_function_assigns : Valid [wp] [Alt-Ergo] Goal store_cisapb_assert_8_rte : Valid [wp] [Alt-Ergo] Goal store_cisapb_assert_7_rte : Valid [wp] [Alt-Ergo] Goal store_cisapb_assert_5_rte : Valid [wp] [Alt-Ergo] Goal store_cisapb_loop_inv_1_established : Valid [wp] [Alt-Ergo] Goal store_cisapb_assert_9_rte : Valid [wp] [Alt-Ergo] Goal store_cisapb_loop_inv_2_established : Valid [wp] [Alt-Ergo] Goal store_cisapb_loop_inv_1_preserved : Valid [wp] [Alt-Ergo] Goal store_cisapb_loop_variant_decrease : Valid [wp] [Alt-Ergo] Goal store_cisapb_loop_variant_positive : Valid [wp] [Alt-Ergo] Goal store_cisapb_loop_assigns_2 : Valid [wp] [Alt-Ergo] Goal store_cisapb_post_1 : Valid [wp] [Alt-Ergo] Goal store_cisapb_loop_inv_2_preserved : Valid [wp] [Alt-Ergo] Goal store_cisapb_assert_6_rte : Valid [...] -------------------------------------------------------------------------------- --- Status Report Summary -------------------------------------------------------------------------------- 12 Completely validated 12 Total """ Best regards, d.