1
Vote

Not able to verify

description

unsigned mult (unsigned n, unsigned m)
_(requires m >= 0 && m <= UINT_MAX && n*m <= UINT_MAX)
_(ensures \result == n*m) {
unsigned a = 0;
unsigned x = 0;
while (x < m)
_(invariant (a == n*x) && (0 <= x) && (x <= m))
{
a = a + n;
x = x + 1;
}
return a;
}

While trying to verify the above program, VCC gave the following error:
a+n might overflow

I am not able to understand how a+n might overflow when I have taken the precondition accordingly.

comments