Bill Pringlemeir wrote:
> On 13 Oct 2009, michael.woj...@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.
Hi
Yes, ?'ve seen that. The problem, from my point of view, is that there
is no clear separation of the definition itself and an further
explanation/discussion of the definition. This is what complicates
things. Then, the Appendix text simply broadens the confusion.
Also, I think that, in the text, the usage of "usable/accessible" might
be more appropriate than null, since null is one case of not usable. And
also an explanation of "usable", similar to the one you provided.
>>> 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.
Ok this is clear things now.
> *OR*
>
> If result is TRUE, first parameter is not accessible.
With your explanation of the go/no-go functions, this it totally clear
too. True indicates that the first parameter is not-accessible for
implementation specific reasons (not the correct type or whatever).
Thank you both for both your time and your detailed explanations,
Vangelis Katsikaros
>>> 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).
_______________________________________________
splint-discuss mailing list
splint-discuss@mail.cs.virginia.edu
http://www.cs.virginia.edu/mailman/listinfo/splint-discuss
