[splint-discuss] undefined field in my storage

[CBFalconer]

David Evans wrote:
> On Wed, 18 Dec 2002, Bertrand Mollinier Toublet wrote:
> 
> > I am a new user of Splint, and of course already ran into my first
> > puzzling issue. From a rapid browse of the list archive, it seems that
> > it is ok to post such issue here. However, if it is *not* ok, please let
> > me know. My issue is related to the following tiny bit of code:
> >
> > #include <stdlib.h>
> >
> > struct node
> > {
> >     size_t nchildren;
> >     /*@relnull@*/ struct node **children;
> > };
> >
> > static /*@null@*/ struct node *alloc_node(unsigned int, size_t);
> >
> > struct node *alloc_node(size_t nchildren)
> > {
> >     struct node *node;
> >     size_t i;
> >
> >     node = malloc(sizeof *node);
> >     if (NULL == node) return NULL;
> >
> >     node->nchildren = nchildren;
> >     if (0 == nchildren)
> >     {
> >         node->children = NULL;
> >     }
> >     else
> >     {
> >         node->children = malloc(nchildren * sizeof *node->children);
> >         if (NULL == node->children)
> >         {
> >             free(node);
> >             return NULL;
> >         }
> >         for (i = 0; i < nchildren; ++i)
> >         {
> >             node->children[i] = NULL;
> >         }
> >     }
> >     return node;
> > }
> >
> > The idea is to allocate storage for a single node of a tree with a
> > variable number of children per node. The function tries to allocate
> > storage for the struct itself, and returns NULL if it fails. It then
> > goes on allocating storage for the list of children with the following
> > rules:
> >   - if the number of children passed to the function is zero, it is
> > indicated by setting the list to NULL
> >   - else, storage is allocated for enough pointers to the children
> > (de-allocating node and returning NULL is case of malloc failure), and
> > all the children are initialized to NULL (I want them to be set later).
> >
> > Now my problem: Splint complains that when returning node, at the last
> > return, the field children is undefined. Here comes the full message:
> >
> > test.c(37,12): Returned storage *node contains 1 undefined field:
> > children
> >   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)
> >
> > It seems to me that node->children is fully defined, either as a NULL
> > pointer if nchildren==0, or as an array of NULL pointer in the opposite
> > case, except if the storage allocation failed, in which case, a NULL
> > pointer is returned.
> >
> > In other words, I do not understand how Splint is able to see the
> > children field as being undefined.
> >
> > Anyone willing to clarify things for me, please ?
> 
> The reason splint is reporting a warning about node perhaps not being
> completely defined at line 37, is that it cannot determine that the
> body of the loop which initializes it with node->children[i] = NULL
> actually executes.  (A deeper analysis would be able to determine this
> because the else only executes when nchildren > 0, but splint's analyses
> are not deep enough to determine that.)
> 
> The way to elimintate the warning is to add a syntactic comment that
> indicates that the loop body always executes:
> 
>         /*@+forloopexec@*/
>         for (i = 0; i < nchildren; ++i)
>         {
>             node->children[i] = NULL;
>         }
>         /*@=forloopexec@*/
> 
> If you're less paranoid, you could just add +loopexec to the command line
> which would make splint assume all loop bodies are executed.

Let me suggest the following modification to your code, as being
both clearer and possibly more understandable to splint:

/* pasted as quote to avoid line breaks */

> #include <stdlib.h>
> 
> struct node {
>    size_t        nchildren;
>    struct node **children;
> };
> 
> struct node *alloc_node(size_t nchildren)
> {
>    struct node *node;
>    size_t       i;
> 
>    if (NULL != (node = malloc(sizeof *node))) {
>       node->nchildren = nchildren;
>       if (0 == nchildren) node->children = NULL;
>       else {
>          node->children = malloc(nchildren * sizeof *node->children);
>          if (NULL != node->children)
>             for (i = 0; i < nchildren; ++i) node->children[i] = NULL;
>          else {
>             free(node);
>             node = NULL;
>          }
>       }
>    }
>    return node;
> }

at least IMNSHO :-)  No 'peculiar' comments needed, single exit
point, etc.  Now I get:

> [1] c:\c\junk>splint tsplint1.c
> Splint 3.0.1.6 --- 11 Feb 2002
> 
> tsplint1.c: (in function alloc_node)
> tsplint1.c(26,12): Possibly null storage node returned as non-null: node
>   Function returns a possibly null pointer, but is not declared using
>   /*@null@*/ annotation of result.  If function may return NULL, add /*@null@*/
>   annotation to the return value declaration. (Use -nullret to inhibit warning)
>    tsplint1.c(13,25): Storage node may become null
> tsplint1.c(26,12): Returned storage *node contains 2 undefined fields:
>                       nchildren, children
>   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

PS: why doesn't the list include a reply-to field in the header? 
That would avoid many nuisance direct emails.

-- 
Chuck F (cbfalconer at yahoo.com) (cbfalconer at worldnet.att.net)
   Available for consulting/temporary embedded and systems.
   <http://cbfalconer.home.att.net>  USE worldnet address!