[splint-discuss] How does splint check a pointer to constant

[Tommy Pettersson]

On Tue, Mar 06, 2007 at 12:52:13PM -0300, Jorge Peixoto de Morais Neto wrote:
> #include <stdlib.h>
> int main(void){
> 
>  /*@unused@*/  const char *p="a";
>  /*@unused@*/ char *x=p;
>  return EXIT_SUCCESS;
> }
[...]
> #include <stdlib.h>
> int main(void){
>  /*@unused@*/ char const * const teststringarray[]={"a"};
>  return EXIT_SUCCESS;
> }
[...]
> The behavior in the program is bugging me (I have similar case in a real
> program). Why does this happen? There is nothing wrong or suspect in
> initializing with a string literal an array of const pointers to constants
> (const * const) How can I fix this? In the manual, I only found something
> about /*@observer@*/, but this seems absurd, since I am not dealing with an
> abstract type.

splint is ignorant about the const declaration, so an extra
/*@observer@*/ is unfortunately required.

I'm not sure about the second example, but I think it could have
to do with the "inner storage" thing. In the first example I
think splint automatically detects that p is an /*@observer@*/
since it is assigned a string literal. But apparently not in the
second example. A problem is that there is no easy way to tell
splint what the pointers "inside" the array are. Here is how to
work around it:

  typedef /*@observer@*/ char * const_char_ptr_t;
  const_char_ptr_t teststringarray[] = { "a" };


-- 
Tommy Pettersson <ptp at lysator.liu.se>