home *** CD-ROM | disk | FTP | other *** search
/ OS/2 Shareware BBS: 10 Tools / 10-Tools.zip / splint3s.zip / splint-3.0.1.6 / lib / ansi.h next >
C/C++ Source or Header  |  2002-02-13  |  33KB  |  1,102 lines
  1. /*
  2. ** satndard.h --- ISO C99 Standard Library for Splint.
  3. **
  4. ** Process with -DSTRICT to get strict library.
  5. */
  6.  
  7. /*@-nextlinemacros@*/
  8. /*@+allimponly@*/
  9. /*@+globsimpmodifiesnothing@*/
  10.  
  11. /*
  12. ** errno.h
  13. */
  14.  
  15. /*@constant int EDOM;@*/
  16. /*@constant int ERANGE;@*/
  17. /*@constant int EILSEQ;@*/
  18.  
  19. # ifdef STRICT
  20. /*@checkedstrict@*/ int errno;
  21. # else 
  22. /*@unchecked@*/ int errno;
  23. # endif
  24.  
  25. /*
  26. ** types 
  27. */
  28.  
  29. typedef /*@integraltype@*/ ptrdiff_t;    
  30. typedef /*@unsignedintegraltype@*/ size_t;
  31. typedef /*@signedintegraltype@*/ ssize_t;
  32. typedef /*@integraltype@*/ wchar_t;
  33.  
  34. /*
  35. ** Added by Amendment 1 to ISO.
  36. */
  37.  
  38. typedef /*@integraltype@*/ wint_t;
  39. typedef /*@abstract@*/ mbstate_t;
  40.  
  41. /*@constant null anytype NULL = 0;@*/
  42.  
  43. /*
  44. ** assert.h
  45. */
  46.  
  47. /*@constant lltX_bool NDEBUG;@*/
  48.  
  49. # ifdef STRICT
  50. /*@falseexit@*/ void assert (/*@sef@*/ lltX_bool e) 
  51.   /*@*/ ;
  52. # else
  53. /*@falseexit@*/ void assert (/*@sef@*/ lltX_bool /*@alt int@*/ e) 
  54.   /*@*/ ;
  55. # endif
  56.  
  57.  
  58. /*
  59. ** ctype.h
  60. */
  61.  
  62. # ifdef STRICT
  63. lltX_bool isalnum (int c) /*@*/ ;
  64. lltX_bool isalpha (int c) /*@*/ ;
  65. lltX_bool iscntrl (int c) /*@*/ ;
  66. lltX_bool isdigit (int c) /*@*/ ;
  67. lltX_bool isgraph (int c) /*@*/ ;
  68. lltX_bool islower (int c) /*@*/ ;
  69. lltX_bool isprint (int c) /*@*/ ;
  70. lltX_bool ispunct (int c) /*@*/ ;
  71. lltX_bool isspace (int c) /*@*/ ;
  72. lltX_bool isupper (int c) /*@*/ ;
  73. lltX_bool isxdigit (int c) /*@*/ ;
  74. char tolower (int c) /*@*/ ;
  75. char toupper (int c) /*@*/ ;
  76. # else
  77. /*
  78. ** evans 2002-01-03: added alt char (was alt unsigned char)
  79. */
  80.  
  81. lltX_bool /*@alt int@*/ isalnum (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  82. lltX_bool /*@alt int@*/ isalpha (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  83. lltX_bool /*@alt int@*/ iscntrl (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  84. lltX_bool /*@alt int@*/ isdigit (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  85. lltX_bool /*@alt int@*/ isgraph (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  86. lltX_bool /*@alt int@*/ islower (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  87. lltX_bool /*@alt int@*/ isprint (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  88. lltX_bool /*@alt int@*/ ispunct (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  89. lltX_bool /*@alt int@*/ isspace (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  90. lltX_bool /*@alt int@*/ isupper (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  91. lltX_bool /*@alt int@*/ isxdigit (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  92. char /*@alt int@*/ tolower (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  93. char /*@alt int@*/ toupper (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  94. # endif
  95.  
  96. /*
  97. ** locale.h
  98. */
  99.  
  100. struct lconv
  101. {
  102.   char *decimal_point;
  103.   char *thousands_sep;
  104.   char *grouping;
  105.   char *int_curr_symbol;
  106.   char *currency_symbol;
  107.   char *mon_decimal_point;
  108.   char *mon_thousands_sep;
  109.   char *mon_grouping;
  110.   char *positive_sign;
  111.   char *negative_sign;
  112.   char int_frac_digits;
  113.   char frac_digits;
  114.   char p_cs_precedes;
  115.   char p_sep_by_space;
  116.   char n_cs_precedes;
  117.   char n_sep_by_space;
  118.   char p_sign_posn;
  119.   char n_sign_posn;
  120. } ;
  121.  
  122. /*@constant int LC_ALL;@*/
  123. /*@constant int LC_COLLATE;@*/
  124. /*@constant int LC_CTYPE;@*/
  125. /*@constant int LC_MONETARY;@*/
  126. /*@constant int LC_NUMERIC;@*/
  127. /*@constant int LC_TIME;@*/
  128.  
  129. /*@observer@*/ /*@null@*/ char *setlocale (int category, /*@null@*/ char *locale) 
  130.    /*@modifies internalState, errno@*/ ;
  131.  
  132. struct lconv *localeconv (void) /*@*/ ;
  133.  
  134. /*
  135. ** float.h
  136. */
  137.  
  138. /*
  139. ** Note, these are defined by macros, but NOT necessarily
  140. ** constants.  They may be used as lvalues.
  141. */
  142.  
  143. /*@unchecked@*/ int    DBL_DIG;
  144. /*@unchecked@*/ double DBL_EPSILON;
  145. /*@unchecked@*/ int    DBL_MANT_DIG;
  146. /*@unchecked@*/ double DBL_MAX;
  147. /*@unchecked@*/ int    DBL_MAX_10_EXP;
  148. /*@unchecked@*/ int    DBL_MAX_EXP;
  149. /*@unchecked@*/ double DBL_MIN;
  150. /*@unchecked@*/ int    DBL_MIN_10_EXP;
  151. /*@unchecked@*/ int    DBL_MIN_EXP;
  152.  
  153. /*@unchecked@*/ int   FLT_DIG;
  154. /*@unchecked@*/ float FLT_EPSILON;
  155. /*@unchecked@*/ int   FLT_MANT_DIG;
  156. /*@unchecked@*/ float FLT_MAX;
  157. /*@unchecked@*/ int   FLT_MAX_10_EXP;
  158. /*@unchecked@*/ int   FLT_MAX_EXP;
  159. /*@unchecked@*/ float FLT_MIN;
  160. /*@unchecked@*/ int   FLT_MIN_10_EXP;
  161. /*@unchecked@*/ int   FLT_MIN_EXP;
  162. /*@constant            int   FLT_RADIX@*/
  163. /*@unchecked@*/ int   FLT_ROUNDS;
  164.  
  165. /*@unchecked@*/ int         LDBL_DIG;
  166. /*@unchecked@*/ long double LDBL_EPSILON;
  167. /*@unchecked@*/ int         LDBL_MANT_DIG;
  168. /*@unchecked@*/ long double LDBL_MAX;
  169. /*@unchecked@*/ int         LDBL_MAX_10_EXP;
  170. /*@unchecked@*/ int         LDBL_MAX_EXP;
  171. /*@unchecked@*/ long double LDBL_MIN;
  172. /*@unchecked@*/ int         LDBL_MIN_10_EXP;
  173. /*@unchecked@*/ int         LDBL_MIN_EXP;
  174.  
  175. /*
  176. ** limits.h
  177. */
  178.  
  179. /*@constant int CHAR_BIT; @*/
  180. /*@constant char CHAR_MAX; @*/
  181. /*@constant char CHAR_MIN; @*/
  182. /*@constant int INT_MAX; @*/
  183. /*@constant int INT_MIN; @*/
  184. /*@constant long int LONG_MAX; @*/
  185. /*@constant long int LONG_MIN; @*/
  186. /*@constant long int MB_LEN_MAX@*/
  187. /*@constant signed char SCHAR_MAX; @*/
  188. /*@constant signed char SCHAR_MIN; @*/
  189. /*@constant short SHRT_MAX; @*/
  190. /*@constant short SHRT_MIN; @*/
  191. /*@constant unsigned char UCHAR_MAX; @*/
  192. /*@constant unsigned char UCHAR_MIN; @*/
  193. /*@constant unsigned int UINT_MAX; @*/
  194. /*@constant unsigned long ULONG_MAX; @*/
  195. /*@constant unsigned short USHRT_MAX; @*/
  196.  
  197. /*
  198. ** math.h
  199. */
  200.  
  201. /*@constant double HUGE_VAL; @*/
  202.  
  203. /*
  204. ** math functions that may have a range error modify errno 
  205. */
  206.  
  207. double sin (double x) /*@*/ ;
  208. double cos (double x) /*@*/ ;
  209. double tan (double x) /*@*/ ;
  210. double asin (double x) /*@modifies errno@*/ ;
  211. double acos (double x) /*@modifies errno@*/ ;
  212. double atan (double x) /*@*/ ;
  213. double atan2 (double y, double x) /*@*/ ;
  214. double sinh (double x) /*@*/ ;
  215. double cosh (double x) /*@modifies errno@*/ ;
  216. double tanh (double x) /*@*/ ;
  217.  
  218. double exp (double x) /*@modifies errno@*/ ;
  219. double ldexp (double x, int n) /*@modifies errno@*/ ;
  220. double frexp (double x, /*@out@*/ int *xp) /*@modifies *xp;@*/ ;
  221.  
  222. double log (double x) /*@modifies errno@*/ ;
  223. double log10 (double x) /*@modifies errno@*/ ;
  224.  
  225. double pow (double x, double y) /*@modifies errno@*/ ;
  226. double sqrt (double x) /*@modifies errno@*/ ;
  227.  
  228. double ceil (double x) /*@*/ ;
  229. double floor (double x) /*@*/ ;
  230. double fabs (double x) /*@*/ ;
  231.  
  232. double modf (double x, /*@out@*/ double *ip) /*@modifies *ip;@*/ ;
  233. double fmod (double x, double y) /*@*/ ;
  234.  
  235. /*
  236. ** These functions are optional in iso C.  An implementation does not
  237. ** have to provide them.  They are included in comments here, but
  238. ** are not required to be part of the standard library.
  239. */
  240.  
  241. # ifdef OPTIONAL_MATH
  242.  
  243. float acosf (float x) /*@modifies errno@*/ ;
  244. long double acosl (long double x) /*@modifies errno@*/ ;
  245. float asinf (float x)    /*@modifies errno@*/ ;
  246. long double asinl (long double x) /*@modifies errno@*/ ;
  247. float atanf (float x)    /*@*/ ;
  248. long double atanl (long double x) /*@*/ ;
  249. float atan2f (float y, float x) /*@*/ ;
  250. long double atan2l (long double y, long double x) /*@*/ ;
  251. float ceilf (float x)    /*@*/ ;
  252. long double ceill (long double x) /*@*/ ;
  253. float cosf (float x) /*@*/ ;
  254. long double cosl (long double x) /*@*/ ;
  255. float coshf (float x)    /*@modifies errno@*/ ;
  256. long double coshl (long double x) /*@modifies errno@*/ ;
  257. float expf (float x) /*@modifies errno@*/ ;
  258. long double expl (long double x) /*@modifies errno@*/;
  259. float fabsf (float x)    /*@*/ ;
  260. long double fabsl (long double x) /*@*/ ;
  261. float floorf (float x) /*@*/ ;
  262. long double floorl (long double x) /*@*/ ;
  263. float fmodf (float x, float y) /*@*/ ;
  264. long double fmodl (long double x, long double y)    /*@*/ ;
  265. float frexpf (float x, /*@out@*/ int *xp) /*@modifies *xp@*/;
  266. long double frexpl (long double x, /*@out@*/ int *xp) /*@modifies *xp@*/;
  267. float ldexpf (float x, int n) /*@modifies errno@*/ ;
  268. long double ldexpl (long double x, int n) /*@modifies errno@*/ ;
  269. float logf (float x) /*@modifies errno@*/ ;
  270. long double logl (long double x) /*@modifies errno@*/ ;
  271. float log10f (float x) /*@modifies errno@*/;
  272. long double log10l (long double x) /*@modifies errno@*/;
  273. float modff (float x, /*@out@*/ float *xp) /*@modifies *xp@*/ ;
  274. long double modfl (long double x, /*@out@*/ long double *xp) /*@modifies *xp@*/ ;
  275. float powf (float x, float y) /*@modifies errno@*/ ;
  276. long double powl (long double x, long double y) /*@modifies errno@*/ ;
  277. float sinf (float x) /*@*/ ;
  278. long double sinl (long double x)    /*@*/ ;
  279. float sinhf (float x) /*@*/ ;
  280. long double sinhl (long double x) /*@*/ ;
  281. float sqrtf (float x) /*@modifies errno@*/ ;
  282. long double sqrtl (long double x) /*@modifies errno@*/ ;
  283. float tanf (float x) /*@*/ ;
  284. long double tanl (long double x)    /*@*/ ;
  285. float tanhf (float x) /*@*/ ;
  286. long double tanhl (long double x) /*@*/ ;
  287.  
  288. # endif
  289.  
  290. /*
  291. ** setjmp.h
  292. */
  293.  
  294. typedef /*@abstract@*/ /*@mutable@*/ void *jmp_buf;
  295.  
  296. int setjmp (/*@out@*/ jmp_buf env) /*@modifies env;@*/ ;
  297. /*@mayexit@*/ void longjmp (jmp_buf env, int val) /*@*/ ;
  298.  
  299. /*
  300. ** signal.h
  301. */
  302.  
  303. /*@constant int SIGABRT; @*/
  304. /*@constant int SIGFPE; @*/
  305. /*@constant int SIGILL; @*/
  306. /*@constant int SIGINT; @*/
  307. /*@constant int SIGSEGV; @*/
  308. /*@constant int SIGTERM; @*/
  309.  
  310. typedef /*@integraltype@*/ sig_atomic_t;
  311.  
  312. /*@constant void (*SIG_DFL)(int); @*/
  313. /*@constant void (*SIG_ERR)(int); @*/
  314. /*@constant void (*SIG_IGN)(int); @*/
  315.  
  316. /*
  317. ** signal takes an int, and a function takes int returns void, and
  318. ** returns the function (or NULL if unsuccessful).
  319. */
  320.  
  321. /*@null@*/ void (*signal (int sig, /*@null@*/ void (*func)(int))) (int) 
  322.    /*@modifies internalState, errno;@*/ ;
  323.  
  324. /*@mayexit@*/ int raise (int sig) ;
  325.  
  326. /*
  327. ** stdarg.h
  328. */
  329.  
  330. typedef /*@abstract@*/ /*@mutable@*/ void *va_list;
  331.  
  332. void va_start (/*@out@*/ va_list ap, ...) /*@modifies ap;@*/ ;
  333. void va_end (va_list va) /*@modifies va;@*/ ;
  334.  
  335. /*
  336. ** va_arg is builtin
  337. */
  338.  
  339. /*
  340. ** stdio.h
  341. */
  342.  
  343. typedef /*@abstract@*/ /*@mutable@*/ void *FILE;
  344. typedef /*@abstract@*/ /*@mutable@*/ void *fpos_t;
  345.  
  346. /*@constant int _IOFBF; @*/
  347. /*@constant int _IOLBF; @*/
  348. /*@constant int _IONBF; @*/
  349.  
  350. /*@constant int BUFSIZ; @*/
  351. /*@constant int EOF; @*/
  352.  
  353. /*@constant int FOPEN_MAX; @*/
  354. /*@constant int FILENAME_MAX; @*/
  355.  
  356. /*@constant int L_tmpnam; @*/
  357.  
  358. /*@constant int SEEK_CUR; @*/
  359. /*@constant int SEEK_END; @*/
  360. /*@constant int SEEK_SET; @*/
  361.  
  362. /*@constant int TMP_MAX; @*/
  363.  
  364. # ifdef STRICT
  365. /*@checked@*/ FILE *stderr;
  366. /*@checked@*/ FILE *stdin;
  367. /*@checked@*/ FILE *stdout;
  368. # else
  369. /*@unchecked@*/ FILE *stderr;
  370. /*@unchecked@*/ FILE *stdin;
  371. /*@unchecked@*/ FILE *stdout;
  372. # endif
  373.  
  374. int remove (char *filename) /*@modifies fileSystem, errno@*/ ;
  375. int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ;
  376.  
  377. /*@null@*/ FILE *tmpfile (void) /*@modifies fileSystem@*/ ;
  378. /*@observer@*/ char *
  379.   tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s) 
  380.   /*@modifies *s, internalState@*/ ;
  381.  
  382. int fclose (FILE *stream) /*@modifies *stream, errno, fileSystem;@*/ ;
  383. int fflush (/*@null@*/ FILE *stream) 
  384.    /*@modifies *stream, errno, fileSystem;@*/ ;
  385.  
  386. /*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode) 
  387.    /*@modifies fileSystem@*/ ;         
  388.  
  389. /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream) 
  390.   /*@modifies *stream, fileSystem, errno@*/ ;
  391.  
  392.   extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf) 
  393.    /*@modifies fileSystem, *stream, *buf@*/ ;
  394.  
  395.    extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf, 
  396.             int mode, size_t size)
  397.    /*@modifies fileSystem, *stream, *buf@*/ ;
  398.  
  399. # ifdef STRICT
  400. /*@printflike@*/ 
  401. int fprintf (FILE *stream, char *format, ...)
  402.    /*@modifies fileSystem, *stream@*/ ;
  403. # else
  404. /*@printflike@*/ 
  405. int /*@alt void@*/ fprintf (FILE *stream, char *format, ...)
  406.    /*@modifies fileSystem, *stream@*/ ;
  407. # endif
  408.  
  409. /*@scanflike@*/ 
  410. int fscanf (FILE *stream, char *format, ...)
  411.    /*@modifies fileSystem, *stream@*/ ;
  412.  
  413. # ifdef STRICT
  414. /*@printflike@*/ 
  415. int printf (char *format, ...) 
  416.    /*@globals stdout@*/
  417.    /*@modifies fileSystem, *stdout@*/ ;
  418. # else
  419. /*@printflike@*/ 
  420. int /*@alt void@*/ printf (char *format, ...) 
  421.    /*@globals stdout@*/
  422.    /*@modifies fileSystem, *stdout@*/ ;
  423. # endif
  424.  
  425. /*@scanflike@*/
  426. int scanf(char *format, ...)
  427.    /*@globals stdin@*/
  428.    /*@modifies fileSystem, *stdin@*/ ;
  429.  
  430. # ifdef STRICT
  431. /*@printflike@*/ 
  432. int sprintf (/*@out@*/ char *s, char *format, ...) 
  433.    /*@modifies *s@*/ ;
  434. # else
  435. /*@printflike@*/ 
  436. int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...) 
  437.    /*@modifies *s@*/ ;
  438. # endif
  439.  
  440. /*@scanflike@*/ 
  441. int sscanf (/*@out@*/ char *s, char *format, ...) /*@*/ ;
  442.    /* modifies extra arguments */
  443.  
  444. int vprintf (const char *format, va_list arg)
  445.    /*@globals stdout@*/
  446.    /*@modifies fileSystem, *stdout@*/ ;
  447.  
  448. int vfprintf (FILE *stream, char *format, va_list arg)
  449.    /*@modifies fileSystem, *stream, arg, errno@*/ ;
  450.  
  451. int vsprintf (/*@out@*/ char *str, const char *format, va_list ap)
  452.      /*@warn bufferoverflowhigh "Use vsnprintf instead"@*/
  453.      /*@modifies str@*/ ;
  454.  
  455. int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap)
  456.      /*@requires maxSet(str) >= size@*/
  457.      /*@modifies str@*/ ;
  458.  
  459. int fgetc (FILE *stream) 
  460.    /*@modifies fileSystem, *stream, errno@*/ ;
  461.  
  462. /*@null@*/ char *
  463.   fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream)
  464.      /*@modifies fileSystem, *s, *stream, errno@*/
  465.      /*@requires maxSet(s) >= (n -1); @*/
  466.      /*@ensures maxRead(s) <= (n -1) /\ maxRead(s) >= 0; @*/
  467.      ;
  468.  
  469. int fputc (int /*@alt char@*/ c, FILE *stream)
  470.   /*:errorcode EOF:*/
  471.   /*@modifies fileSystem, *stream, errno@*/ ;
  472.  
  473. int fputs (char *s, FILE *stream)
  474.   /*@modifies fileSystem, *stream@*/ ;
  475.  
  476. /* note use of sef --- stream may be evaluated more than once */
  477. int getc (/*@sef@*/ FILE *stream)
  478.   /*@modifies fileSystem, *stream@*/ ;
  479.  
  480. int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/ ;
  481.  
  482. /*@null@*/ char *gets (/*@out@*/ char *s) 
  483.    /*@warn bufferoverflowhigh
  484.            "Use of gets leads to a buffer overflow vulnerability.  Use fgets instead"@*/
  485.    /*@globals stdin@*/ /*@modifies fileSystem, *s, *stdin, errno@*/ ;
  486.  
  487. int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
  488.    /*:errorcode EOF:*/
  489.    /*@modifies fileSystem, *stream;@*/ ;
  490.  
  491. int putchar (int /*@alt char@*/ c)
  492.    /*:errorcode EOF:*/
  493.    /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ; 
  494.  
  495. int puts (const char *s)
  496.    /*:errorcode EOF:*/
  497.    /*@globals stdout@*/
  498.    /*@modifies fileSystem, *stdout@*/ ; 
  499.  
  500. int ungetc (int /*@alt char@*/ c, FILE *stream)
  501.   /*@modifies fileSystem, *stream, errno@*/ ;
  502.  
  503. size_t 
  504.   fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream)
  505.   /*@modifies fileSystem, *ptr, *stream, errno@*/ ;
  506.  
  507. size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream)
  508.   /*@modifies fileSystem, *stream, errno@*/ ;
  509.  
  510. int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos)
  511.   /*@modifies *pos, errno@*/ ;
  512.  
  513. int fseek (FILE *stream, long int offset, int whence)
  514.    /*:errorcode -1:*/
  515.    /*@modifies fileSystem, *stream, errno@*/ ;
  516.  
  517. int fsetpos (FILE *stream, fpos_t *pos)
  518.    /*@modifies fileSystem, *stream, errno@*/ ;
  519.  
  520. long int ftell(FILE *stream) 
  521.    /*:errorcode -1:*/ /*@modifies errno*/ ;
  522.  
  523. void rewind (FILE *stream) /*@modifies *stream@*/ ;
  524. void clearerr (FILE *stream) /*@modifies *stream@*/ ;
  525.  
  526. int feof (FILE *stream) /*@modifies errno@*/ ;
  527. int ferror (FILE *stream) /*@modifies errno@*/ ;
  528.  
  529. void perror (/*@null@*/ char *s) 
  530.    /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ; 
  531.  
  532. /*
  533. ** stdlib.h
  534. */
  535.  
  536. double atof (char *s) /*@*/ ;
  537. int atoi (char *s) /*@*/ ;
  538. long int atol (char *s) /*@*/ ;
  539.  
  540. double strtod (char *s, /*@null@*/ /*@out@*/ char **endp)
  541.   /*@modifies *endp, errno@*/ ;
  542.  
  543. long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
  544.   /*@modifies *endp, errno@*/ ;
  545.  
  546. unsigned long 
  547.   strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
  548.   /*@modifies *endp, errno@*/ ;
  549.  
  550. /*@constant int RAND_MAX; @*/
  551. int rand (void) /*@modifies internalState@*/ ;
  552. void srand (unsigned int seed) /*@modifies internalState@*/ ;
  553.  
  554. /*
  555.   drl
  556.   changed 12/29/2000
  557. */
  558.  
  559. /*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/
  560.      /*@ensures maxSet(result) == (nobj - 1); @*/ ;
  561. /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@*/
  562.      /*@ensures maxSet(result) == (size - 1); @*/ ;
  563.  
  564. /*end drl changed */
  565.      
  566. /* 11 June 1997: removed out on return value */
  567.  
  568. # if 0
  569. /*@null@*/ /*@only@*/ void *
  570.    realloc (/*@null@*/ /*@only@*/ /*@special@*/ void *p, 
  571.         size_t size) /*@releases p@*/ /*@modifies *p@*/
  572.      /*@ensures maxSet(result) == (size - 1) @*/;
  573. # endif
  574.  
  575. /*
  576. ** LCLint annotations cannot fully describe realloc.  The semantics we
  577. ** want are:
  578. **    realloc returns null: ownership of parameter is not changed
  579. **    realloc returns non-null: ownership of parameter is transferred to return value
  580. **
  581. ** Otherwise, storage is in the same state before and after the call.
  582. */
  583.  
  584. /*@null@*/ /*@only@*/ void *
  585.    realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size) 
  586.      /*@modifies *p@*/ /*@ensures maxSet(result) >= (size - 1) @*/;
  587.  
  588. void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies p@*/ ;
  589.  
  590. /*@constant int EXIT_FAILURE; @*/ 
  591. /*@constant int EXIT_SUCCESS; @*/ 
  592.  
  593. /*@exits@*/ void abort (void) /*@*/ ;
  594. /*@exits@*/ void exit (int status) /*@*/ ;
  595. int atexit (void (*func)(void)) /*@modifies internalState@*/ ;
  596.  
  597. /*@observer@*/ /*@null@*/ char *getenv (char *name) /*@*/ ;
  598.  
  599. int system (/*@null@*/ char *s) /*@modifies fileSystem@*/ ;
  600.  
  601. /*@null@*/ /*@dependent@*/ void *
  602.   bsearch (void *key, void *base, 
  603.        size_t n, size_t size, 
  604.        int (*compar)(void *, void *)) /*@*/ ;
  605.  
  606. void qsort (void *base, size_t n, size_t size, 
  607.            int (*compar)(void *, void *))
  608.    /*@modifies *base, errno@*/ ;
  609.  
  610. int abs (int n) /*@*/ ;
  611.  
  612. typedef /*@concrete@*/ struct 
  613. {
  614.   int quot;
  615.   int rem;
  616. } div_t ;
  617.  
  618. div_t div (int num, int denom) /*@*/ ;
  619.  
  620. long int labs (long int n) /*@*/ ; 
  621.  
  622. typedef /*@concrete@*/ struct 
  623. {
  624.   long int quot;
  625.   long int rem;
  626. } ldiv_t ;
  627.  
  628. ldiv_t ldiv (long num, long denom) /*@*/ ;
  629.  
  630. /*@constant size_t MB_CUR_MAX; @*/
  631.  
  632. /*
  633. ** wchar_t and wint_t functions added by Amendment 1 to ISO.
  634. */
  635.  
  636. /*@constant int WCHAR_MAX@*/
  637. /*@constant int WCHAR_MIN@*/
  638. /*@constant wint_t WEOF@*/
  639.  
  640. wint_t btowc (int c) /*@*/ ;
  641.  
  642. wint_t fgetwc (FILE *fp)    /*@modifies fileSystem, *fp*/ ;
  643.  
  644. /*@null@*/ wchar_t *fgetws (/*@returned@*/ wchar_t *s, int n, FILE *stream)
  645.    /*@modifies fileSystem, *s, *stream@*/;
  646.  
  647. wint_t fputwc (wchar_t c, FILE *stream)
  648.    /*@modifies fileSystem, *stream@*/;
  649.  
  650. int fputws (const wchar_t *s, FILE *stream)
  651.    /*@modifies fileSystem, *stream@*/ ;
  652.  
  653. int fwide (FILE *stream, int mode) /*@*/ ; 
  654.    /* does not modify the stream */
  655.  
  656. /*@printflike@*/ int fwprintf (FILE *stream, const wchar_t *format, ...)
  657.     /*@modifies *stream, fileSystem@*/ ;
  658.  
  659. /*@scanflike@*/ int fwscanf (FILE *stream, const wchar_t *format, ...)
  660.     /*@modifies *stream, fileSystem@*/ ;
  661.  
  662. /* note use of sef --- stream may be evaluated more than once */
  663. wint_t getwc (/*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ;
  664.  
  665. wint_t getwchar (void) /*@modifies fileSystem, *stdin@*/;
  666.  
  667. size_t mbrlen (const char *s, size_t n, /*@null@*/ mbstate_t *ps) /*@*/ ;
  668.  
  669. size_t mbrtowc (/*@null@*/ wchar_t *pwc, const char *s, size_t n,
  670.                /*@null@*/ mbstate_t *ps) 
  671.    /*@modifies *pwc@*/ ;
  672.  
  673. int mbsinit (/*@null@*/ const mbstate_t *ps) /*@*/ ;
  674.  
  675. size_t mbsrtowcs (/*@null@*/ wchar_t *dst, const char **src, size_t len,
  676.              /*@null@*/ mbstate_t *ps) 
  677.    /*@modifies *dst@*/ ;
  678.  
  679. /* note use of sef --- stream may be evaluated more than once */
  680. wint_t putwc (wchar_t c, /*@sef@*/ FILE *stream)    /*@modifies fileSystem, *stream@*/ ;
  681.  
  682. wint_t putwchar (wchar_t c) /*@modifies fileSystem, *stdout@*/ ;
  683.  
  684. /*@printflike@*/ int swprintf (wchar_t *s, size_t n, const wchar_t *format, ...)
  685.    /*@modifies *s@*/ ;
  686.  
  687. /*@scanflike@*/ int swscanf (const wchar_t *s, const wchar_t *format, ...)
  688.    /*@modifies *stdin@*/ ;
  689.  
  690. wint_t ungetwc (wint_t c, FILE *stream) /*@modifies fileSystem, *stream@*/ ;
  691.  
  692. int vfwprintf (FILE *stream, const wchar_t *format, va_list arg)
  693.    /*@modifies fileSystem, *stream@*/ ;
  694.  
  695. int vswprintf (wchar_t *s, size_t n, const wchar_t *format, va_list arg)
  696.    /*@modifies *s@*/ ;
  697.  
  698. int vwprintf (const wchar_t *format, va_list arg)
  699.    /*@modifies fileSystem, *stdout@*/ ;
  700.  
  701. size_t wcrtomb (/*@null@*/ /*@out@*/ char *s, wchar_t wc, /*@null@*/ mbstate_t *ps)
  702.    /*@modifies *s@*/;
  703.  
  704. void /*@alt wchar_t *@*/
  705.   wcscat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2)
  706.   /*@modifies *s1@*/ ;
  707.  
  708. /*@exposed@*/ /*@null@*/ wchar_t *
  709.   wcschr (/*@returned@*/ const wchar_t *s, wchar_t c)
  710.   /*@*/ ;
  711.  
  712. int wcscmp (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
  713.  
  714. int wcscoll (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
  715.  
  716. void /*@alt wchar_t *@*/ 
  717.   wcscpy (/*@unique@*/ /*@out@*/ /*@returned@*/ wchar_t *s1, const wchar_t *s2)
  718.   /*@modifies *s1@*/ ;
  719.  
  720. size_t wcscspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
  721.  
  722. size_t wcsftime (/*@out@*/ wchar_t *s, size_t maxsize, const wchar_t *format,
  723.             const struct tm *timeptr) 
  724.    /*@modifies *s@*/ ;
  725.  
  726. size_t wcslen (const wchar_t *s) /*@*/ ;
  727.  
  728. void /*@alt wchar_t *@*/
  729.   wcsncat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
  730.        size_t n) 
  731.   /*@modifies *s1@*/ ;
  732.  
  733. int wcsncmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
  734.  
  735. void /*@alt wchar_t *@*/
  736.   wcsncpy (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
  737.        size_t n) 
  738.    /*@modifies *s1@*/ ;
  739.  
  740. /*@null@*/ wchar_t *
  741.   wcspbrk (/*@returned@*/ const wchar_t *s1, const wchar_t *s2)
  742.   /*@*/ ;
  743.  
  744. /*@null@*/ wchar_t *
  745.   wcsrchr (/*@returned@*/ const wchar_t *s, wchar_t c)
  746.   /*@*/ ;
  747.  
  748. size_t
  749.   wcsrtombs (/*@null@*/ char *dst, const wchar_t **src, size_t len,
  750.          /*@null@*/ mbstate_t *ps) 
  751.   /*@modifies *src@*/ ;
  752.  
  753. size_t wcsspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
  754.  
  755. /*@null@*/ wchar_t *wcsstr (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
  756.  
  757. double wcstod (const wchar_t *nptr, /*@null@*/ wchar_t **endptr)
  758.    /*@modifies *endptr@*/ ;
  759.  
  760. /*@null@*/ wchar_t *
  761.   wcstok (/*@null@*/ wchar_t *s1, const wchar_t *s2, wchar_t **ptr)
  762.   /*@modifies *ptr@*/;
  763.  
  764. long wcstol (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
  765.    /*@modifies *endptr@*/;
  766.  
  767. unsigned long
  768.   wcstoul (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
  769.   /*@modifies *endptr@*/;
  770.  
  771. size_t
  772.   wcsxfrm (/*@null@*/ wchar_t *s1, const wchar_t *s2, size_t n)
  773.   /*@modifies *s1@*/;
  774.  
  775. int wctob (wint_t c) /*@*/;
  776.  
  777. /*@null@*/ wchar_t *wmemchr (const wchar_t *s, wchar_t c, size_t n) /*@*/ ;
  778.  
  779. int wmemcmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
  780.  
  781. wchar_t *wmemcpy (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
  782.    /*@modifies *s1@*/;
  783.  
  784. wchar_t *wmemmove (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
  785.    /*@modifies *s1@*/;
  786.  
  787. wchar_t *wmemset (/*@returned@*/ wchar_t *s, wchar_t c, size_t n)
  788.    /*@modifies *s@*/;
  789.  
  790. /*@printflike@*/ int wprintf (const wchar_t *format, ...)
  791.    /*@globals stdout@*/ /*@modifies errno, *stdout@*/;
  792.  
  793. /*@scanflike@*/ int
  794.   wscanf (const wchar_t *format, ...)
  795.   /*@globals stdin@*/ /*@modifies errno, *stdin@*/;
  796.  
  797. /*
  798. ** wctype.h (added by Amendment 1)
  799. */
  800.  
  801. /* Warning: not sure about these (maybe abstract?): */
  802. typedef /*@integraltype@*/ wctype_t;
  803. typedef /*@integraltype@*/ wctrans_t;
  804.  
  805. # ifdef STRICT
  806. lltX_bool iswalnum (wint_t c) /*@*/ ;
  807. lltX_bool iswalpha (wint_t c) /*@*/ ;
  808. lltX_bool iswcntrl (wint_t c) /*@*/ ;
  809. lltX_bool iswctype (wint_t c, wctype_t ctg) /*@*/ ;
  810. lltX_bool iswdigit (wint_t c) /*@*/ ;
  811. lltX_bool iswgraph (wint_t c) /*@*/ ;
  812. lltX_bool iswlower (wint_t c) /*@*/ ;
  813. lltX_bool iswprint (wint_t c) /*@*/ ;
  814. lltX_bool iswpunct (wint_t c) /*@*/ ;
  815. lltX_bool iswspace (wint_t c) /*@*/ ;
  816. lltX_bool iswupper (wint_t c) /*@*/ ;
  817. lltX_bool iswxdigit (wint_t c) /*@*/ ;
  818.  
  819. wint_t towctrans (wint_t c, wctrans_t ctg) /*@*/ ;
  820. wint_t towlower (wint_t c) /*@*/ ;
  821. wint_t towupper (wint_t c) /*@*/ ;
  822. # else
  823. lltX_bool /*@alt int@*/ iswalnum (wint_t c) /*@*/ ;
  824. lltX_bool /*@alt int@*/ iswalpha (wint_t c) /*@*/ ;
  825. lltX_bool /*@alt int@*/ iswcntrl (wint_t c) /*@*/ ;
  826. lltX_bool /*@alt int@*/ iswctype (wint_t c, wctype_t ctg) /*@*/ ;
  827. lltX_bool /*@alt int@*/ iswdigit (wint_t c) /*@*/ ;
  828. lltX_bool /*@alt int@*/ iswgraph (wint_t c) /*@*/ ;
  829. lltX_bool /*@alt int@*/ iswlower (wint_t c) /*@*/ ;
  830. lltX_bool /*@alt int@*/ iswprint (wint_t c) /*@*/ ;
  831. lltX_bool /*@alt int@*/ iswpunct (wint_t c) /*@*/ ;
  832. lltX_bool /*@alt int@*/ iswspace (wint_t c) /*@*/ ;
  833. lltX_bool /*@alt int@*/ iswupper (wint_t c) /*@*/ ;
  834. lltX_bool /*@alt int@*/ iswxdigit (wint_t c) /*@*/ ;
  835.  
  836. wint_t /*@alt int@*/ towctrans (wint_t c, wctrans_t ctg)    /*@*/ ;
  837. wint_t /*@alt int@*/ towlower (wint_t c)    /*@*/ ;
  838. wint_t /*@alt int@*/ towupper (wint_t c)    /*@*/ ;
  839. # endif
  840.  
  841. wctrans_t wctrans (const char *property)    /*@*/ ;
  842. wctype_t wctype (const char *property) /*@*/ ;
  843.  
  844. int mblen (char *s, size_t n) /*@*/ ;
  845. int mbtowc (/*@null@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n) 
  846.    /*@modifies *pwc@*/ ;
  847. int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar) 
  848.    /*@modifies *s@*/ ;
  849. size_t mbstowcs (/*@out@*/ wchar_t *pwcs, char *s, size_t n)
  850.   /*@modifies *pwcs@*/ ;
  851. size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n)
  852.   /*@modifies *s@*/ ;
  853.  
  854. /*
  855. ** string.h
  856. */
  857.      
  858. void /*@alt void * @*/
  859.   memcpy (/*@unique@*/ /*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n) 
  860.   /*@modifies *s1@*/
  861.      /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
  862.      ;
  863.  
  864. void /*@alt void * @*/
  865.   memmove (/*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
  866.   /*@modifies *s1@*/
  867.   /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
  868.    ;
  869.  
  870.   
  871.   /* drl
  872.      modifed  12/29/2000
  873.   */
  874.  
  875. void /*@alt char * @*/ 
  876.   strcpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2) 
  877.      /*@modifies *s1@*/ 
  878.      /*@requires maxSet(s1) >= maxRead(s2) @*/
  879.      /*@ensures maxRead(s1) == maxRead (s2) /\ maxRead(result) == maxRead(s2) /\ maxSet(result) == maxSet(s1); @*/;
  880.  
  881. void /*@alt char * @*/
  882.   strncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2, size_t n) 
  883.   /*@modifies *s1@*/      /*@requires maxSet(s1) >= ( n - 1 ); @*/ /*@ensures maxRead (s2) >= maxRead(s1) /\ maxRead (s1) <= n; @*/; 
  884.  
  885. void /*@alt char * @*/
  886.   strcat (/*@unique@*/ /*@returned@*/ char *s1, char *s2) 
  887.      /*@modifies *s1@*/ /*@requires maxSet(s1) >= (maxRead(s1) + maxRead(s2) );@*/
  888.      /*@ensures maxRead(result) == (maxRead(s1) + maxRead(s2) );@*/;
  889.  
  890. void /*@alt char * @*/
  891.   strncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, size_t n)
  892.      /*@modifies *s1@*/ 
  893.      /*@requires maxSet(s1) >= ( maxRead(s1) + n); @*/
  894.       /*@ensures maxRead(s1) >= (maxRead(s1) + n); @*/;
  895.  
  896.      /*drl end*/
  897.      
  898. int memcmp (void *s1, void *s2, size_t n) /*@*/ ;
  899. int strcmp (char *s1, char *s2) /*@*/ ;
  900. int strcoll (char *s1, char *s2) /*@*/ ;
  901. int strncmp (char *s1, char *s2, size_t n) /*@*/ ;
  902. size_t strxfrm (/*@out@*/ /*@null@*/ char *s1, char *s2, size_t n) 
  903.   /*@modifies *s1@*/ ;  /* s1 may be null only if n == 0 */ 
  904.  
  905. /*@null@*/ void *memchr (void *s, int c, size_t n) /*@*/ ;
  906.  
  907. # ifdef STRICT
  908. /*@exposed@*/ /*@null@*/ char *
  909. strchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
  910. # else
  911. /*@exposed@*/ /*@null@*/ char *
  912.   strchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0; @*/ ;
  913. # endif
  914.  
  915. size_t strcspn (char *s1, char *s2) /*@*/ ;
  916. /*@null@*/ /*@exposed@*/ char *
  917.   strpbrk (/*@returned@*/ char *s, char *t) /*@*/ ;
  918.  
  919. # ifdef STRICT
  920. /*@null@*/ /*@exposed@*/ char *
  921.   strrchr (/*@returned@*/ char *s, char c) /*@*/  /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
  922. # else
  923. /*@null@*/ /*@exposed@*/ char *
  924.   strrchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/  /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
  925. # endif
  926.  
  927. size_t strspn (char *s, char *t) /*@*/ ;
  928.  
  929. /*@null@*/ /*@exposed@*/  char *
  930.   strstr (/*@returned@*/ /*@unique@*/ char *s, char *t) /*@*/
  931.        /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 /\ maxRead(result) >= maxRead(t) /\ maxSet(result) >= maxRead(t)@*/ ;
  932.  
  933. /*@null@*/ /*@exposed@*/ char *
  934.   strtok (/*@returned@*/ /*@null@*/ char *s, char *t)
  935.   /*@modifies *s, internalState, errno@*/ ;
  936.  
  937. void /*@alt void *@*/ memset (/*@out@*/ /*@returned@*/ void *s, 
  938.                      int c, size_t n)
  939.      /*@modifies *s@*/ /*@requires maxSet(s) >= (n - 1) @*/ /*@ensures maxRead(s) >= (n - 1) @*/ ;
  940.  
  941. /*@observer@*/ char *strerror (int errnum) /*@*/ ;
  942.  
  943. /*drl */
  944. size_t strlen (char *s) /*@*/ /*@ensures result == maxRead(s); @*/; 
  945.  
  946. /*
  947. ** time.h
  948. */
  949.  
  950. /*@constant int CLOCKS_PER_SEC;@*/
  951.  
  952. typedef /*@integraltype@*/ clock_t;
  953. typedef /*@integraltype@*/ time_t;
  954.  
  955. struct tm
  956.   {
  957.     int tm_sec;
  958.     int tm_min;
  959.     int tm_hour;
  960.     int tm_mday;
  961.     int tm_mon;
  962.     int tm_year;
  963.     int tm_wday;
  964.     int tm_yday;
  965.     int tm_isdst;
  966.   } ;
  967.  
  968. clock_t clock (void) /*@modifies internalState@*/ ;
  969. double difftime (time_t time1, time_t time0) /*@*/ ;
  970. time_t mktime (struct tm *timeptr) /*@*/ ;
  971.  
  972. time_t time (/*@null@*/ /*@out@*/ time_t *tp)
  973.   /*@modifies *tp@*/ ;
  974.  
  975. /*@observer@*/ char *asctime (struct tm *timeptr) 
  976.   /*@modifies errno*/ /*@ensures maxSet(result) == 25 /\  maxRead(result) == 25; @*/ ;
  977.  
  978. /*@observer@*/ char *ctime (time_t *tp) /*@*/
  979.      /*@ensures maxSet(result) == 25 /\  maxRead(result) == 25; @*/;
  980.  
  981. /*@null@*/ /*@observer@*/ struct tm *gmtime (time_t *tp) /*@*/ ;
  982.  
  983. /*@null@*/ /*@observer@*/ struct tm *localtime (time_t *tp) 
  984.   /*@modifies errno@*/ ;
  985.  
  986. size_t strftime (/*@out@*/ char *s, size_t smax,
  987.             char *fmt, struct tm *timeptr)
  988.   /*@modifies *s@*/ ;
  989.  
  990. /*
  991. ** ISO c99: 7.18 Integer types <stdint.h>
  992. */
  993.  
  994. /*
  995. ** These types are OPTIONAL.  Provide warnings on use.
  996. */
  997.  
  998. typedef /*@integraltype@*/ int8_t
  999.    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least8_t instead."@*/ ;
  1000.  
  1001. typedef /*@integraltype@*/ int16_t
  1002.    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least16_t instead."@*/ ;
  1003.  
  1004. typedef /*@integraltype@*/ int32_t
  1005.    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least32_t instead."@*/ ;
  1006.  
  1007. typedef /*@integraltype@*/ int64_t
  1008.    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least64_t instead."@*/ ;
  1009.  
  1010. typedef /*@unsignedintegraltype@*/ uint8_t
  1011.    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least8_t instead."@*/ ;
  1012.  
  1013. typedef /*@unsignedintegraltype@*/ uint16_t
  1014.    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least16_t instead."@*/ ;
  1015.  
  1016. typedef /*@unsignedintegraltype@*/ uint32_t
  1017.    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least32_t instead."@*/ ;
  1018.  
  1019. typedef /*@unsignedintegraltype@*/ uint64_t
  1020.    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least64_t instead."@*/ ;
  1021.  
  1022. typedef /*@integraltype@*/ int_least8_t;
  1023. typedef /*@integraltype@*/ int_least16_t;
  1024. typedef /*@integraltype@*/ int_least32_t;
  1025. typedef /*@integraltype@*/ int_least64_t;
  1026.  
  1027. typedef /*@unsignedintegraltype@*/ uint_least8_t;
  1028. typedef /*@unsignedintegraltype@*/ uint_least16_t;
  1029. typedef /*@unsignedintegraltype@*/ uint_least32_t;
  1030. typedef /*@unsignedintegraltype@*/ uint_least64_t;
  1031.  
  1032. typedef /*@integraltype@*/ int_fast8_t;
  1033. typedef /*@integraltype@*/ int_fast16_t;
  1034. typedef /*@integraltype@*/ int_fast32_t;
  1035. typedef /*@integraltype@*/ int_fast64_t;
  1036.  
  1037. typedef /*@unsignedintegraltype@*/ uint_fast8_t;
  1038. typedef /*@unsignedintegraltype@*/ uint_fast16_t;
  1039. typedef /*@unsignedintegraltype@*/ uint_fast32_t;
  1040. typedef /*@unsignedintegraltype@*/ uint_fast64_t;
  1041.  
  1042. typedef int *intptr_t
  1043.    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;
  1044.  
  1045. typedef unsigned int *uintptr_t
  1046.    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;
  1047.  
  1048. typedef /*@signedintegraltype@*/ intmax_t;
  1049. typedef /*@unsignedintegraltype@*/ uintmax_t;
  1050.  
  1051. /*
  1052. ** What should the types be here? 
  1053. */ /*#*/
  1054.  
  1055. /*@constant int INT8_MIN@*/
  1056. /*@constant int INT16_MIN@*/
  1057. /*@constant int INT32_MIN@*/
  1058. /*@constant int INT64_MIN@*/
  1059.  
  1060. /*@constant int INT8_MAX@*/
  1061. /*@constant int INT16_MAX@*/
  1062. /*@constant int INT32_MAX@*/
  1063. /*@constant int INT64_MAX@*/
  1064.  
  1065. /*@constant int UINT8_MIN@*/
  1066. /*@constant int UINT16_MIN@*/
  1067. /*@constant int UINT32_MIN@*/
  1068. /*@constant int UINT64_MIN@*/
  1069.  
  1070. /*@constant int INT_LEAST8_MIN@*/
  1071. /*@constant int INT_LEAST16_MIN@*/
  1072. /*@constant int INT_LEAST32_MIN@*/
  1073. /*@constant int INT_LEAST64_MIN@*/
  1074.  
  1075. /*@constant int INT_LEAST8_MAX@*/
  1076. /*@constant int INT_LEAST16_MAX@*/
  1077. /*@constant int INT_LEAST32_MAX@*/
  1078. /*@constant int INT_LEAST64_MAX@*/
  1079.  
  1080. /*@constant int UINT_LEAST8_MAX@*/
  1081. /*@constant int UINT_LEAST16_MAX@*/
  1082. /*@constant int UINT_LEAST32_MAX@*/
  1083. /*@constant int UINT_LEAST64_MAX@*/
  1084.  
  1085. /*@constant int INT_FAST8_MIN@*/
  1086. /*@constant int INT_FAST16_MIN@*/
  1087. /*@constant int INT_FAST32_MIN@*/
  1088. /*@constant int INT_FAST64_MIN@*/
  1089.  
  1090. /*@constant int INT_FAST8_MAX@*/
  1091. /*@constant int INT_FAST16_MAX@*/
  1092. /*@constant int INT_FAST32_MAX@*/
  1093. /*@constant int INT_FAST64_MAX@*/
  1094.  
  1095. /*@constant int UINT_FAST8_MAX@*/
  1096. /*@constant int UINT_FAST16_MAX@*/
  1097. /*@constant int UINT_FAST32_MAX@*/
  1098. /*@constant int UINT_FAST64_MAX@*/
  1099.  
  1100. /*@constant size_t INTPTR_MIN@*/
  1101. /*@constant size_t INTPTR_MAX@*/
  1102.