Bill Pringlemeir wrote:
> On 12 Oct 2009, michael.woj...@microfocus.com wrote:
>
>>> On 10 Oct 2009, ibo...@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
_______________________________________________
splint-discuss mailing list
splint-discuss@mail.cs.virginia.edu
http://www.cs.virginia.edu/mailman/listinfo/splint-discuss
