Hi Enrico,
On 2 Jul 2002, Enrico Scholz wrote:
> Hello,
>
> I try to find an annotation for the recvmsg() function, but had only little
> success in it. The program below is a simplified version demonstrating my
> problems.
>
> The main issue is the non-detected definition of the 'ptr' parameter of
> bar() by the foo() function. I hoped that the @define@ clause in line 29
> tells that the 'ptr'-members of *all* 'msg->vec' fields will be defined
> by foo(), but splint ignores it :(
>
> Are my annotations wrong and/or can they be extended so that the warning
> disappear?
>
>
> When using foo1() by uncommenting line 53 things are fine and the warning
> go away. When using foo1() in line 54 instead of, the warning reappear,
> so splint seems to be unable to conclude the definition-state if arrays
> are involved. Can I add annotations to help splint here?
>
You're running into the limits of the analysis here, unfortunately. There
is no way to add annotations to make this work. Splint's alias analysis
isn't sophisticated enough to track all aliases through array elements for
this, so it is unable to conclude that ptr is defined. Other than
simplifying the code to make the analysis work, you can use
extern void assertDefined (/*@out@*/ /*@sef@*/ /*@unused@*/ void *p_x) ;
/*@-mustdefine@*/
# define assertDefined(x) ;
/*@=mustdefine@*/
...
foo (&msg);
assertDefined (ptr);
to suppress the warning. (This assumes +allmacros is used to prevent
expansion of assertSet.)
>
> The explicit @temp@-storage annotations in line 5 and 12 are another
> issue. When not using them, a lot of warnings regarding bad storage
> transfer appear. It is not a problem to add fitting
> storage-specifications in the example but when using the shipped unix.h
> library annotations, the @only@ storage is assumed for 'struct iovec'
> and 'struct msghdr'.
>
> IMO this implicit @only@-storage is wrong for the iovec and msghdr
> structures and should be fixed in lib/unix.h. Does there exists a way
> to change the storage of members at the declaration of variables?
>
You're right that the library should be fixed (it is now in CVS, and the
next release). You can fix this by making the change and remaking the
libraries (make in libs/ directory); or you can override the library
declaration with your own declaration in your source files.
--- Dave
>
>
> Enrico
>
> ----
> 1 #include <stdlib.h>
> 2
> 3 struct Iovec
> 4 {
> 5 /*@temp@*/
> 6 void *ptr;
> 7 size_t len;
> 8 };
> 9
> 10 struct Msg
> 11 {
> 12 /*@temp@*/
> 13 struct Iovec *vec;
> 14 size_t len;
> 15 };
> 16
> 17 static void /*@unused@*/
> 18 foo1(/*@special@*/struct Iovec *vec)
> 19 /*@modifies vec->ptr[]@*/
> 20 /*@defines vec->ptr[]@*/
> 21 /*@uses vec@*/
> 22 {
> 23 memset(vec->ptr, 0, vec->len);
> 24 }
> 25
> 26 static void
> 27 foo(/*@special@*/struct Msg *msg)
> 28 /*@modifies msg->vec->ptr[]@*/
> 29 /*@defines msg->vec->ptr[]@*/
> 30 /*@uses msg->vec, msg@*/
> 31 {
> 32 size_t i;
> 33 for (i=0; i<msg->len; ++i)
> 34 memset(msg->vec[i].ptr, 0, msg->vec[i].len);
> 35 }
> 36
> 37 static void
> 38 bar(/*@out@*/void *ptr, size_t len)
> 39 /*@modifies *ptr@*/
> 40 {
> 41 /*@temp@*/struct Iovec iov[1], vec;
> 42 /*@temp@*/struct Msg msg;
> 43
> 44 iov[0].ptr = ptr;
> 45 iov[0].len = len;
> 46 msg.vec = iov;
> 47 msg.len = 1;
> 48
> 49 vec.ptr = ptr;
> 50 vec.len = len;
> 51
> 52 foo(&msg);
> 53 //foo1(&vec);
> 54 //foo1(iov);
> 55 }
> 56
> 57 int main()
> 58 {
> 59 char buf[1024];
> 60
> 61 bar(buf, sizeof buf);
> 62 return 0;
> 63 }
> ----
>
> | $ splint gath.c
> | Splint 3.0.1.6 --- 17 Jun 2002
> |
> | gath.c: (in function bar)
> | gath.c:55:2: Out storage ptr not defined before return
> | An out parameter or global is not defined before control is transferred. (Use
> | -mustdefine to inhibit warning)
> |
> | Finished checking --- 1 code warning
>
