Here is the lemma that helps:
_(ghost _(pure) bool lemma(\integer a, \integer b, \integer i)
_(requires a * b < INT_MAX)
_(requires a >= 0 && i < b)
_(ensures a * i + a < INT_MAX)
_(returns \true)
{
_(assert i + 1 <= b)
_(assert a * (i + 1) <= a * b)
return \true;
})
Verify this function by VCC using the command line switch "/oaf" that lets VCC treat the multiplication symbolically.
With the help of this lemma, your above function can be verified (with or without the "/oaf" option) after you insert the following line as the first statement in the loop body, directly before incrementing your variable "ret":
_(assert lemma(termA, termB, i))
By the way, it your precondition is probably weaker than what you intended. You might have meant something like:
_(requires a >= 0 && b >= 0 && ((\integer) a) * ((\integer) b) < (\integer) INT_MAX)
Note that your condition "a * b < INT_MAX" holds for nearly all "a" and "b" due to integer overflow ("a * b <= INT_MAX" should be true for all integers "a" and "b").
