[splint-discuss] Function interface annotations

[Hollas Boris (CR/AEY1)]

Hi,

I want to use annotations to specify the interface of a function. I want
to specify every variable that is an input to the function (except
variables passed by value; this is obvious by the parameter list) and
every variable that is output of that function (if not returned by
return()). Also, i want to specify the side-effects of the function. For
that purpose, I want to use @in@, @out@, @modifies@, @globals@
annotations.

Is this the correct approach?

I have some questions on these annotations:

/*@in@*/ int *p: Is p or *p mutable?

/*@out@*/ int *p: Does p have to be allocated? That is, if p==NULL, does
splint generate an error?
             Do I have to include *p in @modifies@?

@globals@: How do I specify that a function does not use any globals?

Regards,
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.cs.virginia.edu/pipermail/splint-discuss/attachments/20080924/78408d30/attachment.html