[splint-discuss] Annoying False Positives

[Tommy Pettersson]

On Thu, Sep 14, 2006 at 10:49:07PM -0500, Felipe Contreras wrote:
> I have stumbled upon a lot of false positive errors with splint.
> 
> Here is the one that bothers me the most (attached).
> 
> Am I doing something wrong?

You did not say with what options you are running splint, but
here's the output I get from splint with no extra options:

  Splint 3.1.1 --- 20 Jul 2006
  
  f.c: (in function my_test_new)
  f.c:23: Only storage test->data (type void *) not released before assignment:
             test->data = malloc(100)
    A memory leak has been detected. Only-qualified storage is not released
    before the last reference to it is lost. (Use -mustfreeonly to inhibit
    warning)
  f.c:25: Returned storage *test contains 1 undefined field: data
    Storage derivable from a parameter, return value or global is not defined.
    Use /*@out@*/ to denote passed or returned storage which need not be defined.
    (Use -compdef to inhibit warning)
  
  Finished checking --- 2 code warnings


The first warning is annoying, I agree, but as most of the time,
splint is buggingly correct. The call to memset gives test->data
a value of all zero bits. What that value means is architecture
dependent and not guaranteed to be a NULL pointer. This means
among other things that tests like "if (!test->data)" are
equally undefined until the pointer gets a proper value. Your
code give test->data a proper value right away, and it's obvious
from looking at the code that it always works as expected. But
splint does not "understand" code and can of course not see
that.

I don't know if maybe splint should be extended to keep track of
values with undefined behavior. It is clearly wrong to free a
pointer after setting its value with memset, but the code

  memset (test, 0, sizeof (test));
  free (test->data);

does NOT produce a warning from splint! (even in strict mode.)


After a memset (foo, 0, ...) you can put lines like:

  /*@-mustfreeonly@*/
  foo->ptr1 = 0;
  foo->ptr2 = init2;
  ..
  /*@=mustfreeonly@*/



The second warning you get is also correct. me_test_new does
(possibly) return reachable undefined storage. The returned
pointer points to a struct with a pointer to newly malloced but
not initialized memory, and it would be wrong to read that
memory. Splint does much of its checking per function, and in
this case you need to put a partial annotation on the functions
return value, so splint can generate correct warnings for
functions that call me_test_new.

  /*@null@*/ /*@partial@*/ static MyTest * my_test_new (void) { ...

There are also more advanced special annotations to specify in
detail what fields of a struct get allocated, freed, initialized
and so on by a function.


-- 
Tommy Pettersson <ptp at lysator.liu.se>