--- layout: fc_discuss_archives title: Message 27 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



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.