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: loic.correnson at cea.fr (Loïc Correnson)
  • Date: Tue, 7 Feb 2012 12:58:22 +0100
  • In-reply-to: <CALiiei7XaT4q6C5-ij8=2wndqKE-NjShjw8DD0wJ=2OgF2uYKQ@mail.gmail.com>
  • References: <CALiiei7XaT4q6C5-ij8=2wndqKE-NjShjw8DD0wJ=2OgF2uYKQ@mail.gmail.com>
Missing also : @loop assigns x ; since the loop is modifying x.
	L.

Le 7 f?vr. 12 ? 05:51, Henry a ?crit :

> Hi,
> I encounter a problem about the plugin wp. Here given a simple  
> program named b.c as follow
> void phase(void)
> {
>   int x;
>   int z;
>   x = 0;
>   z = 10;
>   /*@ loop invariant ? int x; x>=0;
>   */
>   while (x<=z) {
>     x++;
>   }
>   return;
> }
>
> void main(void)
> {
>   phase();
>   return;
> }
>
> 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)
>
> I think the reason is that wp didn't consider the initial value of  
> x. Can wp prove this invariant?
>
> Best wishes.
> Henry
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss