This project is read-only.


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 1:56 AM by erniecohen
won't fix


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