Hi all, I've been fighting with splint for a little while over this and
I'm not getting anywhere. I've boiled down the error to a pretty simple
example here that works, is glaringly obvious but splint still claims
there's a possible out of bounds store operation. Any ideas on how to
get splint to recognize that maxSet(count) is actually 0?
Here's the code:
void Get_Fail_Count(/[EMAIL PROTECTED]@*/ unsigned char *failures)
/[EMAIL PROTECTED] maxSet(failures) >= [EMAIL PROTECTED]/
{
*failures = 20;
}
void my_other_func()
{
unsigned char count;
Get_Fail_Count(&count);
}
And here is the error:
$ splint test.c +bounds +charint -exportlocal
Splint 3.1.1 --- 09 Aug 2007
test.c: (in function my_other_func)
test.c:13:2: Possible out-of-bounds store:
Get_Fail_Count(&count)
Unable to resolve constraint:
requires maxSet(&count @ test.c:13:17) >= 0
needed to satisfy precondition:
requires maxSet(&count @ test.c:13:17) >= 0
derived from Get_Fail_Count precondition:
requires maxSet(<parameter 1>) >= 0
A memory write may write to an address beyond the allocated buffer.
(Use
-boundswrite to inhibit warning)
Finished checking --- 1 code warning
Paul B.
_______________________________________________
splint-discuss mailing list
splint-discuss@mail.cs.virginia.edu
http://www.cs.virginia.edu/mailman/listinfo/splint-discuss
