[splint-discuss] Bounds checking quirk

[Paul Bartosek]

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(/*@out@*/ unsigned char *failures)

            /*@requires maxSet(failures) >= 0@*/

{

            *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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.cs.virginia.edu/pipermail/splint-discuss/attachments/20080626/ddf102a0/attachment-0001.html