From 79127b5daf9969416a14658e7f98ee1fe5b1ba7a Mon Sep 17 00:00:00 2001 From: evans1629 Date: Sun, 30 Dec 2001 22:31:40 +0000 Subject: [PATCH] Added legacy flag for unix lib. --- lib/ansi.h | 653 ++++++++++++++++++++++++----------------------- lib/unix.h | 184 +++++++++++-- src/flags.def | 8 + test/help.expect | 2 + 4 files changed, 497 insertions(+), 350 deletions(-) diff --git a/lib/ansi.h b/lib/ansi.h index 2e91a4e..1d49737 100644 --- a/lib/ansi.h +++ b/lib/ansi.h @@ -17,9 +17,9 @@ /*@constant int EILSEQ;@*/ # ifdef STRICT -/*@checkedstrict@*/ extern int errno; +/*@checkedstrict@*/ int errno; # else -/*@unchecked@*/ extern int errno; +/*@unchecked@*/ int errno; # endif /* @@ -47,10 +47,10 @@ typedef /*@abstract@*/ mbstate_t; /*@constant lltX_bool NDEBUG;@*/ # ifdef STRICT -extern /*@falseexit@*/ void assert (/*@sef@*/ lltX_bool e) +/*@falseexit@*/ void assert (/*@sef@*/ lltX_bool e) /*@*/ ; # else -extern /*@falseexit@*/ void assert (/*@sef@*/ lltX_bool /*@alt int@*/ e) +/*@falseexit@*/ void assert (/*@sef@*/ lltX_bool /*@alt int@*/ e) /*@*/ ; # endif @@ -60,33 +60,33 @@ extern /*@falseexit@*/ void assert (/*@sef@*/ lltX_bool /*@alt int@*/ e) */ # ifdef STRICT -extern lltX_bool isalnum (int c) /*@*/ ; -extern lltX_bool isalpha (int c) /*@*/ ; -extern lltX_bool iscntrl (int c) /*@*/ ; -extern lltX_bool isdigit (int c) /*@*/ ; -extern lltX_bool isgraph (int c) /*@*/ ; -extern lltX_bool islower (int c) /*@*/ ; -extern lltX_bool isprint (int c) /*@*/ ; -extern lltX_bool ispunct (int c) /*@*/ ; -extern lltX_bool isspace (int c) /*@*/ ; -extern lltX_bool isupper (int c) /*@*/ ; -extern lltX_bool isxdigit (int c) /*@*/ ; -extern char tolower (int c) /*@*/ ; -extern char toupper (int c) /*@*/ ; +lltX_bool isalnum (int c) /*@*/ ; +lltX_bool isalpha (int c) /*@*/ ; +lltX_bool iscntrl (int c) /*@*/ ; +lltX_bool isdigit (int c) /*@*/ ; +lltX_bool isgraph (int c) /*@*/ ; +lltX_bool islower (int c) /*@*/ ; +lltX_bool isprint (int c) /*@*/ ; +lltX_bool ispunct (int c) /*@*/ ; +lltX_bool isspace (int c) /*@*/ ; +lltX_bool isupper (int c) /*@*/ ; +lltX_bool isxdigit (int c) /*@*/ ; +char tolower (int c) /*@*/ ; +char toupper (int c) /*@*/ ; # else -extern lltX_bool /*@alt int@*/ isalnum (int /*@alt unsigned char@*/ c) /*@*/ ; -extern lltX_bool /*@alt int@*/ isalpha (int /*@alt unsigned char@*/ c) /*@*/ ; -extern lltX_bool /*@alt int@*/ iscntrl (int /*@alt unsigned char@*/ c) /*@*/ ; -extern lltX_bool /*@alt int@*/ isdigit (int /*@alt unsigned char@*/ c) /*@*/ ; -extern lltX_bool /*@alt int@*/ isgraph (int /*@alt unsigned char@*/ c) /*@*/ ; -extern lltX_bool /*@alt int@*/ islower (int /*@alt unsigned char@*/ c) /*@*/ ; -extern lltX_bool /*@alt int@*/ isprint (int /*@alt unsigned char@*/ c) /*@*/ ; -extern lltX_bool /*@alt int@*/ ispunct (int /*@alt unsigned char@*/ c) /*@*/ ; -extern lltX_bool /*@alt int@*/ isspace (int /*@alt unsigned char@*/ c) /*@*/ ; -extern lltX_bool /*@alt int@*/ isupper (int /*@alt unsigned char@*/ c) /*@*/ ; -extern lltX_bool /*@alt int@*/ isxdigit (int /*@alt unsigned char@*/ c) /*@*/ ; -extern char /*@alt int@*/ tolower (int /*@alt unsigned char@*/ c) /*@*/ ; -extern char /*@alt int@*/ toupper (int /*@alt unsigned char@*/ c) /*@*/ ; +lltX_bool /*@alt int@*/ isalnum (int /*@alt unsigned char@*/ c) /*@*/ ; +lltX_bool /*@alt int@*/ isalpha (int /*@alt unsigned char@*/ c) /*@*/ ; +lltX_bool /*@alt int@*/ iscntrl (int /*@alt unsigned char@*/ c) /*@*/ ; +lltX_bool /*@alt int@*/ isdigit (int /*@alt unsigned char@*/ c) /*@*/ ; +lltX_bool /*@alt int@*/ isgraph (int /*@alt unsigned char@*/ c) /*@*/ ; +lltX_bool /*@alt int@*/ islower (int /*@alt unsigned char@*/ c) /*@*/ ; +lltX_bool /*@alt int@*/ isprint (int /*@alt unsigned char@*/ c) /*@*/ ; +lltX_bool /*@alt int@*/ ispunct (int /*@alt unsigned char@*/ c) /*@*/ ; +lltX_bool /*@alt int@*/ isspace (int /*@alt unsigned char@*/ c) /*@*/ ; +lltX_bool /*@alt int@*/ isupper (int /*@alt unsigned char@*/ c) /*@*/ ; +lltX_bool /*@alt int@*/ isxdigit (int /*@alt unsigned char@*/ c) /*@*/ ; +char /*@alt int@*/ tolower (int /*@alt unsigned char@*/ c) /*@*/ ; +char /*@alt int@*/ toupper (int /*@alt unsigned char@*/ c) /*@*/ ; # endif /* @@ -122,10 +122,10 @@ struct lconv /*@constant int LC_NUMERIC;@*/ /*@constant int LC_TIME;@*/ -extern /*@observer@*/ /*@null@*/ char *setlocale (int category, /*@null@*/ char *locale) +/*@observer@*/ /*@null@*/ char *setlocale (int category, /*@null@*/ char *locale) /*@modifies internalState, errno@*/ ; -extern struct lconv *localeconv (void) /*@*/ ; +struct lconv *localeconv (void) /*@*/ ; /* ** float.h @@ -136,37 +136,37 @@ extern struct lconv *localeconv (void) /*@*/ ; ** constants. They may be used as lvalues. */ -/*@unchecked@*/ extern int DBL_DIG; -/*@unchecked@*/ extern double DBL_EPSILON; -/*@unchecked@*/ extern int DBL_MANT_DIG; -/*@unchecked@*/ extern double DBL_MAX; -/*@unchecked@*/ extern int DBL_MAX_10_EXP; -/*@unchecked@*/ extern int DBL_MAX_EXP; -/*@unchecked@*/ extern double DBL_MIN; -/*@unchecked@*/ extern int DBL_MIN_10_EXP; -/*@unchecked@*/ extern int DBL_MIN_EXP; - -/*@unchecked@*/ extern int FLT_DIG; -/*@unchecked@*/ extern float FLT_EPSILON; -/*@unchecked@*/ extern int FLT_MANT_DIG; -/*@unchecked@*/ extern float FLT_MAX; -/*@unchecked@*/ extern int FLT_MAX_10_EXP; -/*@unchecked@*/ extern int FLT_MAX_EXP; -/*@unchecked@*/ extern float FLT_MIN; -/*@unchecked@*/ extern int FLT_MIN_10_EXP; -/*@unchecked@*/ extern int FLT_MIN_EXP; +/*@unchecked@*/ int DBL_DIG; +/*@unchecked@*/ double DBL_EPSILON; +/*@unchecked@*/ int DBL_MANT_DIG; +/*@unchecked@*/ double DBL_MAX; +/*@unchecked@*/ int DBL_MAX_10_EXP; +/*@unchecked@*/ int DBL_MAX_EXP; +/*@unchecked@*/ double DBL_MIN; +/*@unchecked@*/ int DBL_MIN_10_EXP; +/*@unchecked@*/ int DBL_MIN_EXP; + +/*@unchecked@*/ int FLT_DIG; +/*@unchecked@*/ float FLT_EPSILON; +/*@unchecked@*/ int FLT_MANT_DIG; +/*@unchecked@*/ float FLT_MAX; +/*@unchecked@*/ int FLT_MAX_10_EXP; +/*@unchecked@*/ int FLT_MAX_EXP; +/*@unchecked@*/ float FLT_MIN; +/*@unchecked@*/ int FLT_MIN_10_EXP; +/*@unchecked@*/ int FLT_MIN_EXP; /*@constant int FLT_RADIX@*/ -/*@unchecked@*/ extern int FLT_ROUNDS; - -/*@unchecked@*/ extern int LDBL_DIG; -/*@unchecked@*/ extern long double LDBL_EPSILON; -/*@unchecked@*/ extern int LDBL_MANT_DIG; -/*@unchecked@*/ extern long double LDBL_MAX; -/*@unchecked@*/ extern int LDBL_MAX_10_EXP; -/*@unchecked@*/ extern int LDBL_MAX_EXP; -/*@unchecked@*/ extern long double LDBL_MIN; -/*@unchecked@*/ extern int LDBL_MIN_10_EXP; -/*@unchecked@*/ extern int LDBL_MIN_EXP; +/*@unchecked@*/ int FLT_ROUNDS; + +/*@unchecked@*/ int LDBL_DIG; +/*@unchecked@*/ long double LDBL_EPSILON; +/*@unchecked@*/ int LDBL_MANT_DIG; +/*@unchecked@*/ long double LDBL_MAX; +/*@unchecked@*/ int LDBL_MAX_10_EXP; +/*@unchecked@*/ int LDBL_MAX_EXP; +/*@unchecked@*/ long double LDBL_MIN; +/*@unchecked@*/ int LDBL_MIN_10_EXP; +/*@unchecked@*/ int LDBL_MIN_EXP; /* ** limits.h @@ -200,30 +200,30 @@ extern struct lconv *localeconv (void) /*@*/ ; ** math functions that may have a range error modify errno */ -extern double sin (double x) /*@*/ ; -extern double cos (double x) /*@*/ ; -extern double tan (double x) /*@*/ ; -extern double asin (double x) /*@modifies errno@*/ ; -extern double acos (double x) /*@modifies errno@*/ ; -extern double atan (double x) /*@*/ ; -extern double atan2 (double y, double x) /*@*/ ; -extern double sinh (double x) /*@*/ ; -extern double cosh (double x) /*@modifies errno@*/ ; -extern double tanh (double x) /*@*/ ; +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 atan (double x) /*@*/ ; +double atan2 (double y, double x) /*@*/ ; +double sinh (double x) /*@*/ ; +double cosh (double x) /*@modifies errno@*/ ; +double tanh (double x) /*@*/ ; -extern double exp (double x) /*@modifies errno@*/ ; -extern double ldexp (double x, int n) /*@modifies errno@*/ ; -extern double frexp (double x, /*@out@*/ int *xp) /*@modifies *xp;@*/ ; +double exp (double x) /*@modifies errno@*/ ; +double ldexp (double x, int n) /*@modifies errno@*/ ; +double frexp (double x, /*@out@*/ int *xp) /*@modifies *xp;@*/ ; -extern double log (double x) /*@modifies errno@*/ ; -extern double log10 (double x) /*@modifies errno@*/ ; +double log (double x) /*@modifies errno@*/ ; +double log10 (double x) /*@modifies errno@*/ ; -extern double pow (double x, double y) /*@modifies errno@*/ ; -extern double sqrt (double x) /*@modifies errno@*/ ; +double pow (double x, double y) /*@modifies errno@*/ ; +double sqrt (double x) /*@modifies errno@*/ ; -extern double ceil (double x) /*@*/ ; -extern double floor (double x) /*@*/ ; -extern double fabs (double x) /*@*/ ; +double ceil (double x) /*@*/ ; +double floor (double x) /*@*/ ; +double fabs (double x) /*@*/ ; double modf (double x, /*@out@*/ double *ip) /*@modifies *ip;@*/ ; double fmod (double x, double y) /*@*/ ; @@ -236,50 +236,50 @@ double fmod (double x, double y) /*@*/ ; # ifdef OPTIONAL_MATH -extern float acosf (float x) /*@modifies errno@*/ ; -extern long double acosl (long double x) /*@modifies errno@*/ ; -extern float asinf (float x) /*@modifies errno@*/ ; -extern long double asinl (long double x) /*@modifies errno@*/ ; -extern float atanf (float x) /*@*/ ; -extern long double atanl (long double x) /*@*/ ; -extern float atan2f (float y, float x) /*@*/ ; -extern long double atan2l (long double y, long double x) /*@*/ ; -extern float ceilf (float x) /*@*/ ; -extern long double ceill (long double x) /*@*/ ; -extern float cosf (float x) /*@*/ ; -extern long double cosl (long double x) /*@*/ ; -extern float coshf (float x) /*@modifies errno@*/ ; -extern long double coshl (long double x) /*@modifies errno@*/ ; -extern float expf (float x) /*@modifies errno@*/ ; -extern long double expl (long double x) /*@modifies errno@*/; -extern float fabsf (float x) /*@*/ ; -extern long double fabsl (long double x) /*@*/ ; -extern float floorf (float x) /*@*/ ; -extern long double floorl (long double x) /*@*/ ; -extern float fmodf (float x, float y) /*@*/ ; -extern long double fmodl (long double x, long double y) /*@*/ ; -extern float frexpf (float x, /*@out@*/ int *xp) /*@modifies *xp@*/; -extern long double frexpl (long double x, /*@out@*/ int *xp) /*@modifies *xp@*/; -extern float ldexpf (float x, int n) /*@modifies errno@*/ ; -extern long double ldexpl (long double x, int n) /*@modifies errno@*/ ; -extern float logf (float x) /*@modifies errno@*/ ; -extern long double logl (long double x) /*@modifies errno@*/ ; -extern float log10f (float x) /*@modifies errno@*/; -extern long double log10l (long double x) /*@modifies errno@*/; -extern float modff (float x, /*@out@*/ float *xp) /*@modifies *xp@*/ ; -extern long double modfl (long double x, /*@out@*/ long double *xp) /*@modifies *xp@*/ ; -extern float powf (float x, float y) /*@modifies errno@*/ ; -extern long double powl (long double x, long double y) /*@modifies errno@*/ ; -extern float sinf (float x) /*@*/ ; -extern long double sinl (long double x) /*@*/ ; -extern float sinhf (float x) /*@*/ ; -extern long double sinhl (long double x) /*@*/ ; -extern float sqrtf (float x) /*@modifies errno@*/ ; -extern long double sqrtl (long double x) /*@modifies errno@*/ ; -extern float tanf (float x) /*@*/ ; -extern long double tanl (long double x) /*@*/ ; -extern float tanhf (float x) /*@*/ ; -extern long double tanhl (long double x) /*@*/ ; +float acosf (float x) /*@modifies errno@*/ ; +long double acosl (long double x) /*@modifies errno@*/ ; +float asinf (float x) /*@modifies errno@*/ ; +long double asinl (long double x) /*@modifies errno@*/ ; +float atanf (float x) /*@*/ ; +long double atanl (long double x) /*@*/ ; +float atan2f (float y, float x) /*@*/ ; +long double atan2l (long double y, long double x) /*@*/ ; +float ceilf (float x) /*@*/ ; +long double ceill (long double x) /*@*/ ; +float cosf (float x) /*@*/ ; +long double cosl (long double x) /*@*/ ; +float coshf (float x) /*@modifies errno@*/ ; +long double coshl (long double x) /*@modifies errno@*/ ; +float expf (float x) /*@modifies errno@*/ ; +long double expl (long double x) /*@modifies errno@*/; +float fabsf (float x) /*@*/ ; +long double fabsl (long double x) /*@*/ ; +float floorf (float x) /*@*/ ; +long double floorl (long double x) /*@*/ ; +float fmodf (float x, float y) /*@*/ ; +long double fmodl (long double x, long double y) /*@*/ ; +float frexpf (float x, /*@out@*/ int *xp) /*@modifies *xp@*/; +long double frexpl (long double x, /*@out@*/ int *xp) /*@modifies *xp@*/; +float ldexpf (float x, int n) /*@modifies errno@*/ ; +long double ldexpl (long double x, int n) /*@modifies errno@*/ ; +float logf (float x) /*@modifies errno@*/ ; +long double logl (long double x) /*@modifies errno@*/ ; +float log10f (float x) /*@modifies errno@*/; +long double log10l (long double x) /*@modifies errno@*/; +float modff (float x, /*@out@*/ float *xp) /*@modifies *xp@*/ ; +long double modfl (long double x, /*@out@*/ long double *xp) /*@modifies *xp@*/ ; +float powf (float x, float y) /*@modifies errno@*/ ; +long double powl (long double x, long double y) /*@modifies errno@*/ ; +float sinf (float x) /*@*/ ; +long double sinl (long double x) /*@*/ ; +float sinhf (float x) /*@*/ ; +long double sinhl (long double x) /*@*/ ; +float sqrtf (float x) /*@modifies errno@*/ ; +long double sqrtl (long double x) /*@modifies errno@*/ ; +float tanf (float x) /*@*/ ; +long double tanl (long double x) /*@*/ ; +float tanhf (float x) /*@*/ ; +long double tanhl (long double x) /*@*/ ; # endif @@ -289,8 +289,8 @@ extern long double tanhl (long double x) /*@*/ ; typedef /*@abstract@*/ /*@mutable@*/ void *jmp_buf; -extern int setjmp (/*@out@*/ jmp_buf env) /*@modifies env;@*/ ; -extern /*@mayexit@*/ void longjmp (jmp_buf env, int val) /*@*/ ; +int setjmp (/*@out@*/ jmp_buf env) /*@modifies env;@*/ ; +/*@mayexit@*/ void longjmp (jmp_buf env, int val) /*@*/ ; /* ** signal.h @@ -314,10 +314,10 @@ typedef /*@integraltype@*/ sig_atomic_t; ** returns the function (or NULL if unsuccessful). */ -extern /*@null@*/ void (*signal (int sig, /*@null@*/ void (*func)(int))) (int) +/*@null@*/ void (*signal (int sig, /*@null@*/ void (*func)(int))) (int) /*@modifies internalState, errno;@*/ ; -extern /*@mayexit@*/ int raise (int sig) ; +/*@mayexit@*/ int raise (int sig) ; /* ** stdarg.h @@ -325,8 +325,8 @@ extern /*@mayexit@*/ int raise (int sig) ; typedef /*@abstract@*/ /*@mutable@*/ void *va_list; -extern void va_start (/*@out@*/ va_list ap, ...) /*@modifies ap;@*/ ; -extern void va_end (va_list va) /*@modifies va;@*/ ; +void va_start (/*@out@*/ va_list ap, ...) /*@modifies ap;@*/ ; +void va_end (va_list va) /*@modifies va;@*/ ; /* ** va_arg is builtin @@ -367,69 +367,69 @@ typedef /*@abstract@*/ /*@mutable@*/ void *fpos_t; /*@unchecked@*/ FILE *stdout; # endif -extern int remove (char *filename) /*@modifies fileSystem, errno@*/ ; -extern int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ; +int remove (char *filename) /*@modifies fileSystem, errno@*/ ; +int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ; -extern /*@null@*/ FILE *tmpfile (void) /*@modifies fileSystem@*/ ; -extern /*@observer@*/ char * +/*@null@*/ FILE *tmpfile (void) /*@modifies fileSystem@*/ ; +/*@observer@*/ char * tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s) /*@modifies *s, internalState@*/ ; -extern int fclose (FILE *stream) /*@modifies *stream, errno, fileSystem;@*/ ; -extern int fflush (/*@null@*/ FILE *stream) +int fclose (FILE *stream) /*@modifies *stream, errno, fileSystem;@*/ ; +int fflush (/*@null@*/ FILE *stream) /*@modifies *stream, errno, fileSystem;@*/ ; -extern /*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode) +/*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode) /*@modifies fileSystem@*/ ; -extern /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream) +/*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream) /*@modifies *stream, fileSystem, errno@*/ ; -extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf) +void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf) /*@modifies fileSystem, *stream, *buf@*/ ; -extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf, +int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf, int mode, size_t size) /*@modifies fileSystem, *stream, *buf@*/ ; # ifdef STRICT /*@printflike@*/ -extern int fprintf (FILE *stream, char *format, ...) +int fprintf (FILE *stream, char *format, ...) /*@modifies fileSystem, *stream@*/ ; # else /*@printflike@*/ -extern int /*@alt void@*/ fprintf (FILE *stream, char *format, ...) +int /*@alt void@*/ fprintf (FILE *stream, char *format, ...) /*@modifies fileSystem, *stream@*/ ; # endif /*@scanflike@*/ -extern int fscanf (FILE *stream, char *format, ...) +int fscanf (FILE *stream, char *format, ...) /*@modifies fileSystem, *stream@*/ ; # ifdef STRICT /*@printflike@*/ -extern int printf (char *format, ...) +int printf (char *format, ...) /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ; # else /*@printflike@*/ -extern int /*@alt void@*/ printf (char *format, ...) +int /*@alt void@*/ printf (char *format, ...) /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ; # endif /*@scanflike@*/ -extern int scanf(char *format, ...) +int scanf(char *format, ...) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/ ; # ifdef STRICT /*@printflike@*/ -extern int sprintf (/*@out@*/ char *s, char *format, ...) +int sprintf (/*@out@*/ char *s, char *format, ...) /*@modifies *s@*/ ; # else /*@printflike@*/ -extern int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...) +int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...) /*@modifies *s@*/ ; # endif @@ -452,102 +452,109 @@ int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap) /*@requires maxSet(str) >= size@*/ /*@modifies str@*/ ; -extern int fgetc (FILE *stream) +int fgetc (FILE *stream) /*@modifies fileSystem, *stream, errno@*/ ; -extern /*@null@*/ char * +/*@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; @*/ ; -extern int fputc (int /*@alt char@*/ c, FILE *stream) +int fputc (int /*@alt char@*/ c, FILE *stream) + /*:errorcode EOF:*/ /*@modifies fileSystem, *stream, errno@*/ ; -extern int fputs (char *s, FILE *stream) +int fputs (char *s, FILE *stream) /*@modifies fileSystem, *stream@*/ ; /* note use of sef --- stream may be evaluated more than once */ -extern int getc (/*@sef@*/ FILE *stream) +int getc (/*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ; -extern int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/ ; +int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/ ; -extern /*@null@*/ char *gets (/*@out@*/ char *s) +/*@null@*/ char *gets (/*@out@*/ char *s) /*@warn bufferoverflowhigh "Use of gets leads to a buffer overflow vulnerability. Use fgets instead"@*/ /*@globals stdin@*/ /*@modifies fileSystem, *s, *stdin, errno@*/ ; -extern int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream) - /*@modifies fileSystem, *stream;@*/ ; +int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream) + /*:errorcode EOF:*/ + /*@modifies fileSystem, *stream;@*/ ; -extern int putchar (int /*@alt char@*/ c) +int putchar (int /*@alt char@*/ c) + /*:errorcode EOF:*/ /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ; -extern int puts (const char *s) - /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ; +int puts (const char *s) + /*:errorcode EOF:*/ + /*@globals stdout@*/ + /*@modifies fileSystem, *stdout@*/ ; -extern int ungetc (int /*@alt char@*/ c, FILE *stream) +int ungetc (int /*@alt char@*/ c, FILE *stream) /*@modifies fileSystem, *stream, errno@*/ ; -extern size_t +size_t fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream) /*@modifies fileSystem, *ptr, *stream, errno@*/ ; -extern size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream) +size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream) /*@modifies fileSystem, *stream, errno@*/ ; -extern int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos) +int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos) /*@modifies *pos, errno@*/ ; -extern int fseek (FILE *stream, long int offset, int whence) - /*@modifies fileSystem, *stream, errno@*/ ; +int fseek (FILE *stream, long int offset, int whence) + /*:errorcode -1:*/ + /*@modifies fileSystem, *stream, errno@*/ ; -extern int fsetpos (FILE *stream, fpos_t *pos) +int fsetpos (FILE *stream, fpos_t *pos) /*@modifies fileSystem, *stream, errno@*/ ; -extern long int ftell(FILE *stream) /*@modifies errno@*/ ; +long int ftell(FILE *stream) + /*:errorcode -1:*/ /*@modifies errno*/ ; -extern void rewind (FILE *stream) /*@modifies *stream@*/ ; -extern void clearerr (FILE *stream) /*@modifies *stream@*/ ; +void rewind (FILE *stream) /*@modifies *stream@*/ ; +void clearerr (FILE *stream) /*@modifies *stream@*/ ; -extern int feof (FILE *stream) /*@modifies errno@*/ ; -extern int ferror (FILE *stream) /*@modifies errno@*/ ; +int feof (FILE *stream) /*@modifies errno@*/ ; +int ferror (FILE *stream) /*@modifies errno@*/ ; -extern void perror (/*@null@*/ char *s) +void perror (/*@null@*/ char *s) /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ; /* ** stdlib.h */ -extern double atof (char *s) /*@*/ ; -extern int atoi (char *s) /*@*/ ; -extern long int atol (char *s) /*@*/ ; +double atof (char *s) /*@*/ ; +int atoi (char *s) /*@*/ ; +long int atol (char *s) /*@*/ ; -extern double strtod (char *s, /*@null@*/ /*@out@*/ char **endp) +double strtod (char *s, /*@null@*/ /*@out@*/ char **endp) /*@modifies *endp, errno@*/ ; -extern long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base) +long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base) /*@modifies *endp, errno@*/ ; -extern unsigned long +unsigned long strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base) /*@modifies *endp, errno@*/ ; /*@constant int RAND_MAX; @*/ -extern int rand (void) /*@modifies internalState@*/ ; -extern void srand (unsigned int seed) /*@modifies internalState@*/ ; +int rand (void) /*@modifies internalState@*/ ; +void srand (unsigned int seed) /*@modifies internalState@*/ ; /* drl changed 12/29/2000 */ -extern /*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/ +/*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/ /*@ensures MaxSet(result) == (nobj - 1); @*/ ; -extern /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@*/ +/*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@*/ /*@ensures MaxSet(result) == (size - 1); @*/ ; /*end drl changed */ @@ -555,7 +562,7 @@ extern /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@*/ /* 11 June 1997: removed out on return value */ # if 0 -extern /*@null@*/ /*@only@*/ void * +/*@null@*/ /*@only@*/ void * realloc (/*@null@*/ /*@only@*/ /*@special@*/ void *p, size_t size) /*@releases p@*/ /*@modifies *p@*/ /*@ensures MaxSet(result) == (size - 1) @*/; @@ -570,33 +577,33 @@ extern /*@null@*/ /*@only@*/ void * ** Otherwise, storage is in the same state before and after the call. */ -extern /*@null@*/ /*@only@*/ void * +/*@null@*/ /*@only@*/ void * realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size) /*@modifies *p@*/ /*@ensures MaxSet(result) >= (size - 1) @*/; -extern void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies p@*/ ; +void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies p@*/ ; /*@constant int EXIT_FAILURE; @*/ /*@constant int EXIT_SUCCESS; @*/ -extern /*@exits@*/ void abort (void) /*@*/ ; -extern /*@exits@*/ void exit (int status) /*@*/ ; -extern int atexit (void (*func)(void)) /*@modifies internalState@*/ ; +/*@exits@*/ void abort (void) /*@*/ ; +/*@exits@*/ void exit (int status) /*@*/ ; +int atexit (void (*func)(void)) /*@modifies internalState@*/ ; -extern /*@observer@*/ /*@null@*/ char *getenv (char *name) /*@*/ ; +/*@observer@*/ /*@null@*/ char *getenv (char *name) /*@*/ ; -extern int system (/*@null@*/ char *s) /*@modifies fileSystem@*/ ; +int system (/*@null@*/ char *s) /*@modifies fileSystem@*/ ; -extern /*@null@*/ /*@dependent@*/ void * +/*@null@*/ /*@dependent@*/ void * bsearch (void *key, void *base, size_t n, size_t size, int (*compar)(void *, void *)) /*@*/ ; -extern void qsort (void *base, size_t n, size_t size, +void qsort (void *base, size_t n, size_t size, int (*compar)(void *, void *)) /*@modifies *base, errno@*/ ; -extern int abs (int n) /*@*/ ; +int abs (int n) /*@*/ ; typedef /*@concrete@*/ struct { @@ -604,9 +611,9 @@ typedef /*@concrete@*/ struct int rem; } div_t ; -extern div_t div (int num, int denom) /*@*/ ; +div_t div (int num, int denom) /*@*/ ; -extern long int labs (long int n) /*@*/ ; +long int labs (long int n) /*@*/ ; typedef /*@concrete@*/ struct { @@ -614,7 +621,7 @@ typedef /*@concrete@*/ struct long int rem; } ldiv_t ; -extern ldiv_t ldiv (long num, long denom) /*@*/ ; +ldiv_t ldiv (long num, long denom) /*@*/ ; /*@constant size_t MB_CUR_MAX; @*/ @@ -626,160 +633,160 @@ extern ldiv_t ldiv (long num, long denom) /*@*/ ; /*@constant int WCHAR_MIN@*/ /*@constant wint_t WEOF@*/ -extern wint_t btowc (int c) /*@*/ ; +wint_t btowc (int c) /*@*/ ; -extern wint_t fgetwc (FILE *fp) /*@modifies fileSystem, *fp*/ ; +wint_t fgetwc (FILE *fp) /*@modifies fileSystem, *fp*/ ; -extern /*@null@*/ wchar_t *fgetws (/*@returned@*/ wchar_t *s, int n, FILE *stream) +/*@null@*/ wchar_t *fgetws (/*@returned@*/ wchar_t *s, int n, FILE *stream) /*@modifies fileSystem, *s, *stream@*/; -extern wint_t fputwc (wchar_t c, FILE *stream) +wint_t fputwc (wchar_t c, FILE *stream) /*@modifies fileSystem, *stream@*/; -extern int fputws (const wchar_t *s, FILE *stream) +int fputws (const wchar_t *s, FILE *stream) /*@modifies fileSystem, *stream@*/ ; -extern int fwide (FILE *stream, int mode) /*@*/ ; +int fwide (FILE *stream, int mode) /*@*/ ; /* does not modify the stream */ -/*@printflike@*/ extern int fwprintf (FILE *stream, const wchar_t *format, ...) +/*@printflike@*/ int fwprintf (FILE *stream, const wchar_t *format, ...) /*@modifies *stream, fileSystem@*/ ; -/*@scanflike@*/ extern int fwscanf (FILE *stream, const wchar_t *format, ...) +/*@scanflike@*/ int fwscanf (FILE *stream, const wchar_t *format, ...) /*@modifies *stream, fileSystem@*/ ; /* note use of sef --- stream may be evaluated more than once */ -extern wint_t getwc (/*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ; +wint_t getwc (/*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ; -extern wint_t getwchar (void) /*@modifies fileSystem, *stdin@*/; +wint_t getwchar (void) /*@modifies fileSystem, *stdin@*/; -extern size_t mbrlen (const char *s, size_t n, /*@null@*/ mbstate_t *ps) /*@*/ ; +size_t mbrlen (const char *s, size_t n, /*@null@*/ mbstate_t *ps) /*@*/ ; -extern size_t mbrtowc (/*@null@*/ wchar_t *pwc, const char *s, size_t n, +size_t mbrtowc (/*@null@*/ wchar_t *pwc, const char *s, size_t n, /*@null@*/ mbstate_t *ps) /*@modifies *pwc@*/ ; -extern int mbsinit (/*@null@*/ const mbstate_t *ps) /*@*/ ; +int mbsinit (/*@null@*/ const mbstate_t *ps) /*@*/ ; -extern size_t mbsrtowcs (/*@null@*/ wchar_t *dst, const char **src, size_t len, +size_t mbsrtowcs (/*@null@*/ wchar_t *dst, const char **src, size_t len, /*@null@*/ mbstate_t *ps) /*@modifies *dst@*/ ; /* note use of sef --- stream may be evaluated more than once */ -extern wint_t putwc (wchar_t c, /*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ; +wint_t putwc (wchar_t c, /*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ; -extern wint_t putwchar (wchar_t c) /*@modifies fileSystem, *stdout@*/ ; +wint_t putwchar (wchar_t c) /*@modifies fileSystem, *stdout@*/ ; -/*@printflike@*/ extern int swprintf (wchar_t *s, size_t n, const wchar_t *format, ...) +/*@printflike@*/ int swprintf (wchar_t *s, size_t n, const wchar_t *format, ...) /*@modifies *s@*/ ; -/*@scanflike@*/ extern int swscanf (const wchar_t *s, const wchar_t *format, ...) +/*@scanflike@*/ int swscanf (const wchar_t *s, const wchar_t *format, ...) /*@modifies *stdin@*/ ; -extern wint_t ungetwc (wint_t c, FILE *stream) /*@modifies fileSystem, *stream@*/ ; +wint_t ungetwc (wint_t c, FILE *stream) /*@modifies fileSystem, *stream@*/ ; -extern int vfwprintf (FILE *stream, const wchar_t *format, va_list arg) +int vfwprintf (FILE *stream, const wchar_t *format, va_list arg) /*@modifies fileSystem, *stream@*/ ; -extern int vswprintf (wchar_t *s, size_t n, const wchar_t *format, va_list arg) +int vswprintf (wchar_t *s, size_t n, const wchar_t *format, va_list arg) /*@modifies *s@*/ ; -extern int vwprintf (const wchar_t *format, va_list arg) +int vwprintf (const wchar_t *format, va_list arg) /*@modifies fileSystem, *stdout@*/ ; -extern size_t wcrtomb (/*@null@*/ /*@out@*/ char *s, wchar_t wc, /*@null@*/ mbstate_t *ps) +size_t wcrtomb (/*@null@*/ /*@out@*/ char *s, wchar_t wc, /*@null@*/ mbstate_t *ps) /*@modifies *s@*/; -extern void /*@alt wchar_t *@*/ +void /*@alt wchar_t *@*/ wcscat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2) /*@modifies *s1@*/ ; -extern /*@exposed@*/ /*@null@*/ wchar_t * +/*@exposed@*/ /*@null@*/ wchar_t * wcschr (/*@returned@*/ const wchar_t *s, wchar_t c) /*@*/ ; -extern int wcscmp (const wchar_t *s1, const wchar_t *s2) /*@*/ ; +int wcscmp (const wchar_t *s1, const wchar_t *s2) /*@*/ ; -extern int wcscoll (const wchar_t *s1, const wchar_t *s2) /*@*/ ; +int wcscoll (const wchar_t *s1, const wchar_t *s2) /*@*/ ; -extern void /*@alt wchar_t *@*/ +void /*@alt wchar_t *@*/ wcscpy (/*@unique@*/ /*@out@*/ /*@returned@*/ wchar_t *s1, const wchar_t *s2) /*@modifies *s1@*/ ; -extern size_t wcscspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ; +size_t wcscspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ; -extern size_t wcsftime (/*@out@*/ wchar_t *s, size_t maxsize, const wchar_t *format, +size_t wcsftime (/*@out@*/ wchar_t *s, size_t maxsize, const wchar_t *format, const struct tm *timeptr) /*@modifies *s@*/ ; -extern size_t wcslen (const wchar_t *s) /*@*/ ; +size_t wcslen (const wchar_t *s) /*@*/ ; -extern void /*@alt wchar_t *@*/ +void /*@alt wchar_t *@*/ wcsncat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2, size_t n) /*@modifies *s1@*/ ; -extern int wcsncmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ; +int wcsncmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ; -extern void /*@alt wchar_t *@*/ +void /*@alt wchar_t *@*/ wcsncpy (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2, size_t n) /*@modifies *s1@*/ ; -extern /*@null@*/ wchar_t * +/*@null@*/ wchar_t * wcspbrk (/*@returned@*/ const wchar_t *s1, const wchar_t *s2) /*@*/ ; -extern /*@null@*/ wchar_t * +/*@null@*/ wchar_t * wcsrchr (/*@returned@*/ const wchar_t *s, wchar_t c) /*@*/ ; -extern size_t +size_t wcsrtombs (/*@null@*/ char *dst, const wchar_t **src, size_t len, /*@null@*/ mbstate_t *ps) /*@modifies *src@*/ ; -extern size_t wcsspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ; +size_t wcsspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ; -extern /*@null@*/ wchar_t *wcsstr (const wchar_t *s1, const wchar_t *s2) /*@*/ ; +/*@null@*/ wchar_t *wcsstr (const wchar_t *s1, const wchar_t *s2) /*@*/ ; -extern double wcstod (const wchar_t *nptr, /*@null@*/ wchar_t **endptr) +double wcstod (const wchar_t *nptr, /*@null@*/ wchar_t **endptr) /*@modifies *endptr@*/ ; -extern /*@null@*/ wchar_t * +/*@null@*/ wchar_t * wcstok (/*@null@*/ wchar_t *s1, const wchar_t *s2, wchar_t **ptr) /*@modifies *ptr@*/; -extern long wcstol (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base) +long wcstol (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base) /*@modifies *endptr@*/; -extern unsigned long +unsigned long wcstoul (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base) /*@modifies *endptr@*/; -extern size_t +size_t wcsxfrm (/*@null@*/ wchar_t *s1, const wchar_t *s2, size_t n) /*@modifies *s1@*/; -extern int wctob (wint_t c) /*@*/; +int wctob (wint_t c) /*@*/; -extern /*@null@*/ wchar_t *wmemchr (const wchar_t *s, wchar_t c, size_t n) /*@*/ ; +/*@null@*/ wchar_t *wmemchr (const wchar_t *s, wchar_t c, size_t n) /*@*/ ; -extern int wmemcmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ; +int wmemcmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ; -extern wchar_t *wmemcpy (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n) +wchar_t *wmemcpy (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n) /*@modifies *s1@*/; -extern wchar_t *wmemmove (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n) +wchar_t *wmemmove (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n) /*@modifies *s1@*/; -extern wchar_t *wmemset (/*@returned@*/ wchar_t *s, wchar_t c, size_t n) +wchar_t *wmemset (/*@returned@*/ wchar_t *s, wchar_t c, size_t n) /*@modifies *s@*/; -/*@printflike@*/ extern int wprintf (const wchar_t *format, ...) +/*@printflike@*/ int wprintf (const wchar_t *format, ...) /*@globals stdout@*/ /*@modifies errno, *stdout@*/; -/*@scanflike@*/ extern int +/*@scanflike@*/ int wscanf (const wchar_t *format, ...) /*@globals stdin@*/ /*@modifies errno, *stdin@*/; @@ -792,65 +799,65 @@ typedef /*@integraltype@*/ wctype_t; typedef /*@integraltype@*/ wctrans_t; # ifdef STRICT -extern lltX_bool iswalnum (wint_t c) /*@*/ ; -extern lltX_bool iswalpha (wint_t c) /*@*/ ; -extern lltX_bool iswcntrl (wint_t c) /*@*/ ; -extern lltX_bool iswctype (wint_t c, wctype_t ctg) /*@*/ ; -extern lltX_bool iswdigit (wint_t c) /*@*/ ; -extern lltX_bool iswgraph (wint_t c) /*@*/ ; -extern lltX_bool iswlower (wint_t c) /*@*/ ; -extern lltX_bool iswprint (wint_t c) /*@*/ ; -extern lltX_bool iswpunct (wint_t c) /*@*/ ; -extern lltX_bool iswspace (wint_t c) /*@*/ ; -extern lltX_bool iswupper (wint_t c) /*@*/ ; -extern lltX_bool iswxdigit (wint_t c) /*@*/ ; - -extern wint_t towctrans (wint_t c, wctrans_t ctg) /*@*/ ; -extern wint_t towlower (wint_t c) /*@*/ ; -extern wint_t towupper (wint_t c) /*@*/ ; +lltX_bool iswalnum (wint_t c) /*@*/ ; +lltX_bool iswalpha (wint_t c) /*@*/ ; +lltX_bool iswcntrl (wint_t c) /*@*/ ; +lltX_bool iswctype (wint_t c, wctype_t ctg) /*@*/ ; +lltX_bool iswdigit (wint_t c) /*@*/ ; +lltX_bool iswgraph (wint_t c) /*@*/ ; +lltX_bool iswlower (wint_t c) /*@*/ ; +lltX_bool iswprint (wint_t c) /*@*/ ; +lltX_bool iswpunct (wint_t c) /*@*/ ; +lltX_bool iswspace (wint_t c) /*@*/ ; +lltX_bool iswupper (wint_t c) /*@*/ ; +lltX_bool iswxdigit (wint_t c) /*@*/ ; + +wint_t towctrans (wint_t c, wctrans_t ctg) /*@*/ ; +wint_t towlower (wint_t c) /*@*/ ; +wint_t towupper (wint_t c) /*@*/ ; # else -extern lltX_bool /*@alt int@*/ iswalnum (wint_t c) /*@*/ ; -extern lltX_bool /*@alt int@*/ iswalpha (wint_t c) /*@*/ ; -extern lltX_bool /*@alt int@*/ iswcntrl (wint_t c) /*@*/ ; -extern lltX_bool /*@alt int@*/ iswctype (wint_t c, wctype_t ctg) /*@*/ ; -extern lltX_bool /*@alt int@*/ iswdigit (wint_t c) /*@*/ ; -extern lltX_bool /*@alt int@*/ iswgraph (wint_t c) /*@*/ ; -extern lltX_bool /*@alt int@*/ iswlower (wint_t c) /*@*/ ; -extern lltX_bool /*@alt int@*/ iswprint (wint_t c) /*@*/ ; -extern lltX_bool /*@alt int@*/ iswpunct (wint_t c) /*@*/ ; -extern lltX_bool /*@alt int@*/ iswspace (wint_t c) /*@*/ ; -extern lltX_bool /*@alt int@*/ iswupper (wint_t c) /*@*/ ; -extern lltX_bool /*@alt int@*/ iswxdigit (wint_t c) /*@*/ ; - -extern wint_t /*@alt int@*/ towctrans (wint_t c, wctrans_t ctg) /*@*/ ; -extern wint_t /*@alt int@*/ towlower (wint_t c) /*@*/ ; -extern wint_t /*@alt int@*/ towupper (wint_t c) /*@*/ ; +lltX_bool /*@alt int@*/ iswalnum (wint_t c) /*@*/ ; +lltX_bool /*@alt int@*/ iswalpha (wint_t c) /*@*/ ; +lltX_bool /*@alt int@*/ iswcntrl (wint_t c) /*@*/ ; +lltX_bool /*@alt int@*/ iswctype (wint_t c, wctype_t ctg) /*@*/ ; +lltX_bool /*@alt int@*/ iswdigit (wint_t c) /*@*/ ; +lltX_bool /*@alt int@*/ iswgraph (wint_t c) /*@*/ ; +lltX_bool /*@alt int@*/ iswlower (wint_t c) /*@*/ ; +lltX_bool /*@alt int@*/ iswprint (wint_t c) /*@*/ ; +lltX_bool /*@alt int@*/ iswpunct (wint_t c) /*@*/ ; +lltX_bool /*@alt int@*/ iswspace (wint_t c) /*@*/ ; +lltX_bool /*@alt int@*/ iswupper (wint_t c) /*@*/ ; +lltX_bool /*@alt int@*/ iswxdigit (wint_t c) /*@*/ ; + +wint_t /*@alt int@*/ towctrans (wint_t c, wctrans_t ctg) /*@*/ ; +wint_t /*@alt int@*/ towlower (wint_t c) /*@*/ ; +wint_t /*@alt int@*/ towupper (wint_t c) /*@*/ ; # endif -extern wctrans_t wctrans (const char *property) /*@*/ ; -extern wctype_t wctype (const char *property) /*@*/ ; +wctrans_t wctrans (const char *property) /*@*/ ; +wctype_t wctype (const char *property) /*@*/ ; -extern int mblen (char *s, size_t n) /*@*/ ; -extern int mbtowc (/*@null@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n) +int mblen (char *s, size_t n) /*@*/ ; +int mbtowc (/*@null@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n) /*@modifies *pwc@*/ ; -extern int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar) +int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar) /*@modifies *s@*/ ; -extern size_t mbstowcs (/*@out@*/ wchar_t *pwcs, char *s, size_t n) +size_t mbstowcs (/*@out@*/ wchar_t *pwcs, char *s, size_t n) /*@modifies *pwcs@*/ ; -extern size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n) +size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n) /*@modifies *s@*/ ; /* ** string.h */ -extern void /*@alt void * @*/ +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); @*/ ; -extern void /*@alt void * @*/ +void /*@alt void * @*/ memmove (/*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n) /*@modifies *s1@*/ /*@requires MaxRead(s2) >= (n - 1) /\ MaxSet(s1) >= (n - 1); @*/ @@ -861,22 +868,22 @@ extern void /*@alt void * @*/ modifed 12/29/2000 */ -extern void /*@alt char * @*/ +void /*@alt char * @*/ 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); @*/; -extern void /*@alt char * @*/ +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; @*/; -extern void /*@alt char * @*/ +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) );@*/; -extern void /*@alt char * @*/ +void /*@alt char * @*/ strncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, size_t n) /*@modifies *s1@*/ /*@requires MaxSet(s1) >= ( MaxRead(s1) + n); @*/ @@ -884,53 +891,53 @@ extern void /*@alt char * @*/ /*drl end*/ -extern int memcmp (void *s1, void *s2, size_t n) /*@*/ ; -extern int strcmp (char *s1, char *s2) /*@*/ ; -extern int strcoll (char *s1, char *s2) /*@*/ ; -extern int strncmp (char *s1, char *s2, size_t n) /*@*/ ; -extern size_t strxfrm (/*@out@*/ /*@null@*/ char *s1, char *s2, size_t n) +int memcmp (void *s1, void *s2, size_t n) /*@*/ ; +int strcmp (char *s1, char *s2) /*@*/ ; +int strcoll (char *s1, char *s2) /*@*/ ; +int strncmp (char *s1, char *s2, size_t n) /*@*/ ; +size_t strxfrm (/*@out@*/ /*@null@*/ char *s1, char *s2, size_t n) /*@modifies *s1@*/ ; /* s1 may be null only if n == 0 */ -extern /*@null@*/ void *memchr (void *s, int c, size_t n) /*@*/ ; +/*@null@*/ void *memchr (void *s, int c, size_t n) /*@*/ ; # ifdef STRICT -extern /*@exposed@*/ /*@null@*/ char * +/*@exposed@*/ /*@null@*/ char * strchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0 @*/ ; # else -extern /*@exposed@*/ /*@null@*/ char * +/*@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; @*/ ; # endif -extern size_t strcspn (char *s1, char *s2) /*@*/ ; -extern /*@null@*/ /*@exposed@*/ char * +size_t strcspn (char *s1, char *s2) /*@*/ ; +/*@null@*/ /*@exposed@*/ char * strpbrk (/*@returned@*/ char *s, char *t) /*@*/ ; # ifdef STRICT -extern /*@null@*/ /*@exposed@*/ char * +/*@null@*/ /*@exposed@*/ char * strrchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0 @*/ ; # else -extern /*@null@*/ /*@exposed@*/ char * +/*@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 @*/ ; # endif -extern size_t strspn (char *s, char *t) /*@*/ ; +size_t strspn (char *s, char *t) /*@*/ ; -extern /*@null@*/ /*@exposed@*/ char * +/*@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 @*/ ; -extern /*@null@*/ /*@exposed@*/ char * +/*@null@*/ /*@exposed@*/ char * strtok (/*@returned@*/ /*@null@*/ char *s, char *t) /*@modifies *s, internalState, errno@*/ ; -extern void /*@alt void *@*/ memset (/*@out@*/ /*@returned@*/ void *s, +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) @*/ ; -extern /*@observer@*/ char *strerror (int errnum) /*@*/ ; +/*@observer@*/ char *strerror (int errnum) /*@*/ ; /*drl */ -extern size_t strlen (char *s) /*@*/ /*@ensures result == MaxRead(s); @*/; +size_t strlen (char *s) /*@*/ /*@ensures result == MaxRead(s); @*/; /* ** time.h @@ -954,25 +961,25 @@ struct tm int tm_isdst; } ; -extern clock_t clock (void) /*@modifies internalState@*/ ; -extern double difftime (time_t time1, time_t time0) /*@*/ ; -extern time_t mktime (struct tm *timeptr) /*@*/ ; +clock_t clock (void) /*@modifies internalState@*/ ; +double difftime (time_t time1, time_t time0) /*@*/ ; +time_t mktime (struct tm *timeptr) /*@*/ ; -extern time_t time (/*@null@*/ /*@out@*/ time_t *tp) +time_t time (/*@null@*/ /*@out@*/ time_t *tp) /*@modifies *tp@*/ ; -extern /*@observer@*/ char *asctime (struct tm *timeptr) +/*@observer@*/ char *asctime (struct tm *timeptr) /*@modifies errno*/ /*@ensures MaxSet(result) == 25 /\ MaxRead(result) == 25; @*/ ; -extern /*@observer@*/ char *ctime (time_t *tp) /*@*/ +/*@observer@*/ char *ctime (time_t *tp) /*@*/ /*@ensures MaxSet(result) == 25 /\ MaxRead(result) == 25; @*/; -extern /*@null@*/ /*@observer@*/ struct tm *gmtime (time_t *tp) /*@*/ ; +/*@null@*/ /*@observer@*/ struct tm *gmtime (time_t *tp) /*@*/ ; -extern /*@null@*/ /*@observer@*/ struct tm *localtime (time_t *tp) +/*@null@*/ /*@observer@*/ struct tm *localtime (time_t *tp) /*@modifies errno@*/ ; -extern size_t strftime (/*@out@*/ char *s, size_t smax, +size_t strftime (/*@out@*/ char *s, size_t smax, char *fmt, struct tm *timeptr) /*@modifies *s@*/ ; diff --git a/lib/unix.h b/lib/unix.h index 769b88a..2500fdd 100644 --- a/lib/unix.h +++ b/lib/unix.h @@ -903,9 +903,9 @@ truncate (const char *name, off_t length) /*@constant int ENEEDAUTH@*/ /*@constant int ELAST@*/ -/*________________________________________________________________________ - * tar.h - */ +/* +** tar.h +*/ /*@unchecked@*/ extern char *TMAGIC; /*@constant int TMAGLEN@*/ @@ -957,9 +957,9 @@ struct ipc_perm { /*@constant int IPC_SET@*/ /*@constant int IPC_STAT@*/ -/*________________________________________________________________________ - * sys/msg.h - */ +/* +** sys/msg.h +*/ struct msqid_ds { struct ipc_perm msg_perm; /* msg queue permission bits */ @@ -1002,9 +1002,9 @@ msgrcv (int id, /*@out@*/ void *ptr, size_t nbytes, long type, int flags) msgsnd (int id, const void *ptr, size_t nbytes, int flag) /*@modifies errno@*/; -/*________________________________________________________________________ - * sys/sem.h - */ +/* +** sys/sem.h +*/ struct semid_ds { struct ipc_perm sem_perm; @@ -1066,9 +1066,9 @@ semget (key_t key, int nsems, int flag) semop (int id, struct sembuf *semoparray, size_t nops) /*@modifies errno@*/; -/*________________________________________________________________________ - * sys/shm.h - */ +/* +** sys/shm.h +*/ struct shmid_ds { struct ipc_perm shm_perm; @@ -1095,25 +1095,155 @@ semop (int id, struct sembuf *semoparray, size_t nops) /*@constant int SHM_W@*/ /*@constant int SHM_UNLOCK@*/ - void * -shmat (int id, /*@null@*/ void *addr, int flag) - /*@modifies errno@*/; +void * shmat (int id, /*@null@*/ void *addr, int flag) + /*@modifies errno@*/ ; + +extern int shmctl (int id, int cmd, /*@out@*/ struct shmid_ds *buf) + /*@modifies errno, *buf@*/ ; - extern int -shmctl (int id, int cmd, /*@out@*/ struct shmid_ds *buf) - /*@modifies errno, *buf@*/; +extern int shmdt (void *addr) + /*@modifies errno@*/ ; - extern int -shmdt (void *addr) - /*@modifies errno@*/; +extern int shmget (key_t key, int size, int flag) + /*@modifies errno@*/ ; - extern int -shmget (key_t key, int size, int flag) - /*@modifies errno@*/; +# if 0 + /* + ** this is in stdio.h! + */ -/*________________________________________________________________________ - * syslog.h - */ +/* +** stdio.h +*/ + +/* +** evans 2001-12-30: added from http://www.opengroup.org/onlinepubs/007908799/xsh/stdio.h.html +*/ + +/*@constant unsignedintegraltype BUFSIZ@*/ +/*@constant unsignedintegraltype FILENAME_MAX@*/ +/*@constant unsignedintegraltype FOPEN_MAX@*/ +/*@constant bool _IOFBF@*/ +/*@constant bool _IOLBF@*/ +/*@constant bool _IONBF@*/ +/*@constant unsignedintegraltype L_ctermid@*/ +/*@constant unsignedintegraltype L_cuserid@*/ +/*@constant unsignedintegraltype L_tmpnam@*/ +/*@constant unsignedintegraltype SEEK_CUR@*/ +/*@constant unsignedintegraltype SEEK_END@*/ +/*@constant unsignedintegraltype SEEK_SET@*/ +/*@constant unsignedintegraltype TMP_MAX@*/ + +/* EOF */ +/* NULL */ + +/*@constant observer char *P_tmpdir@*/ + +/*@dependent@*/ char *ctermid (/*@returned@*/ /*@null@*/ char *) /*@*/ ; + /* Result may be static pointer if parameter is NULL, otherwise is fresh. */ + +char *cuserid (/*@null@*/ /*@returned@*/ char *) + /*@warn legacy "cuserid is obsolete"@*/ /*@*/ ; + +/*@null@*/ FILE *fdopen (int, const char *) + /*@modifies errno, fileSystem@*/ ; + +int fileno (/*@notnull@*/ FILE *) + /*:errorcode -1:*/ + /*@modifies errno@*/ ; + +void flockfile (/*@notnull@*/ FILE *f) + /*@modifies f, fileSystem@*/ ; + +int fseeko (FILE *stream, off_t offset, int whence) + /*:errorcode -1:*/ + /*@modifies stream, errno@*/ ; + +off_t ftello(FILE *stream) + /*:errorcode -1:*/ /*@modifies errno*/ ; + +int ftrylockfile(FILE *stream) + /*:errorcode !0:*/ + /*@modifies stream, fileSystem, errno*/ ; + +void funlockfile (FILE *stream) + /*@modifies stream, fileSystem*/ ; + +int getc_unlocked(FILE *stream) + /*@warn multithreaded "getc_unlocked is a thread unsafe version of getc"@*/ + /*@modifies *stream, fileSystem, errno@*/ ; + +int getchar_unlocked (void) + /*@warn multithreaded "getchar_unlocked is a thread unsafe version of getchar"@*/ + /*@globals stdin@*/ + /*@modifies *stdin, fileSystem@*/ ; + +int getopt (int, char * const[], const char) + /*@warn legacy@*/ ; + +int getw (FILE *stream) + /*:errorcode EOF:*/ + /*@modifies fileSystem, *stream, errno@*/ ; + +int pclose(FILE *stream) + /*:errorcode -1:*/ + /*@modifies *stream, errno@*/ ; + +/*@null@*/ FILE *popen (const char *command, const char *mode) + /*:errorcode NULL:*/ + /*@modifies fileSystem, errno@*/ ; + +int putc_unlocked (int, FILE *stream) + /*@warn multithreaded "putc_unlocked is a thread unsafe version of putc"@*/ + /*:errorcode EOF:*/ + /*@modifies fileSystem, *stream, errno@*/ ; + +int putchar_unlocked(int) + /*@warn multithreaded "putchar_unlocked is a thread unsafe version of putchar"@*/ + /*:errorcode EOF:*/ + /*@modifies fileSystem, *stdout, errno@*/ ; + +int putw(int, FILE *stream) + /*:errorcode EOF:*/ + /*@modifies fileSystem, *stdout, errno@*/ ; + +int remove (const char *) + /*@modifies fileSystem@*/ ; + +int rename (const char *, const char *) + /*@modifies fileSystem@*/ ; + +void rewind (FILE *stream) + /*@modifies *stream@*/ ; + +void setbuf (FILE *stream, /*@null@*/ char *buf); + int setvbuf(FILE *, char *, int, size_t); + int snprintf(char *, size_t, const char *, ...); + int sprintf(char *, const char *, ...); + int sscanf(const char *, const char *, int ...); + char *tempnam(const char *, const char *); + FILE *tmpfile(void); + char *tmpnam(char *); + int ungetc(int, FILE *); + int vfprintf(FILE *, const char *, va_list); + int vprintf(const char *, va_list); + int vsnprintf(char *, size_t, const char *, va_list); + int vsprintf(char *, const char *, va_list); + + + The following external variables are defined: + + + extern char *optarg; ) + extern int opterr; ) + extern int optind; ) (LEGACY) + extern int optopt; ) + +# endif + +/* +** syslog.h +*/ /*@constant int LOG_EMERG@*/ /*@constant int LOG_ALERT@*/ diff --git a/src/flags.def b/src/flags.def index 5ef7203..0644a83 100644 --- a/src/flags.def +++ b/src/flags.def @@ -3823,5 +3823,13 @@ static flaglist flags = "Use of a declarator that is implementation optional, not required by ISO99.", 0, 0 }, + { + FK_WARNUSE, FK_NONE, modeFlag, + "legacy", + FLG_LEGACY, + "legacy declaration in Unix Standard", + "Use of a declarator that is marked as a legacy entry in the Unix Standard.", + 0, 0 + }, } ; diff --git a/test/help.expect b/test/help.expect index 4afc528..c79e014 100644 --- a/test/help.expect +++ b/test/help.expect @@ -255,6 +255,7 @@ Finished checking --- no code processed lclexpect lclimportdir lcs + legacy lh libmacros likelybool @@ -1080,4 +1081,5 @@ unixstandard --- function is not required in Standard UNIX Specification superuser --- function is restricted to superusers implementationoptional --- declarator is implementation optional (ISO99 does not require an implementation to provide it) +legacy --- legacy declaration in Unix Standard -- 2.45.2