]> andersk Git - splint.git/blobdiff - lib/standard.h
andersk / splint.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
Making fixes for Microsoft Visual C++ compiler.
[splint.git] / lib / standard.h
diff --git a/lib/standard.h b/lib/standard.h
index 7e4f55226c27ca6290ff7a8a394d97421697a4d1..ee6185fc625a3fc018ba5e06659f26f01161ada7 100644 (file)
--- a/lib/standard.h
+++ b/lib/standard.h
@@ -22,6 +22,17 @@
 /*@unchecked@*/ int errno;
 # endif
 
+/*
+** stdbool.h
+*/
+
+/*@-likelybool@*/
+typedef _Bool bool;
+/*@=likelybool@*/
+/*@constant bool true@*/
+/*@constant bool false@*/
+/*@constant int __bool_true_false_are_defined = 1@*/
+
 /*
 ** types 
 */
@@ -44,13 +55,13 @@ typedef /*@abstract@*/ mbstate_t;
 ** assert.h
 */
 
-/*@constant lltX_bool NDEBUG;@*/
+/*@constant _Bool NDEBUG;@*/
 
 # ifdef STRICT
-/*@falseexit@*/ void assert (/*@sef@*/ lltX_bool e) 
+/*@falseexit@*/ void assert (/*@sef@*/ _Bool e) 
   /*@*/ ;
 # else
-/*@falseexit@*/ void assert (/*@sef@*/ lltX_bool /*@alt int@*/ e) 
+/*@falseexit@*/ void assert (/*@sef@*/ _Bool /*@alt int@*/ e) 
   /*@*/ ;
 # endif
 
@@ -60,17 +71,17 @@ typedef /*@abstract@*/ mbstate_t;
 */
 
 # ifdef STRICT
-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) /*@*/ ;
+_Bool isalnum (int c) /*@*/ ;
+_Bool isalpha (int c) /*@*/ ;
+_Bool iscntrl (int c) /*@*/ ;
+_Bool isdigit (int c) /*@*/ ;
+_Bool isgraph (int c) /*@*/ ;
+_Bool islower (int c) /*@*/ ;
+_Bool isprint (int c) /*@*/ ;
+_Bool ispunct (int c) /*@*/ ;
+_Bool isspace (int c) /*@*/ ;
+_Bool isupper (int c) /*@*/ ;
+_Bool isxdigit (int c) /*@*/ ;
 char tolower (int c) /*@*/ ;
 char toupper (int c) /*@*/ ;
 # else
@@ -78,17 +89,17 @@ char toupper (int c) /*@*/ ;
 ** evans 2002-01-03: added alt char (was alt unsigned char)
 */
 
-lltX_bool /*@alt int@*/ isalnum (int /*@alt char, unsigned char@*/ c) /*@*/ ;
-lltX_bool /*@alt int@*/ isalpha (int /*@alt char, unsigned char@*/ c) /*@*/ ;
-lltX_bool /*@alt int@*/ iscntrl (int /*@alt char, unsigned char@*/ c) /*@*/ ;
-lltX_bool /*@alt int@*/ isdigit (int /*@alt char, unsigned char@*/ c) /*@*/ ;
-lltX_bool /*@alt int@*/ isgraph (int /*@alt char, unsigned char@*/ c) /*@*/ ;
-lltX_bool /*@alt int@*/ islower (int /*@alt char, unsigned char@*/ c) /*@*/ ;
-lltX_bool /*@alt int@*/ isprint (int /*@alt char, unsigned char@*/ c) /*@*/ ;
-lltX_bool /*@alt int@*/ ispunct (int /*@alt char, unsigned char@*/ c) /*@*/ ;
-lltX_bool /*@alt int@*/ isspace (int /*@alt char, unsigned char@*/ c) /*@*/ ;
-lltX_bool /*@alt int@*/ isupper (int /*@alt char, unsigned char@*/ c) /*@*/ ;
-lltX_bool /*@alt int@*/ isxdigit (int /*@alt char, unsigned char@*/ c) /*@*/ ;
+_Bool /*@alt int@*/ isalnum (int /*@alt char, unsigned char@*/ c) /*@*/ ;
+_Bool /*@alt int@*/ isalpha (int /*@alt char, unsigned char@*/ c) /*@*/ ;
+_Bool /*@alt int@*/ iscntrl (int /*@alt char, unsigned char@*/ c) /*@*/ ;
+_Bool /*@alt int@*/ isdigit (int /*@alt char, unsigned char@*/ c) /*@*/ ;
+_Bool /*@alt int@*/ isgraph (int /*@alt char, unsigned char@*/ c) /*@*/ ;
+_Bool /*@alt int@*/ islower (int /*@alt char, unsigned char@*/ c) /*@*/ ;
+_Bool /*@alt int@*/ isprint (int /*@alt char, unsigned char@*/ c) /*@*/ ;
+_Bool /*@alt int@*/ ispunct (int /*@alt char, unsigned char@*/ c) /*@*/ ;
+_Bool /*@alt int@*/ isspace (int /*@alt char, unsigned char@*/ c) /*@*/ ;
+_Bool /*@alt int@*/ isupper (int /*@alt char, unsigned char@*/ c) /*@*/ ;
+_Bool /*@alt int@*/ isxdigit (int /*@alt char, unsigned char@*/ c) /*@*/ ;
 char /*@alt int@*/ tolower (int /*@alt char, unsigned char@*/ c) /*@*/ ;
 char /*@alt int@*/ toupper (int /*@alt char, unsigned char@*/ c) /*@*/ ;
 # endif
