[splint-discuss] /*@null@*/ array elements

[Brian Quinlan]

On Sun, 2007-06-24 at 22:28 +0200, Kozics Péter wrote:
> I couldn't figure out myself and could not find any hint in the splint 
> manual how to annotate array elements to be /*@null@*/.
> 
> I would like to get rid of the warning
> 
> redef.c:5:20: Local a[0][0] initialized to null value: a[0][0] = 0
>   A reference with no null annotation is assigned or initialized to NULL.
> 
> for the following code.
> 
> 
> int *f( void )
> {
>   int *a[2][3] = {{0}};
>  
>   return a[1][1];
> }
> 
> 
> When I naively annotate the array with /*@null@*/., it seems that I make 
> statement about ``a'' and not about its elements which are of type int 
> *, and which the the warning refers to.
> 
Hi Peter,
It's not perfect, because it involves a change to your coding style, but
you could try using an annotated typedef in the array:


typedef /*@null@*/ int *IntPtr;

IntPtr f( void )
{
  IntPtr a[2][3] = {{0, 0, 0}, {0, 0, 0}};

  return a[1][1];
}

There's still a warning to fix in this modified code, but it's not the
one about null values.

Bye,
Brian