[splint-discuss] staticinittrans

[Brian Quinlan]

On Thu, 2009-04-23 at 19:24 +0100, Jonathan and Caroline Moore wrote:
> Splint is a wonderful tool but I could use some help with a few last
> +checks warnings in a project.
> 
> Please go easy on me I'm not CompSci just an engineer trying to make
> sure the compiler is forced to do what I intend.
> 
> I don't understand the unqualified static, implicitly and inconsistent
> way parts of the splint warning.
> 
Hi Jonathan,

implicitly only - the x field in the struct is a pointer, which means
splint implicitly sets it as /*@only@*/ storage. Unless you explicitly
annotate it to be some other storage type, then splint will issue a
warning if another variable has a reference to the same memory. Clearly
x and stL.x both point to the same memory, so splint complains about
this.

I'm not sure about the meaning of unqualified storage and inconsistent,
but I expect that if you choose the right annotation (only, dependent,
owned, etc.) for the source and destination when you're assigning the
pointer value, then the problem will go away.

The following makes the warning go away, but only you'll know if the
dependent annotation is reasonable for your application:

typedef struct {
  /*@dependent@*/int *x;
} stL_t;


Bye,
Brian

> Google hasn't helped either - just people saying use -staticinittrans
> or other code markup which I feel defeats the point of trying to
> understand WHY the static analysis is complaining.
> 
> How do I get around this or initialise a pointer in a struct in a way
> that splint likes. Everything I've tried seems to generate an error
> similar to these below or warnings about losing memory pointers
> without deallocating them
> 
> Deep thanks in advance.
> 
> Jonathan
> 
> P.S. I'd appreciate a cc on any replies - not sure I got the mailer
> set up right.
> 
> WS867:Thu 23:1845:~:$ cat test.c
> #include <stdio.h>
> 
> typedef struct {
>        int *x;
> } stL_t;
> 
> static int x[2] = {5, 10};
> 
> static stL_t stL = {
>        x
> };
> 
> 
> int main(int argc, char *argv[]) {
>        printf("%s\n", argv[argc - 1]);
>        printf("%d\n", stL.x[0]);
>        return 0;
> }
> WS867:Thu 23:1845:~:$ gcc -Wall -Wextra -o test test.c
> WS867:Thu 23:1845:~:$ ./test
> ./test
> 5
> WS867:Thu 23:1845:~:$ splint +checks test.c
> Splint 3.1.2 --- 07 May 2008
> 
> test.c:10:2: Unqualified static storage x used as initial value for implicitly
>                only: stL.x = x
>  Static storage is used as an initial value in an inconsistent way. (Use
>  -staticinittrans to inhibit warning)
> 
> Finished checking --- 1 code warning
>