CodePlexProject Hosting for Open Source Software

1

Closed

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))

{

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.

_(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.

No files are attached

## comments

erniecohen wrote May 25 at 1:55 AM

_(assert n

m == nx + n*(m-x))