[splint-discuss] Abstract data type annotation help

David Evans evans at cs.virginia.edu
Sun Nov 2 15:33:56 EST 2003


On Wed, 29 Oct 2003, David Hawkins wrote:

>
> Hi,
>
> Thanks Dave for the annotation suggestions yesterday.
> I've reposted the splintTest3.c code. Checking
> this code using
>
> splint +unixlib splintTest3.c
>
> Gives this one last error:
>
> splintTest3.c: (in function openHandle)
> splintTest3.c:128:11: Function returns with null storage derivable from
> global
>                          file_handle[]->base
>   A possibly null pointer is reachable from a parameter or global variable
> that
>   is not declared using a /*@null@*/ annotation. (Use -nullstate to inhibit
>   warning)
>    splintTest3.c:127:25: Storage file_handle[]->base becomes null
>
> Now, its possible that splint is confused due to the
> use of mmap here. The code checks for a valid
> return value from mmap, so there is no way that
> base will be null when assigning to file_handle[]->base.
> If this is a spurious warning, then I guess I could
> always add an if (base == NULL) test. Suggestions?
>

The problem is splint does not know that the MAP_FAILED constant is null,
so the check,

	if(base == (int *) MAP_FAILED) {
                (void)close(fd);
                return -1;
        }

isn't enough to convince splint that base is not NULL.  I don't believe
MAP_FAILED is necessarily NULL, but it is probably the case the mmap
either returns a non-NULL pointer or MAP_FAILED, so after the if we know
base is non-NULL.  To be sure, you can do assert (base != NULL) after the
if.

> There were several other errors due to the use of the
> local variable FILE_HANDLE fh in openHandle(). I added
> the annotation /*@temp@*/ - is that the correct annotation?
> My thinking for using it was that fh is a temporary
> variable, and that ownership was being passed to
> the global array. However, I thought that the
> annotation of only in the FILE_HANDLE type
> definition would have implied that the local
> FILE_HANDLE variable fh was passing ownership
> over to the global, and hence no annotation
> would be necessary. Care to comment/explain
> whats going on here?
>

I don't get any of these errors when I run splint normally, but perhaps
you are setting the -accessmodule flag to prevent the module where
FILE_HANDLE is defined from having access to its representation.  (Then,
there are many warnings about accessing the representation of
FILE_HANDLE.)

Adding the /*@temp@*/ annotation to a local variable declaration doesn't
effect this, so I'm not sure what the problem is.

--- Dave



More information about the splint-discuss mailing list