X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/898d4ae5dd7550dda57d426d1c0de6dd251fbd7d..11c40ce9ae842585926cc1abd029f9f5a6702827:/lib/standard.h diff --git a/lib/standard.h b/lib/standard.h index ee6185f..7e2288b 100644 --- a/lib/standard.h +++ b/lib/standard.h @@ -1142,9 +1142,10 @@ time_t time (/*@null@*/ /*@out@*/ time_t *tp) /*@observer@*/ char *ctime (time_t *tp) /*@*/ /*@ensures maxSet(result) == 25 /\ maxRead(result) == 25; @*/; -/*@null@*/ /*@observer@*/ struct tm *gmtime (time_t *tp) /*@*/ ; +/* 2003-11-01: remove null annotation: gmtima and localtime cannot return null */ +/*@observer@*/ struct tm *gmtime (time_t *tp) /*@*/ ; -/*@null@*/ /*@observer@*/ struct tm *localtime (time_t *tp) +/*@observer@*/ struct tm *localtime (time_t *tp) /*@modifies errno@*/ ; size_t strftime (/*@out@*/ char *s, size_t smax,