]> andersk Git - splint.git/blobdiff - lib/ansi.h
andersk / splint.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
*** empty log message ***
[splint.git] / lib / ansi.h
diff --git a/lib/ansi.h b/lib/ansi.h
index 519e14b6bc17c5121e0bba498b237490523f5dd5..2e91a4ecbe288625e2b1dd0b183b9be171ec1966 100644 (file)
--- a/lib/ansi.h
+++ b/lib/ansi.h
@@ -437,15 +437,20 @@ extern int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...)
 int sscanf (/*@out@*/ char *s, char *format, ...) /*@*/ ;
    /* modifies extra arguments */
 
-extern int vfprintf (FILE *stream, char *format, va_list arg)
+int vprintf (const char *format, va_list arg)
+   /*@globals stdout@*/
+   /*@modifies fileSystem, *stdout@*/ ;
+
+int vfprintf (FILE *stream, char *format, va_list arg)
    /*@modifies fileSystem, *stream, arg, errno@*/ ;
 
-extern int vprintf (char *format, va_list arg)
-   /*@globals stdout@*/
-   /*@modifies fileSystem, arg, *stdout@*/ ;
+int vsprintf (/*@out@*/ char *str, const char *format, va_list ap)
+     /*@warn bufferoverflowhigh "Use vsnprintf instead"@*/
+     /*@modifies str@*/ ;
 
-extern int vsprintf (/*@out@*/ char *s, char *format, va_list arg)
-   /*@modifies *s, arg@*/ ;
+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) 
    /*@modifies fileSystem, *stream, errno@*/ ;
@@ -471,7 +476,7 @@ extern int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/
 
 extern /*@null@*/ char *gets (/*@out@*/ char *s) 
    /*@warn bufferoverflowhigh
-           "Use of gets leads to a buffer overflow vulnerability.  Use fgets instead."@*/
+           "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)
@@ -553,7 +558,7 @@ extern /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@*/
 extern /*@null@*/ /*@only@*/ void *
    realloc (/*@null@*/ /*@only@*/ /*@special@*/ void *p, 
            size_t size) /*@releases p@*/ /*@modifies *p@*/
-     /*@ensures MaxSet(result) >= (size - 1) @*/;
+     /*@ensures MaxSet(result) == (size - 1) @*/;
 # endif
 
 /*
@@ -567,9 +572,9 @@ extern /*@null@*/ /*@only@*/ void *
 
 extern /*@null@*/ /*@only@*/ void *
    realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size) 
-     /*@modifies *p @*/ /*@ensures MaxSet(result) >= (size - 1) @*/;
+     /*@modifies *p@*/ /*@ensures MaxSet(result) >= (size - 1) @*/;
 
-extern void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies *p@*/ ;
+extern void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies p@*/ ;
 
 /*@constant int EXIT_FAILURE; @*/ 
 /*@constant int EXIT_SUCCESS; @*/ 
@@ -842,13 +847,13 @@ extern size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n)
 extern void /*@alt void * @*/
   memcpy (/*@unique@*/ /*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n) 
   /*@modifies *s1@*/
-     /*@requires MaxRead(s2) >= n /\ MaxSet(s1) >= n; @*/
+     /*@requires MaxRead(s2) >= (n - 1) /\ MaxSet(s1) >= (n - 1); @*/
      ;
 
 extern void /*@alt void * @*/
   memmove (/*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
   /*@modifies *s1@*/
-  /*@requires MaxRead(s2) >= n /\ MaxSet(s1) >= n; @*/
+  /*@requires MaxRead(s2) >= (n - 1) /\ MaxSet(s1) >= (n - 1); @*/
    ;
 
   
@@ -858,20 +863,24 @@ extern void /*@alt void * @*/
 
 extern 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); @*/;
+     /*@modifies *s1@*/ 
+     /*@requires maxSet(s1) >= maxRead(s2) @*/
+     /*@ensures MaxRead(s1) == MaxRead (s2) /\ MaxRead(result) == MaxRead(s2) /\ MaxSet(result) == MaxSet(s1); @*/;
 
 extern 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 * @*/
-  strcat (/*@unique@*/ /*returned*/ /*@out@*/ char *s1, char *s2) 
+  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 * @*/
-  strncat (/*@unique@*/ /*@returned@*/ /*@out@*/ char *s1, char *s2, int n)
-     /*@modifies *s1@*/ /*@requires MaxSet(s1) >= ( MaxRead(s1) + n); @*/ /*@ensures MaxRead(result) >= (MaxRead(s1) + n); @*/;
+  strncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, size_t n)
+     /*@modifies *s1@*/ 
+     /*@requires MaxSet(s1) >= ( MaxRead(s1) + n); @*/
+      /*@ensures MaxRead(s1) >= (MaxRead(s1) + n); @*/;
 
      /*drl end*/
      
@@ -886,10 +895,10 @@ extern /*@null@*/ void *memchr (void *s, int c, size_t n) /*@*/ ;
 
 # ifdef STRICT
 extern /*@exposed@*/ /*@null@*/ char *