@@ -520,12 +531,15 @@ int fflush (/*@null@*/ FILE *stream)
 /*@dependent@*/ /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream) 
   /*@modifies *stream, fileSystem, errno@*/ ;
 
-extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf) 
-     /*@modifies fileSystem, *stream, *buf@*/ ;
+void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf) 
+     /*@modifies fileSystem, *stream, *buf@*/ 
+     /*:errorcode != 0*/ ;
+     /*:requires maxSet(buf) >= (BUFSIZ - 1):*/ ;
 
-extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf, 
-                   int mode, size_t size)
-     /*@modifies fileSystem, *stream, *buf@*/ ;
+int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf, 
+            int mode, size_t size)
+      /*@modifies fileSystem, *stream, *buf@*/
+     /*@requires maxSet(buf) >= (size - 1) @*/ ;
 
 # ifdef STRICT
 /*@printflike@*/ 
@@ -539,7 +553,7 @@ int /*@alt void@*/ fprintf (FILE *stream, char *format, ...)
 
 /*@scanflike@*/ 
 int fscanf (FILE *stream, char *format, ...)
-   /*@modifies fileSystem, *stream@*/ ;
+   /*@modifies fileSystem, *stream, errno@*/ ;
 
 # ifdef STRICT
 /*@printflike@*/ 
@@ -556,20 +570,29 @@ int /*@alt void@*/ printf (char *format, ...)
 /*@scanflike@*/
 int scanf(char *format, ...)
    /*@globals stdin@*/
-   /*@modifies fileSystem, *stdin@*/ ;
+   /*@modifies fileSystem, *stdin, errno@*/ ;
+   /*drl added errno 09-19-2001 */ ;
 
 # ifdef STRICT
 /*@printflike@*/ 
 int sprintf (/*@out@*/ char *s, char *format, ...) 
+   /*@warn bufferoverflowhigh "Buffer overflow possible with sprintf.  Recommend using snprintf instead"@*/
    /*@modifies *s@*/ ;
 # else
 /*@printflike@*/ 
 int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...) 
+   /*@warn bufferoverflowhigh "Buffer overflow possible with sprintf.  Recommend using snprintf instead"@*/
    /*@modifies *s@*/ ;
 # endif
 
+/* evans 2002-07-09: snprintf added to standard.h (from unix.h) */
+/*@printflike@*/
+int snprintf (/*@out@*/ char * restrict s, size_t n, const char * restrict format, ...)
+   /*@modifies s@*/
+   /*@requires maxSet(s) >= (n - 1)@*/ ;
+
 /*@scanflike@*/ 
-int sscanf (/*@out@*/ char *s, char *format, ...) /*@*/ ;
+int sscanf (/*@out@*/ char *s, char *format, ...) /*@modifies errno@*/ ;
    /* modifies extra arguments */
 
 int vprintf (const char *format, va_list arg)
@@ -584,7 +607,7 @@ int vsprintf (/*@out@*/ char *str, const char *format, va_list ap)
      /*@modifies str@*/ ;
 
 int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap)
-     /*@requires maxSet(str) >= size@*/
+     /*@requires maxSet(str) >= (size - 1)@*/ /* drl - this was size, size-1 in stdio.h */
      /*@modifies str@*/ ;
 
 int fgetc (FILE *stream) 
