[splint-discuss] undefined field in my storage

[Bertrand Mollinier Toublet]

Hi all,

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 ?

Bertrand