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?
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?
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
