This project is read-only.

loops not working in vcc?

Aug 13, 2011 at 5:41 PM

i tried this simple example in the online vcc

#include <vcc.h>

int main(void)
{
  unsigned i;
  for (i = 0; i < 2; i++)
    ;
  _(assert i == 2);
}

 

but the assert did not verify. Why?

 

Aug 13, 2011 at 7:15 PM

Hi there,

  in VCC loops need to be annotated with invariants. Without a loop invariant, VCC would here just know that the exit condition does not hold, i.e., _(assert i >= 2) can be proven straight away after the loop without a loop invariant. To prove your assertion above, you need to add _(invariant i <= 2) as a loop invariant, as listed below:

#include <vcc.h>

int foo1(void)
{
  unsigned i;
  for (i = 0; i < 2; i++)
    ;
  _(assert i >= 2);
}

int foo2(void)
{
  unsigned i;
  for (i = 0; i < 2; i++)
    _(invariant i <= 2)
    ;
  _(assert i == 2);
}

  You can find more information on loop invariant in the VCC tutorial (linked from the front page).

  Cheers, Mark