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>