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] How to make wp to prove the invariant successfully?

  • Subject: [Frama-c-discuss] How to make wp to prove the invariant successfully?
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Tue, 7 Feb 2012 06:01:34 +0100
  • In-reply-to: <CALiiei7XaT4q6C5-ij8=2wndqKE-NjShjw8DD0wJ=2OgF2uYKQ@mail.gmail.com>
  • References: <CALiiei7XaT4q6C5-ij8=2wndqKE-NjShjw8DD0wJ=2OgF2uYKQ@mail.gmail.com>
Hello,

On Tue, Feb 7, 2012 at 5:51 AM, Henry <njucslzh0714 at gmail.com> wrote:

>   x = 0;
>   z = 10;
>   /*@ loop invariant ? int x; x>=0;
>   */
>   while (x<=z) {
>     x++;
>   }
> Then the command "frama-c-gui -wp b.c" was executed. But I found that the
> status of the loop invariant was unknown because loop_inv_1_established
> could not decide. The proof obligation was:
> Goal store_phase_loop_inv_1_established:
>   forall x_0:int.
>   is_sint32(x_0) ->
>   (0 <= x_0)
>

The \forall quantifier in your invariant means that "x" in the rest of the
formula is not variable x from the program, but any int x.
You mean to talk about the variable x of the program. For instance, like
this:

  /*@ loop invariant 0 <= x <= (z+1) ;
  */
  while (x<=z) {
    x++;
  }

Frama-C Nitrogen with baseline Wp, together with alt-ergo 0.93, verify this
invariant.

Pascal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120207/542cb617/attachment.htm>