I've slightly reworked how cpychecker tracks unknown values in
http://git.fedorahosted.org/git/?p=gcc-python-plugin.git;a=commitdiff;h=2...
For integer types, it now uses a new WithinRange abstract value,
describing the closed interval of possible values i.e.:
minvalue <= x <= maxvalue
For example, given this test case:
extern void __cpychecker_dump(int);
char array[12] = {2, 2, 2, 2, 8, 1, 8, 1, 8, 2, 8, 2};
char
test(int i)
{
__cpychecker_dump(i);
/* This ought to constrain i to within [0-255]: */
i = i & 0xff;
__cpychecker_dump(i);
/* and this ought to constrain it to within [0-7]: */
i = i >> 5;
__cpychecker_dump(i);
/* and hence this read is within the array bounds: */
return array[i];
}
we can see the values the analyzer knows about, using the "magic"
function __cpychecker_dump():
__dump((int)val [-0x80000000 <= val <= 0x7fffffff])
__dump((int)val [0 <= val <= 255])
__dump((int)val [0 <= val <= 7])
i.e. it starts by treating "i" as any possible int, but the mask against
0xff gives a new WithinRange(0, 255), and the right-shift constrains it
again.
In theory we can use this to do bounds-checking of array/buffer
accesses. I'm still working through the errors we were discussing in
the "python exceptions from refcount checker" thread, so I'm holding off
on implementing that yet.
I ran into this when compiling a fragment of code similar to the above
in gdb; the difference there is that the array was a local, initialized
within the function scope. cpychecker was complaining that the array
access was a read of an uninitialized value, since it wasn't able to
prove that "i" was within the bounds. Unfortunately, even with this
fix, it still complains, since it isn't smart enough to know that all
possible indices have an initialized value, and picks the "default"
value for the array, which is "uninitialized". Hopefully I can fix that
case too.
Dave