1

Closed

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.
Closed Today at 12:56 AM by erniecohen
won't fix

comments

erniecohen wrote Today at 12:55 AM

VCC is not very good at nonlinear arithmetic, so if you do something like this that requires nonlinear reasoning, it will often need help. One way to do this is to try to assert what it might be missing, and to make these assertions trigger appropriately by using the switch /oaf (operators as functions), which causes arithmetic operators to be treated like ordinary function symbols. Here, you have only to add the following hint before the assignment of a:

_(assert nm == nx + n*(m-x))