[splint-discuss] nullwhentrue explained

[Vangelis Katsikaros]

Bill Pringlemeir wrote:
> On 12 Oct 2009, Michael.Wojcik at microfocus.com wrote:
> 
>>> On 10 Oct 2009, ibob17 at yahoo.gr wrote:
> 
>>>> I am new to splint and I would like to ask a question about
>>>> nullwhentrue.
> 
>>> 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.
> 
>> In short, the annotation is misnamed. It indicates the function returns
>> true if the first argument is null [1]. The function may return true
>> under other circumstances as well. Thus the annotation should be called
>> "truewhennull", since that's the claim it makes. "nullwhentrue" is an
>> incorrect description.
> 
>> Unfortunately, it's too late to fix it now.
> 
> If that is really the problem ("truewhennull" versus "nullwhentrue")
> it is very easy to add a new annotation.  "nullwhentrue" was
> originally named "truenull".  They all map to the same thing
> underneath, this is just an extra key to add to the parsing level.  It
> sets the 'QU_TRUENULL' qualifier to set the semantic machinery in
> either case.  I was intending to add another parser that would
> understand gcc attribute() statements (which can also be useful for
> code generation).  For the most part this is just a parsing level
> problem and the analysis algorithms are unchanged.
> 
> I don't think that is the whole problem though.  I think that
> "Predicate Functions" might better be titled "argument checkers" or
> something like that.  People versed in Lisp, Lambda calculus, etc will
> easily grok "predicate functions".  However, not everyone who uses 'C'
> would understand that nomenclature.
> 
> Probably both would be helpful, but the OP has the benefit of
> experience, so if Vangelis could tell us if he understands now and
> what the confusion was that might be helpful.
> 


Hello Bill and Michael

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"
and in Appendix C:
   "nullwhentrue
    If result is true, first parameter is NULL."

from which I derived
   if returns true => arg 1 is NULL (a)

whereas the correct one should be
   if arg 1 is NULL => returns true (b)

So, is (b) the correct one, or have I made a complete mess?

and also from what Bill said:
 >>> So, code that initially
 >>> has a potential NULL value will be not NULL for the false case (ie
 >>> case ii is correct)
 From this one I understand that (c) also stands correct for nullwhentrue.
   if returns false => arg 1 is NOT NULL (c)

So there is one implication (=>) for the nature of the argument and one 
implication for the nature of the return result.


If this is the case, then I think that the text in the manual is 
confusing and not the name of the annotation, or my lack of of Lambda 
calculus knowledge (for which BTW I have no clue, except some mentioning 
in a program analysis course).

BTW, the way I try to understand how these things work (ie by converting 
them to a => "implication") is the proper way to understand them, or 
does this l-calulus/predicates changes things somehow? Don't shoot me if 
this question sounds totally stupid :P

Thanks for your responses.
Vangelis