On Mon, 1 Jul 2002, Olivier L'Heureux wrote:
> Hello!
>
> I use Splint 3.0.1.6 on Linux and I think it is really a great
> tool. But I'm wondering why the ISO header file
> ("<install_dir>/splint/lib/standard.h:930") defines the first
> argument of "strstr()" as "unique":
>
> ||> /*@null@*/ /*@exposed@*/ char *
> ||> strstr (/*@returned@*/ /*@unique@*/ char *s, char *t) /*@*/
> ||> /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead
>(result) <= maxRead(s) /\ maxRead(result) >= 0 /\ maxRead(result) >= maxRead(t) /\
>maxSet(result) >= maxRead(t)@*/ ;
>
> AFAIK, ISO-9899 defines it as:
>
> &&> char *strstr(const char *s1, const char *s2);
>
> and not as:
>
> ##> char *strstr(const char * restrict s1, const char * restrict s2);
>
> Nothing forbids to alias the two string arguments, but they
> need to be "const".
You're right, there should be no /*@unique@*/ annotation there. I believe
its a remant from pre-ISO99 libraries that did not specify this clearly
(and may have had underfined behavior is the pointer parameters shared
storage).
Thanks for the correction,
--- DAve
>
> (BTW, there is also a typo on line 2:
> ||> ** satndard.h --- ISO C99 Standard Library for Splint.
> )
>
> Regards,
>
> Olivier L'Heureux
> --
> Olivier L'Heureux <[EMAIL PROTECTED]>
> Septentrio NV, Belgium <http://www.septentrio.com>
>
