[splint-discuss] nullwhentrue explained

[Bill Pringlemeir]

On 13 Oct 2009, Michael.Wojcik at microfocus.com wrote:

>> Vangelis Katsikaros Wrote:
>> Sent: Tuesday, 13 October, 2009 15:37

>> I think that the confusion started from the manual 2.1.1 where it says:
>> "If a function annotated with nullwhentrue returns true it means
>> its first passed parameter is NULL"

Ah, but I think you should always read a whole paragraph.

   If a function annotated with nullwhentrue returns true it means its
   first passed parameter is NULL.  If it returns false, the parameter
   is not NULL. Note that it may return true for a parameter that is
   not NULL. A more descriptive name for nullwhentrue would be "if the
   result is false, the parameter was not null".

The "more descriptive name" is the correct description.  The use of
'NULL' is also confusing.  Really 'NULL' denotes that splint will emit
an error if this value is used.

>> and in Appendix C:
>> "nullwhentrue
>> If result is true, first parameter is NULL."

It should be as the "falsewhennull" description,

  If result is FALSE, first parameter is not NULL.

*OR*

  If result is TRUE, first parameter is not accessible.

>> If this is the case, then I think that the text in the manual is
>> confusing and not the name of the annotation,

> Those aren't exclusive. Both the text in the manual and the name of the
> annotation are wrong.

The annotation name is wrong/confusing from a logic/English
perspective.  The statement "returns true when null" is correct.  The
statement "null when returning true" is not.  The statement
"un-useable/not accessible when true" is the intent.  So
"truewhennull" might seem better, but "unusablewhentrue" is probably a
better annotation.  This annotation is for use of the function, versus
the implementation of the function.  The function,

	int foo(char *bar) {
	    return 1;
	}

says that bar is always un-usable.  However, the user of 'foo()' in
another module,

 void bazzle(char *bar) {
   if(foo(bar))
     /* with "truewhennull" splint knows bar illegal here.*/;
   else {
     /* fine to use bar here.*/
     printf("The bar is set to %c.\n", *bar);
   }
 }

is possibly also important.  Especially as at some point you might
decide that some type of 'bar' is worthwhile.

The whole intent of the predicate functions is that you may wish to
'refactor' error checking logic into a 'go/no-go' function.  The
predicate annotation allows splint to understand which branch of an
if/else has a valid 'bar'.  Splint does not validate the predicate
function, just the flow control of the users of 'foo()'; bazzle() in
the snippet above.  This does seem clear to me if I read the whole
section 2.1.1.  The appendix does not stand well by itself; if you
start in the appendix you can easily get confused.

I have no access to the FAQ or the manual.  However, the mailing list
is publicly accessible.  I am inclined to leave the annotation as it
is for now (and not add another variant).

Fwiw,
Bill Pringlemeir.

-- 
Washing one's hands of the conflict between the powerful and the
powerless means to side with the powerful, not to be neutral. - Freire