I'm not sure about the spurious warning on line 12.
For line 11, Splint doesn't try to detect buffer "underflow errors" like this
one.
Buffer underflow errors are not nearly as common as buffer overflow errors so
we didn't think that the additional false positives were worth the additional
checking.
> great tool, I was wondering
> if it could catch more errors.
>
> As shown by the following program, Splint doesn't seem
> to catch a negative index in an array. (On line 11)
> It generates however a spurious warning on line 12,
> where it could perhaps infer that "n" is not negative.
>
> |> 1 #include <assert.h>
> |> 2 #include <stdio.h>
> |> 3
> |> 4 int main( void )
> |> 5 {
> |> 6 unsigned int a[3] = { 17, 19, 23 };
> |> 7 const int n = 2;
> |> 8
> |> 9 if( n>=0 ) {
> |> 10 assert( n>=0 );
> |> 11 printf( "a[-2] = %u\n", a[-2] );
> |> 12 printf( "result = %d\n", 19 >> n );
> |> 13 }
> |> 14
> |> 15 return 0;
> |> 16 }
>
> #> [olheureu@WKS13 gnss 339] $ splint +boundswrite +boundsread ../tst5.c
> #> Splint 3.0.1.6 --- 27 Mar 2002
> #>
> #> tst5.c: (in function main)
> #> tst5.c:12:36: Right operand of >> may be negative (int): 19 >> n
> #> The right operand to a shift operator may be negative (behavior undefined).
> #> (Use -shiftnegative to inhibit warning)
> #>
> #> Finished checking --- 1 code warning
>
> Do somebody has a clue to let Splint report the first
> warning, and not the second?
>
> Regards,
>
> Olivier L'Heureux
> --
> Olivier L'Heureux
> Septentrio NV, Belgium
>
>