@@ -606,9 +629,9 @@ int fputs (char *s, FILE *stream)
 
 /* note use of sef --- stream may be evaluated more than once */
 int getc (/*@sef@*/ FILE *stream)
-  /*@modifies fileSystem, *stream@*/ ;
+  /*@modifies fileSystem, *stream, errno@*/ ;
 
-int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/ ;
+int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin, errno@*/ ;
 
 /*@null@*/ char *gets (/*@out@*/ char *s) 
    /*@warn bufferoverflowhigh
@@ -617,29 +640,36 @@ int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/ ;
 
 int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
    /*:errorcode EOF:*/
-   /*@modifies fileSystem, *stream;@*/ ;
+   /*@modifies fileSystem, *stream, errno;@*/ ;
 
 int putchar (int /*@alt char@*/ c)
    /*:errorcode EOF:*/
-   /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ; 
+   /*@globals stdout@*/ 
+   /*@modifies fileSystem, *stdout, errno@*/ ; 
 
 int puts (const char *s)
    /*:errorcode EOF:*/
    /*@globals stdout@*/
-   /*@modifies fileSystem, *stdout@*/ ; 
+   /*@modifies fileSystem, *stdout, errno@*/ ; 
 
 int ungetc (int /*@alt char@*/ c, FILE *stream)
-  /*@modifies fileSystem, *stream, errno@*/ ;
+  /*@modifies fileSystem, *stream@*/ ;
+      /*drl REMOVED errno 09-19-2001*/
 
 size_t 
   fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream)
-  /*@modifies fileSystem, *ptr, *stream, errno@*/ ;
+  /*@modifies fileSystem, *ptr, *stream, errno@*/ 
+  /*requires maxSet(ptr) >= (size - 1) @*/
+  /*@ensures maxRead(ptr) == (size - 1) @*/ ;
 
 size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream)
-  /*@modifies fileSystem, *stream, errno@*/ ;
+  /*@modifies fileSystem, *stream, errno@*/ 
+  /*@requires maxRead(ptr) >= size @*/ ;
 
 int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos)
-  /*@modifies *pos, errno@*/ ;
+   /*@modifies *pos, errno@*/
+   /*@requires maxSet(pos) >= 0@*/
+   /*@ensures maxRead(pos) >= 0 @*/;
 
 int fseek (FILE *stream, long int offset, int whence)
    /*:errorcode -1:*/
@@ -935,35 +965,35 @@ typedef /*@integraltype@*/ wctype_t;
 typedef /*@integraltype@*/ wctrans_t;
 
 # ifdef STRICT
-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) /*@*/ ;
+_Bool iswalnum (wint_t c) /*@*/ ;
+_Bool iswalpha (wint_t c) /*@*/ ;
+_Bool iswcntrl (wint_t c) /*@*/ ;
+_Bool iswctype (wint_t c, wctype_t ctg) /*@*/ ;
+_Bool iswdigit (wint_t c) /*@*/ ;
+_Bool iswgraph (wint_t c) /*@*/ ;
+_Bool iswlower (wint_t c) /*@*/ ;
+_Bool iswprint (wint_t c) /*@*/ ;
+_Bool iswpunct (wint_t c) /*@*/ ;
+_Bool iswspace (wint_t c) /*@*/ ;
+_Bool iswupper (wint_t c) /*@*/ ;
+_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
-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) /*@*/ ;
+_Bool /*@alt int@*/ iswalnum (wint_t c) /*@*/ ;
+_Bool /*@alt int@*/ iswalpha (wint_t c) /*@*/ ;
+_Bool /*@alt int@*/ iswcntrl (wint_t c) /*@*/ ;
+_Bool /*@alt int@*/ iswctype (wint_t c, wctype_t ctg) /*@*/ ;
+_Bool /*@alt int@*/ iswdigit (wint_t c) /*@*/ ;
+_Bool /*@alt int@*/ iswgraph (wint_t c) /*@*/ ;
+_Bool /*@alt int@*/ iswlower (wint_t c) /*@*/ ;
+_Bool /*@alt int@*/ iswprint (wint_t c) /*@*/ ;
+_Bool /*@alt int@*/ iswpunct (wint_t c) /*@*/ ;
+_Bool /*@alt int@*/ iswspace (wint_t c) /*@*/ ;
+_Bool /*@alt int@*/ iswupper (wint_t c) /*@*/ ;
+_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)       /*@*/ ;
git-cvsimport mirror of splint
This page took 0.050092 seconds and 4 git commands to generate.