Added legacy flag for unix lib.

diff --git a/lib/ansi.h b/lib/ansi.h
index 2e91a4ecbe288625e2b1dd0b183b9be171ec1966..1d49737a76375f2dd4efed0b3d2b376333391363 100644 (file)
--- 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 769b88add2b43a963b16c0a3dfc31315f66ae185..2500fdd50eef9463444721df02a7430ddd595646 100644 (file)
--- 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 5ef72038db9c7ac026fda87646377bdb520d2f19..0644a8372c0b7ac0dd344c52e4161241722372d2 100644 (file)
--- 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 4afc5281a9160683157228e62304fc9275fe9656..c79e0140b8d5878aa758b8b31c41261281b5f7f7 100644 (file)
--- 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