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 >