-strchr (char *s, char c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0 @*/ ;
+strchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0 @*/ ;
 # else
 extern /*@exposed@*/ /*@null@*/ char *
-  strchr ( char *s, int /*@alt char@*/ c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0; @*/ ;
+  strchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0; @*/ ;
 # endif
 
 extern size_t strcspn (char *s1, char *s2) /*@*/ ;
@@ -966,3 +975,116 @@ extern /*@null@*/ /*@observer@*/ struct tm *localtime (time_t *tp)
 extern size_t strftime (/*@out@*/ char *s, size_t smax,
                        char *fmt, struct tm *timeptr)
   /*@modifies *s@*/ ;
+
+/*
+** ISO c99: 7.18 Integer types <stdint.h>
+*/
+
+/*
+** These types are OPTIONAL.  Provide warnings on use.
+*/
+
+typedef /*@integraltype@*/ int8_t
+   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least8_t instead."@*/ ;
+
+typedef /*@integraltype@*/ int16_t
+   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least16_t instead."@*/ ;
+
+typedef /*@integraltype@*/ int32_t
+   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least32_t instead."@*/ ;
+
+typedef /*@integraltype@*/ int64_t
+   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least64_t instead."@*/ ;
+
+typedef /*@unsignedintegraltype@*/ uint8_t
+   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least8_t instead."@*/ ;
+
+typedef /*@unsignedintegraltype@*/ uint16_t
+   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least16_t instead."@*/ ;
+
+typedef /*@unsignedintegraltype@*/ uint32_t
+   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least32_t instead."@*/ ;
+
+typedef /*@unsignedintegraltype@*/ uint64_t
+   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least64_t instead."@*/ ;
+
+typedef /*@integraltype@*/ int_least8_t;
+typedef /*@integraltype@*/ int_least16_t;
+typedef /*@integraltype@*/ int_least32_t;
+typedef /*@integraltype@*/ int_least64_t;
+
+typedef /*@unsignedintegraltype@*/ uint_least8_t;
+typedef /*@unsignedintegraltype@*/ uint_least16_t;
+typedef /*@unsignedintegraltype@*/ uint_least32_t;
+typedef /*@unsignedintegraltype@*/ uint_least64_t;
+
+typedef /*@integraltype@*/ int_fast8_t;
+typedef /*@integraltype@*/ int_fast16_t;
+typedef /*@integraltype@*/ int_fast32_t;
+typedef /*@integraltype@*/ int_fast64_t;
+
+typedef /*@unsignedintegraltype@*/ uint_fast8_t;
+typedef /*@unsignedintegraltype@*/ uint_fast16_t;
+typedef /*@unsignedintegraltype@*/ uint_fast32_t;
+typedef /*@unsignedintegraltype@*/ uint_fast64_t;
+
+typedef int *intptr_t
+   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;
+
+typedef unsigned int *uintptr_t
+   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;
+
+typedef /*@signedintegraltype@*/ intmax_t;
+typedef /*@unsignedintegraltype@*/ uintmax_t;
+
+/*
+** What should the types be here? 
+*/ /*#*/
+
+/*@constant int INT8_MIN@*/
+/*@constant int INT16_MIN@*/
+/*@constant int INT32_MIN@*/
+/*@constant int INT64_MIN@*/
+
+/*@constant int INT8_MAX@*/
+/*@constant int INT16_MAX@*/
+/*@constant int INT32_MAX@*/
+/*@constant int INT64_MAX@*/
+
+/*@constant int UINT8_MIN@*/
+/*@constant int UINT16_MIN@*/
+/*@constant int UINT32_MIN@*/
+/*@constant int UINT64_MIN@*/
+
+/*@constant int INT_LEAST8_MIN@*/
+/*@constant int INT_LEAST16_MIN@*/
+/*@constant int INT_LEAST32_MIN@*/
+/*@constant int INT_LEAST64_MIN@*/
+
+/*@constant int INT_LEAST8_MAX@*/
+/*@constant int INT_LEAST16_MAX@*/
+/*@constant int INT_LEAST32_MAX@*/
+/*@constant int INT_LEAST64_MAX@*/
+
+/*@constant int UINT_LEAST8_MAX@*/
+/*@constant int UINT_LEAST16_MAX@*/
+/*@constant int UINT_LEAST32_MAX@*/
+/*@constant int UINT_LEAST64_MAX@*/
+
+/*@constant int INT_FAST8_MIN@*/
+/*@constant int INT_FAST16_MIN@*/
+/*@constant int INT_FAST32_MIN@*/
+/*@constant int INT_FAST64_MIN@*/
+
+/*@constant int INT_FAST8_MAX@*/
+/*@constant int INT_FAST16_MAX@*/
+/*@constant int INT_FAST32_MAX@*/
+/*@constant int INT_FAST64_MAX@*/
+
+/*@constant int UINT_FAST8_MAX@*/
+/*@constant int UINT_FAST16_MAX@*/
+/*@constant int UINT_FAST32_MAX@*/
+/*@constant int UINT_FAST64_MAX@*/
+
+/*@constant size_t INTPTR_MIN@*/
+/*@constant size_t INTPTR_MAX@*/
git-cvsimport mirror of splint
This page took 0.081077 seconds and 4 git commands to generate.