[splint-discuss] nullwhentrue explained

[Bill Pringlemeir]

On 10 Oct 2009, ibob17 at yahoo.gr wrote:

> I am new to splint and I would like to ask a question about nullwhentrue.
>
> In "2.1.1 Predicate Functions" it says
>
> "If a function annotated with nullwhentrue returns true it means its
> first passed parameter is NULL. [1] If it returns false, the parameter 
> is not NULL. [2]  Note that it may return true for a parameter that is 
> not NULL. [3]  ..."
>
> Then in "Appendix C Annotations" it says:
>
> "nullwhentrue
> If result is true, first parameter is NULL." [4]
>
> So I am confused since I read that
>
> i) result true => first parameter is NULL [1], [4]
> ii) result false => first parameter is not NULL [2]
> iii) result true => (first?) parameter could be not NULL [3]
>
> I see a contradiction between i and iii, unless I haven't understood
> correctly or I miss something obvious.
>
> Is it
> result true => first parameter is whatever
> result false => first parameter is not NULL
> ?

The intent is that the function annotated with this returns a
'go/no-go' status.  Ie, there is some error or something wrong.  Some
code used a magic cookie to denote a type.

struct foo {
 int magic; /* always 0x12348765 for foo struct */
...
}

static /*@nullwhentrue@*/ bool checkFoo (/*@temp@*/ foo * _foo);

The part [3] means that true may be returned if the 'magic' value is
not as denoted.  Some psuedo-code might be like this,

bar * foo_to_bar(/*@null@*/ foo *_foo)
{
 if(checkFoo(_foo)) return barRoot;
 return newBar(_foo);
}

Ie, some default value is returned on either NULL or if the foo does
not seem to be valid.

/* Please don't comment on where this is a correct thing to do in your
nuclear reactor control system.  */
static bool checkFoo (foo * _foo)
{ 
  if(foo && foo->magic == 0x12348765)
      return TRUE;
  return FALSE;
}

So there is no 'assertion' about 'i)'.  If the result is true, it
doesn't *ensure* that arguement one was NULL.  However, if argument
one was NULL, then the return value is true.  So, code that initially
has a potential NULL value will be not NULL for the false case (ie
case ii is correct).  If a function annotated with this returns true,
then the first parameter should not be used in that code path
afterwards.  For the false case, a possibly 'null' value is not longer
possibly 'null' but is known to be good (non-null).

fwiw,
Bill Pringlemeir.

-- 
``C Code. C code run. Run, code, run... PLEASE!!!'' 
- Barbara Tongue