
Hi all,
I'm trying to play a little bit with VCC (right now I stick to very basic cases).
It was successfully able to verify the following program:
#define MIN(a, b) (((a) < (b)) ? (a) : (b))
#define MAX(a, b) (((a) > (b)) ? (a) : (b))
unsigned int midvalue(unsigned int a, unsigned int b, unsigned int c)
requires(a != b && a != c && b != c)
ensures(MIN(MIN(a, b), c) < result < MAX(MAX(a, b), c))
{
return MIN(MIN(MAX(a, b), MAX(b, c)), MAX(a, c));
}
However, for some reason, if I drop the "unsigned" restriction, it does not verify anymore.
Any idea why ? I did not extensively test this basic case but it seems correct to me, even without the "unsigned".
Many thanks,
Regards,
Dinesh Bolkensteyn


Editor
Mar 21, 2010 at 8:17 AM

Hi Dinesh,
Like all sound verifiers, VCC is incomplete: some valid programs will fail to verify. In your case, the formula you are asking it to prove:
MIN(MIN(a, b), c) < MIN(MIN(MAX(a, b), MAX(b, c)), MAX(a, c)) < MAX(MAX(a, b), c)
is a bit too complex. In the case of unsigned integers, it can make the simplifying assumption that a, b and c are positive. When you work with signed integers, the full complexity of the formula appears, and VCC (or Z3) simply can't handle it.
Although I can't give you an indepth explanation of why the proof fails, i can give you a simple way of making it go through: if you break your formula into two simpler formulas, the verification succeeds again, even in the signed case.
int midvalue(int a, int b, int c)
requires(a != b && a != c && b != c)
ensures(MIN(MIN(a, b), c) < result && result < MAX(MAX(a, b), c))
{
return MIN(MIN(MAX(a, b), MAX(b, c)), MAX(a, c));
}
#define MIN(a, b) (((a) < (b)) ? (a) : (b))
#define MAX(a, b) (((a) > (b)) ? (a) : (b))
int midvalue(int a, int b, int c)
requires(a != b && a != c && b != c)
ensures(MIN(MIN(a, b), c) < result && result < MAX(MAX(a, b), c))
{
return MIN(MIN(MAX(a, b), MAX(b, c)), MAX(a, c));
}
In general, if something you believe is true fails to verify, try to simplify the manipulated formulas; it usually helps a lot.
Cheers,
Francois


Coordinator
Mar 24, 2010 at 1:19 PM
Edited Mar 24, 2010 at 1:23 PM

Hi Dinesh, Francois,
in C, 'a < b <c' and 'a < b && b < c' are two semantically different expressions. In C, 'a < b < c' in C roughly corresponds to ((int)((bool)(a < b))) < c; in other words, you are comparing the boolean result of 'a < b'
with c; for unsigned values, the resulting expression is true whereas of signed integers, where the MAX could be negative, this is not the case. Indeed, the counter example has exactly such values:
a > 2147483022:int
b > 3774:int
c > 2147483023:int
If you fix your example and write MIN(MIN(a, b), c) < result && result < MAX(MAX(a, b), c)), as Francois suggested, then VCC verifies your code. Not because the code is now simpler, but because the code is now correct.


Coordinator
Mar 25, 2010 at 10:05 AM

Let me add that with increased warning level (giving /w:2 as a commandline option), VCC produces a warning for the original code hinting at the potential problem:
d:\viridian_mah\vmhv\dinsoft.c(8,12) : warning VC9003: '((((((a) < (b)) ? (a) :
(b))) < (c)) ? ((((a) < (b)) ? (a) : (b))) : (c)) < result < ((((((a) > (b)) ? (
a) : (b))) > (c)) ? ((((a) > (b)) ? (a) : (b))) : (c))' probably does not expres
s what you intended; use two conjoined conditions to express an interval or pare
nthesize the left comparison.
warning VC9003: '((((((a) < (b)) ? (a) : (b))) < (c)) ? ((((a) < (b)) ? (a) : (b))) : (c)) < result < ((((((a) > (b)) ? (a) : (b))) > (c)) ? ((((a) > (b)) ? (a) : (b))) : (c))' probably does not express what you intended;
use two conjoined conditions to express an interval or parenthesize the left comparison.
Best, Mark

