First "strstr()" argument "unique"?

[Olivier L'Heureux]

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".

(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>