I am looking for some assistance on my program which will not verify. VCC reports that my two invariants will not verify and that my program could experience a math overflow issue. I have tried several things. I am new to VCC.
My program listing follows below:
include <vcc.h>
include <stdio.h>
include <conio.h>
include <limits.h>
int add(int a, int b)
_(requires a < INT_MAX && a > INT_MIN )
_(requires b < INT_MAX && b > INT_MIN )
_(ensures \result < INT_MAX && \result > INT_MIN ==>\result == a + b)
_(decreases 0)
{
int sum = a;
if (b< 0)
{
int n;
for (n = b; n < 0; n++)
_(invariant sum < INT_MAX && sum > INT_MIN ==> sum + n == a + b)
_(invariant 0 <= n)
{
_(decreases n)
sum = sum  1;
}
}
else
{
int n;
for (n = b; n > 0; n)
_(invariant sum < INT_MAX && sum > INT_MIN ==> sum + n == a + b)
_(invariant 0 <= n)
{
_(decreases n)
sum = sum + 1;
}
}
return sum;
}
VCC reports the following:, so any suggestions would be greatly appreciated:
C:\benchmarks\addmultBM2.c(24,16) : error VC9500: Loop body invariant 'sum < 2147483647 && sum > (2147483647  1) ==> sum + n == a + b' did not verify.
C:\benchmarks\addmultBM2.c(35,20) : error VC9500: Loop body invariant 'sum < 2147483647 && sum > (2147483647  1) ==> sum + n == a + b' did not verify.
Verification of add#block#0 failed. [0.08]
C:\benchmarks\addmultBM2.c(28,13) : error VC8004: sum  1 might overflow.
Verification of add#block#1 failed. [0.08]
C:\benchmarks\addmultBM2.c(39,13) : error VC8004: sum + 1 might overflow.
