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: njucslzh0714 at gmail.com (Henry)
  • Date: Tue, 7 Feb 2012 12:51:43 +0800
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120207/b418750b/attachment.htm>