Casting seems to change the tracking of /*@out@*/ parameters.
The following code gives gives the warning below, but without the cast to char* , there is no warning, despite the cast being completely valid.
Code:
int func2( /*@out@*/ char *bytes );
void func1(/*@out@*/ void *buf)
{
(void) func2( (char*)buf );
}
Output:
Splint 3.1.2 --- 15 Feb 2009
../../webkit/hp_1.2/tools/usbhp/bcm2727dkb0rev2/linux/testsplint.c: (in function func1)
../../webkit/hp_1.2/tools/usbhp/bcm2727dkb0rev2/linux/testsplint.c:6:2:
Out storage buf 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
Copy of source code