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

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.