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>
