*** empty log message ***

[splint.git] / lib / stdio.h

diff --git a/lib/stdio.h b/lib/stdio.h
index 02cd5c9b851262bc60f2d63d9e0dea8fd867897f..47d554ceed803221f82e4d0e3940b851a6c12e57 100644 (file)
--- a/lib/stdio.h
+++ b/lib/stdio.h
@@ -185,12 +185,12 @@ extern char * ctermid (/*@returned@*/ /*@out@*/ /*@null@*/ char *s)
   /*@modifies fileSystem, *stdin, errno@*/
   /*drl added errno 09-19-001 */ ;
 
-  extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf) 
+  extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf) 
     /*@modifies fileSystem, *stream, *buf@*/ 
      // *@requires maxSet(buf) >= (BUFSIZ - 1) @*/
      ;
 
-    extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf, 
+     extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf, 
             int mode, size_t size)
       /*@modifies fileSystem, *stream, *buf@*/  /*@requires maxSet(buf) >= (size - 1) @*/ ;