#53 Casting breaks tracking of /*@out@*/ parameters

[Anonymous]

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

[Nobody/Anonymous]

Copy of source code