Hi Ralf,

Sorry for the delay.

The reason you are getting this warning is that

    /*@modifies err@*/

means it may modify the object referenced by err, whereas

   /*@modifies *err@*/

means it may modify the object referenced by *err, that is err[0].

Note that if the body of f did,

        *err[0] = 'f';

you would get warnings in both cases.

Hope that helps,

--- Dave

On Thu, 10 Jan 2002, Ralf Wildenhues wrote:

> Considering this code fragment, I do not understand the way
> lclint/splint expects the annotations:
>
> --- foo.c ---
> /*@-exportlocal -exportheader -fcnuse@*/
>
> typedef /*@observer@*/ const char *litstring;
>
> void f(int a, litstring *err)
>   /*@modifies *err@*/
> {
>   if (a==1) {
>     *err = "fubar";
>   }
> }
>
> void g(int x) /*@*/
> {
>   litstring error = "default";
>   if (x != 0) {
>     f(42, &error);
>   }
> }
> ---
>
> As a result I get
>
> splint -strict foo.c
> Splint 3.0.1 --- 09 Jan 2002
>
> foo.c: (in function g)
> foo.c:17:5: Suspect modification of observer error: f(42, &error)
>   Storage declared with observer is possibly modified. Observer storage may not
>   be modified. (Use -modobserver to inhibit warning)
>
> Finished checking --- 1 code warning
>
> But after changing the modifies clause of f to
>   /*@modifies error@*/
> splint reports no more errors.  But f really does modify *error.  How
> can I tell it so and possibly not get the other code warning?  Is there
> a way besides the flag -modobserver?
>
> Thanks,
> Ralf
>


Reply via email to