Invariant

Aug 18, 2013 at 2:09 PM
Hi,

i try to verify a c code with vcc but it don't work. the code remove all the element of an array.

void mem_clear(int *a, unsigned long width)
// sets buffer a of length width to 0,
// as specified by the following contract
_(writes \array_range(a,width))
_(requires \mutable_array(a,width))
_(ensures \forall unsigned long i; i < width ==> a[i] == 0)
{
// add code here

unsigned long i = 0;
while(i < width)
_(invariant 0 <= i && i <= width)       
{
    a[i] = 0;
    i++;
}

_(assert \forall unsigned long i; i < width ==> a[i] == 0)
}

Hier is the fould:

Fehler1Post condition '\forall unsigned long i; i < width ==> a[i] == 0)' did not verify.C:\Users\Nar6Win7\AppData\Roaming\Local Libraries\Lokale Dokumente\Visual Studio 2012\Projects\Homework\Aufgabe 1\Memcopy\memcopy.c571