Program won't verify due to overflow issue; invariant won't verify

Sep 22, 2013 at 6:41 PM
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.