/*
-** ansi.h --- LCLint Standard C Library
+** standard.h --- ISO C99 Standard Library for Splint.
**
** Process with -DSTRICT to get strict library.
*/
/*
** math.h
+**
+** evans 2002-07-03: updated from ISO C99 (http://www.vmunix.com/~gabor/c/draft.html)
*/
+typedef float float_t;
+typedef double double_t;
+
/*@constant double HUGE_VAL; @*/
+/*@constant float HUGE_VALF; @*/
+/*@constant long double HUGE_VALL; @*/
+
+/*@constant float INFINITY; @*/
+
+/*@constant float NAN; @*/
+ /*:warn implementationoptional "NAN is defined if and only if the implementation supports quiet float type NaNs.":*/ ;
+
+/*@constant int FP_INFINITE;@*/
+/*@constant int FP_NAN;@*/
+/*@constant int FP_NORMAL;@*/
+/*@constant int FP_SUBNORMAL;@*/
+/*@constant int FP_ZERO;@*/
+
+/*@constant int FP_ILOGB0;@*/
+/*@constant int FP_ILOGBNAN;@*/
+
+/*@constant int DECIMAL_DIG;@*/
+
+/* Defined for specs only - this type is any real type */
+typedef float /*@alt double, long double@*/ s_real_t;
+
+int fpclassify (/*@sef@*/ s_real_t) /*@*/ ;
+int signbit (/*@sef@*/ s_real_t) /*@*/ ;
+int isfinite (/*@sef@*/ s_real_t) /*@*/ ;
+int isnormal (/*@sef@*/ s_real_t) /*@*/ ;
+int isnan (/*@sef@*/ s_real_t) /*@*/ ;
+int isinf (/*@sef@*/ s_real_t) /*@*/ ;
/*
-** math functions that may have a range error modify errno
+** math functions that may have a range error modify errno (implementation defined).
*/
-double sin (double x) /*@*/ ;
-double cos (double x) /*@*/ ;
-double tan (double x) /*@*/ ;
-double asin (double x) /*@modifies errno@*/ ;
double acos (double x) /*@modifies errno@*/ ;
+double asin (double x) /*@modifies errno@*/ ;
double atan (double x) /*@*/ ;
double atan2 (double y, double x) /*@*/ ;
-double sinh (double x) /*@*/ ;
+
+double cos (double x) /*@*/ ;
+double sin (double x) /*@*/ ;
+double tan (double x) /*@*/ ;
+
double cosh (double x) /*@modifies errno@*/ ;
+double sinh (double x) /*@modifies errno@*/ ;
double tanh (double x) /*@*/ ;
+double acosh (double x) /*@modifies errno@*/ ;
+double asinh (double x) /*@modifies errno@*/ ;
+double atanh (double x) /*@modifies errno@*/ ;
+
double exp (double x) /*@modifies errno@*/ ;
-double ldexp (double x, int n) /*@modifies errno@*/ ;
double frexp (double x, /*@out@*/ int *xp) /*@modifies *xp;@*/ ;
+double ldexp (double x, int n) /*@modifies errno@*/ ;
double log (double x) /*@modifies errno@*/ ;
double log10 (double x) /*@modifies errno@*/ ;
+double modf (double x, /*@out@*/ double *ip) /*@modifies *ip;@*/ ;
+
+double exp2 (double x) /*@modifies errno@*/ ;
+double expm1 (double x) /*@modifies errno@*/ ;
+double log1p (double x) /*@modifies errno@*/ ;
+double log2 (double x) /*@modifies errno@*/ ;
+double logb (double x) /*@modifies errno@*/ ;
+
+double scalbn (double x, int n) /*@modifies errno@*/ ;
+double scalbln (double x, long int n) /*@modifies errno@*/ ;
+long double scalblnl(long double x, long int n) /*@modifies errno@*/ ;
+
+int ilogb (double x) /*@modifies errno@*/ ;
+int ilogbf (float x) /*@modifies errno@*/ ;
+int ilogbl (long double x) /*@modifies errno@*/ ;
+
+double fabs (double x) /*@*/ ;
+float fabsf (float x) /*@*/ ;
+long double fabsl (long double x) /*@*/ ;
+
double pow (double x, double y) /*@modifies errno@*/ ;
+float powf(float x, float y) /*@modifies errno@*/ ;
+long double powl(long double x, long double y) /*@modifies errno@*/ ;
+
double sqrt (double x) /*@modifies errno@*/ ;
+float sqrtf(float x) /*@modifies errno@*/ ;
+long double sqrtl (long double x) /*@modifies errno@*/ ;
+
+double cbrt (double x) /*@*/ ;
+float cbrtf (float x) /*@*/ ;
+long double cbrtl (long double x) /*@*/ ;
+
+double hypot (double x, double y) /*@modifies errno@*/ ;
+float hypotf (float x, float y) /*@modifies errno@*/ ;
+long double hypotl (long double x, long double y) /*@modifies errno@*/ ;
+
+double erf (double x) /*@*/ ;
+double erfc (double x) /*@*/ ;
+float erff (float x) /*@*/ ;
+long double erfl (long double x) /*@*/ ;
+float erfcf (float x) /*@*/ ;
+long double erfcl (long double x) /*@*/ ;
+
+double gamma (double x) /*@modifies errno@*/ ;
+float gammaf(float x) /*@modifies errno@*/ ;
+long double gammal (long double x) /*@modifies errno@*/ ;
+double lgamma (double x) /*@modifies errno@*/ ;
+float lgammaf (float x) /*@modifies errno@*/ ;
+long double lgammal (long double x) /*@modifies errno@*/ ;
double ceil (double x) /*@*/ ;
+float ceilf(float x) /*@*/ ;
+long double ceill(long double x) /*@*/ ;
+
double floor (double x) /*@*/ ;
-double fabs (double x) /*@*/ ;
+float floorf (float x) /*@*/ ;
+long double floorl (long double x) /*@*/ ;
-double modf (double x, /*@out@*/ double *ip) /*@modifies *ip;@*/ ;
+double nearbyint (double x) /*@*/ ;
+float nearbyintf (float x) /*@*/ ;
+long double nearbyintl (long double x) /*@*/ ;
+
+double rint (double x) /*@*/;
+float rintf (float x) /*@*/ ;
+long double rintl (long double x) /*@*/ ;
+long int lrint (double x) /*@modifies errno@*/ ;
+long int lrintf (float x) /*@modifies errno@*/ ;
+long int lrintl (long double x) /*@modifies errno@*/ ;
+long long llrint (double x) /*@modifies errno@*/ ;
+long long llrintf(float x) /*@modifies errno@*/ ;
+long long llrintl(long double x) /*@modifies errno@*/ ;
+
+double round (double x) /*@*/ ;
+long int lround (double x) /*@modifies errno@*/ ;
+long long llround (double x) /*@modifies errno@*/ ;
+
+double trunc (double x) /*@*/ ;
double fmod (double x, double y) /*@*/ ;
+double remainder (double x, double y) /*@*/ ;
+double remquo (double x, double y, /*@out@*/ int *quo) /*@modifies *quo@*/ ;
+double copysign (double x, double y) /*@*/ ;
+double nan (/*@nullterminated@*/ const char *tagp) /*@*/ ;
+double nextafter (double x, double y) /*@*/ ;
+double nextafterx (double x, long double y) /*@*/ ;
+
+double fdim (double x, double y) /*@modifies errno@*/ ;
+double fmax (double x, double y) /*@*/ ;
+double fmin (double x, double y) /*@*/ ;
+double fma (double x, double y, double z) /*@*/ ;
+
+int isgreater (s_real_t x, s_real_t y) /*@*/ ;
+int isgreaterequal (s_real_t x, s_real_t y) /*@*/ ;
+int isless (s_real_t x, s_real_t y) /*@*/ ;
+int islessequal (s_real_t x, s_real_t y) /*@*/ ;
+int islessgreater (s_real_t x, s_real_t y) /*@*/ ;
+int isunordered (s_real_t x, s_real_t y) /*@*/ ;
/*
** These functions are optional in iso C. An implementation does not
typedef /*@abstract@*/ /*@mutable@*/ void *FILE;
typedef /*@abstract@*/ /*@mutable@*/ void *fpos_t;
-/*@constant int _IOFBF; @*/
-/*@constant int _IOLBF; @*/
-/*@constant int _IONBF; @*/
+/*@constant size_t _IOFBF; @*/
+/*@constant size_t _IOLBF; @*/
+/*@constant size_t _IONBF; @*/
+
+/*@constant size_t BUFSIZ; @*/ /* evans 2002-02-27 change suggested by Walter Briscoe */
-/*@constant int BUFSIZ; @*/
/*@constant int EOF; @*/
/*@constant int FOPEN_MAX; @*/
int remove (char *filename) /*@modifies fileSystem, errno@*/ ;
int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ;
-/*@null@*/ FILE *tmpfile (void) /*@modifies fileSystem@*/ ;
+/*@dependent@*/ /*@null@*/ FILE *tmpfile (void)
+ /*@modifies fileSystem, errno@*/ ;
+
/*@observer@*/ char *
tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s)
/*@modifies *s, internalState@*/ ;
-int fclose (FILE *stream) /*@modifies *stream, errno, fileSystem;@*/ ;
+int fclose (FILE *stream)
+ /*@modifies *stream, errno, fileSystem;@*/ ;
+
int fflush (/*@null@*/ FILE *stream)
/*@modifies *stream, errno, fileSystem;@*/ ;
/*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode)
/*@modifies fileSystem@*/ ;
-/*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream)
+/*@dependent@*/ /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream)
/*@modifies *stream, fileSystem, errno@*/ ;
-void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf)
- /*@modifies fileSystem, *stream, *buf@*/ ;
+void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf)
+ /*@modifies fileSystem, *stream, *buf@*/
+ /*:errorcode != 0*/ ;
+ /*:requires maxSet(buf) >= (BUFSIZ - 1):*/ ;
-int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf,
- int mode, size_t size)
- /*@modifies fileSystem, *stream, *buf@*/ ;
+int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf,
+ int mode, size_t size)
+ /*@modifies fileSystem, *stream, *buf@*/
+ /*@requires maxSet(buf) >= (size - 1) @*/ ;
# ifdef STRICT
/*@printflike@*/
/*@scanflike@*/
int fscanf (FILE *stream, char *format, ...)
- /*@modifies fileSystem, *stream@*/ ;
+ /*@modifies fileSystem, *stream, errno@*/ ;
# ifdef STRICT
/*@printflike@*/
/*@scanflike@*/
int scanf(char *format, ...)
/*@globals stdin@*/
- /*@modifies fileSystem, *stdin@*/ ;
+ /*@modifies fileSystem, *stdin, errno@*/ ;
+ /*drl added errno 09-19-2001 */ ;
# ifdef STRICT
/*@printflike@*/
int sprintf (/*@out@*/ char *s, char *format, ...)
+ /*@warn bufferoverflowhigh "Buffer overflow possible with sprintf. Recommend using snprintf instead"@*/
/*@modifies *s@*/ ;
# else
/*@printflike@*/
int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...)
+ /*@warn bufferoverflowhigh "Buffer overflow possible with sprintf. Recommend using snprintf instead"@*/
/*@modifies *s@*/ ;
# endif
+/* evans 2002-07-09: snprintf added to standard.h (from unix.h) */
+/*@printflike@*/
+int snprintf (/*@out@*/ char * restrict s, size_t n, const char * restrict format, ...)
+ /*@modifies s@*/
+ /*@requires maxSet(s) >= (n - 1)@*/ ;
+
/*@scanflike@*/
-int sscanf (/*@out@*/ char *s, char *format, ...) /*@*/ ;
+int sscanf (/*@out@*/ char *s, char *format, ...) /*@modifies errno@*/ ;
/* modifies extra arguments */
int vprintf (const char *format, va_list arg)
/*@modifies str@*/ ;
int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap)
- /*@requires maxSet(str) >= size@*/
+ /*@requires maxSet(str) >= (size - 1)@*/ /* drl - this was size, size-1 in stdio.h */
/*@modifies str@*/ ;
int fgetc (FILE *stream)
/*@null@*/ char *
fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream)
/*@modifies fileSystem, *s, *stream, errno@*/
- /*@requires MaxSet(s) >= (n -1); @*/
- /*@ensures MaxRead(s) <= (n -1) /\ MaxRead(s) >= 0; @*/
+ /*@requires maxSet(s) >= (n -1); @*/
+ /*@ensures maxRead(s) <= (n -1) /\ maxRead(s) >= 0; @*/
;
int fputc (int /*@alt char@*/ c, FILE *stream)
/* note use of sef --- stream may be evaluated more than once */
int getc (/*@sef@*/ FILE *stream)
- /*@modifies fileSystem, *stream@*/ ;
+ /*@modifies fileSystem, *stream, errno@*/ ;
-int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/ ;
+int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin, errno@*/ ;
/*@null@*/ char *gets (/*@out@*/ char *s)
/*@warn bufferoverflowhigh
int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
/*:errorcode EOF:*/
- /*@modifies fileSystem, *stream;@*/ ;
+ /*@modifies fileSystem, *stream, errno;@*/ ;
int putchar (int /*@alt char@*/ c)
/*:errorcode EOF:*/
- /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ;
+ /*@globals stdout@*/
+ /*@modifies fileSystem, *stdout, errno@*/ ;
int puts (const char *s)
/*:errorcode EOF:*/
/*@globals stdout@*/
- /*@modifies fileSystem, *stdout@*/ ;
+ /*@modifies fileSystem, *stdout, errno@*/ ;
int ungetc (int /*@alt char@*/ c, FILE *stream)
- /*@modifies fileSystem, *stream, errno@*/ ;
+ /*@modifies fileSystem, *stream@*/ ;
+ /*drl REMOVED errno 09-19-2001*/
size_t
fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream)
- /*@modifies fileSystem, *ptr, *stream, errno@*/ ;
+ /*@modifies fileSystem, *ptr, *stream, errno@*/
+ /*requires maxSet(ptr) >= (size - 1) @*/
+ /*@ensures maxRead(ptr) == (size - 1) @*/ ;
size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream)
- /*@modifies fileSystem, *stream, errno@*/ ;
+ /*@modifies fileSystem, *stream, errno@*/
+ /*@requires maxRead(ptr) >= size @*/ ;
int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos)
- /*@modifies *pos, errno@*/ ;
+ /*@modifies *pos, errno@*/
+ /*@requires maxSet(pos) >= 0@*/
+ /*@ensures maxRead(pos) >= 0 @*/;
int fseek (FILE *stream, long int offset, int whence)
/*:errorcode -1:*/
void clearerr (FILE *stream) /*@modifies *stream@*/ ;
int feof (FILE *stream) /*@modifies errno@*/ ;
+
int ferror (FILE *stream) /*@modifies errno@*/ ;
void perror (/*@null@*/ char *s)
*/
/*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/
- /*@ensures MaxSet(result) == (nobj - 1); @*/ ;
+ /*@ensures maxSet(result) == (nobj - 1); @*/ ;
/*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@*/
- /*@ensures MaxSet(result) == (size - 1); @*/ ;
+ /*@ensures maxSet(result) == (size - 1); @*/ ;
/*end drl changed */
/*@null@*/ /*@only@*/ void *
realloc (/*@null@*/ /*@only@*/ /*@special@*/ void *p,
size_t size) /*@releases p@*/ /*@modifies *p@*/
- /*@ensures MaxSet(result) == (size - 1) @*/;
+ /*@ensures maxSet(result) == (size - 1) @*/;
# endif
/*
/*@null@*/ /*@only@*/ void *
realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size)
- /*@modifies *p@*/ /*@ensures MaxSet(result) >= (size - 1) @*/;
+ /*@modifies *p@*/ /*@ensures maxSet(result) >= (size - 1) @*/;
void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies p@*/ ;
void /*@alt void * @*/
memcpy (/*@unique@*/ /*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
/*@modifies *s1@*/
- /*@requires MaxRead(s2) >= (n - 1) /\ MaxSet(s1) >= (n - 1); @*/
+ /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
;
void /*@alt void * @*/
memmove (/*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
/*@modifies *s1@*/
- /*@requires MaxRead(s2) >= (n - 1) /\ MaxSet(s1) >= (n - 1); @*/
+ /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
;
strcpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2)
/*@modifies *s1@*/
/*@requires maxSet(s1) >= maxRead(s2) @*/
- /*@ensures MaxRead(s1) == MaxRead (s2) /\ MaxRead(result) == MaxRead(s2) /\ MaxSet(result) == MaxSet(s1); @*/;
+ /*@ensures maxRead(s1) == maxRead (s2) /\ maxRead(result) == maxRead(s2) /\ maxSet(result) == maxSet(s1); @*/;
void /*@alt char * @*/
strncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2, size_t n)
- /*@modifies *s1@*/ /*@requires MaxSet(s1) >= ( n - 1 ); @*/ /*@ensures MaxRead (s2) >= MaxRead(s1) /\ MaxRead (s1) <= n; @*/;
+ /*@modifies *s1@*/
+ /*@requires maxSet(s1) >= ( n - 1 ); @*/
+ /*@ensures maxRead (s2) >= maxRead(s1) /\ maxRead (s1) <= n; @*/ ;
void /*@alt char * @*/
strcat (/*@unique@*/ /*@returned@*/ char *s1, char *s2)
- /*@modifies *s1@*/ /*@requires MaxSet(s1) >= (MaxRead(s1) + MaxRead(s2) );@*/
- /*@ensures MaxRead(result) == (MaxRead(s1) + MaxRead(s2) );@*/;
+ /*@modifies *s1@*/ /*@requires maxSet(s1) >= (maxRead(s1) + maxRead(s2) );@*/
+ /*@ensures maxRead(result) == (maxRead(s1) + maxRead(s2) );@*/;
void /*@alt char * @*/
strncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, size_t n)
/*@modifies *s1@*/
- /*@requires MaxSet(s1) >= ( MaxRead(s1) + n); @*/
- /*@ensures MaxRead(s1) >= (MaxRead(s1) + n); @*/;
+ /*@requires maxSet(s1) >= ( maxRead(s1) + n); @*/
+ /*@ensures maxRead(s1) >= (maxRead(s1) + n); @*/;
/*drl end*/
# ifdef STRICT
/*@exposed@*/ /*@null@*/ char *
-strchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0 @*/ ;
+strchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
# else
/*@exposed@*/ /*@null@*/ char *
- strchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0; @*/ ;
+ strchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0; @*/ ;
# endif
size_t strcspn (char *s1, char *s2) /*@*/ ;
# ifdef STRICT
/*@null@*/ /*@exposed@*/ char *
- strrchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0 @*/ ;
+ strrchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
# else
/*@null@*/ /*@exposed@*/ char *
- strrchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0 @*/ ;
+ strrchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
# endif
size_t strspn (char *s, char *t) /*@*/ ;
/*@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 @*/ ;
+ strstr (/*@returned@*/ const char *s, const 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)@*/ ;
/*@null@*/ /*@exposed@*/ char *
strtok (/*@returned@*/ /*@null@*/ char *s, char *t)
void /*@alt void *@*/ memset (/*@out@*/ /*@returned@*/ void *s,
int c, size_t n)
- /*@modifies *s@*/ /*@requires MaxSet(s) >= (n - 1) @*/ /*@ensures MaxRead(s) >= (n - 1) @*/ ;
+ /*@modifies *s@*/ /*@requires maxSet(s) >= (n - 1) @*/ /*@ensures maxRead(s) >= (n - 1) @*/ ;
/*@observer@*/ char *strerror (int errnum) /*@*/ ;
/*drl */
-size_t strlen (char *s) /*@*/ /*@ensures result == MaxRead(s); @*/;
+size_t strlen (char *s) /*@*/ /*@ensures result == maxRead(s); @*/;
/*
** time.h
/*@modifies *tp@*/ ;
/*@observer@*/ char *asctime (struct tm *timeptr)
- /*@modifies errno*/ /*@ensures MaxSet(result) == 25 /\ MaxRead(result) == 25; @*/ ;
+ /*@modifies errno*/ /*@ensures maxSet(result) == 25 /\ maxRead(result) == 25; @*/ ;
/*@observer@*/ char *ctime (time_t *tp) /*@*/
- /*@ensures MaxSet(result) == 25 /\ MaxRead(result) == 25; @*/;
+ /*@ensures maxSet(result) == 25 /\ maxRead(result) == 25; @*/;
/*@null@*/ /*@observer@*/ struct tm *gmtime (time_t *tp) /*@*/ ;
/*@constant size_t INTPTR_MIN@*/
/*@constant size_t INTPTR_MAX@*/
+
+/*drl 3/5/2003
+ added the __func__ identifier from C99
+ This won't follow the same semantics as
+ __func__ in C99
+
+ FWIW C99 says that __func__ should have the value of the
+ lexically enclosing function
+ e.g. in the function foo __func__ == "foo"
+ in bar __func__ == "bar"
+
+ We're just having the value be constant here and picking
+ an arbitary value.
+*/
+static const char _ _func_ _[] = "function-name";
+
+
+/* drl 3/5/2003
+ added limited supported for _Bool */
+
+/*__Bool shouled really be a basic type but edited the grammar and ripping
+ apart the rest of Splint would probably break too much stuff...
+*/
+
+typedef /*@unsignedintegraltype@*/ _Bool;
+
+/*support stdbool.h */
+
+#define bool _Bool
+
+#define true 1
+
+#define false 0
+
+#define __bool_true_false_are_defined 1