Not able to verify


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 May 25 at 12:56 AM by erniecohen
won't fix


erniecohen wrote May 25 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))