--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to make wp to prove the invariant successfully?



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>