[splint-discuss] newbie question
Martin Krischik
martin at krischik.com
Sun Aug 29 02:30:24 EDT 2004
Am Sonntag, 29. August 2004 07:17 schrieb Rick Bischoff:
> Hello,
>
> I just started using splint and can't seem to figure out how to get rid
> of this error:
>
> x.c: (in function x_init)
> x.c:26:14: Passed storage X.whiteTracker contains 2 undefined fields:
> stack, tos
> Storage derivable from a parameter, return value or global is not
> defined.
> Use /*@out@*/ to denote passed or returned storage which need not be
> defined.
> (Use -compdef to inhibit warning)
>
>
> Where "X" is "typdef struct { FStack whiteTracker; /* other members */
> } XStruct;" and then "Xstruct X" inside of the "x_init" function body.
>
> The line in question is:
>
> fstack_init(&X.whiteTracker)
>
> which simply initializes the allocated structure. I tried the
> following: (fstack_init is "void fstack_init(FStack* foo);"
>
> A. add /* @out foo*/ to the function declaration in "fstack.h"
Just a hint: no space allowed between "/*" and "@" - it needs to be "/*@out".
> B. add /* @out foo*/ tot the function definition in "fstack.c"
> C. Both A & B.
> D. running "splint x.c fstack.c"
> E. running "splint fstack.c" (produces no warnings or errors)
>
> The error message just doesn't want to go away. What am I doing wrong?
>
> Rick Bischoff
>
> _______________________________________________
> splint-discuss mailing list
> splint-discuss at cs.virginia.edu
> http://www.splint.org/mailman/listinfo/splint-discuss
--
Martin Krischik
Papenkamp 33
D-30539 Hannover
Tel. 0511-5198556
mailto://Martin@krischik.com
http://www.krischik.com
More information about the splint-discuss
mailing list