*** empty log message ***

[splint.git] / lib / posix.h

diff --git a/lib/posix.h b/lib/posix.h
index 4f39cdc8dc25ab5c549c1af1b0d8f2a00c7089b7..01fbf408696ef36f9b89b4e41959d8719720a3e7 100644 (file)
--- a/lib/posix.h
+++ b/lib/posix.h
@@ -270,12 +270,12 @@ struct passwd {
 } ;
 
        extern /*@observer@*/ /*@null@*/ struct passwd *
-getpwnam (const char *)
-       /*@modifies errno@*/;
+       getpwnam (const char *)
+       /*@modifies errno@*/  /*@ensures maxRead(result) == 0 /\ maxSet(result) == 0 @*/;
 
        extern /*@observer@*/ /*@null@*/ struct passwd *
 getpwuid (uid_t uid)
-       /*@modifies errno@*/;
+       /*@modifies errno@*/  /*@ensures maxRead(result) == 0 /\ maxSet(result) == 0 @*/;
 
 /*
 ** setjmp.h
@@ -822,8 +822,10 @@ pipe (/*@out@*/ int fd[]) /* Out parameter noticed by Marc Espie. */
 
        extern ssize_t
 read (int fd, /*@out@*/ void *buf, size_t nbyte)
-       /*@modifies errno, *buf@*/;
-
+     /*@modifies errno, *buf@*/ /*@requires maxSet(buf) >= (nbyte - 1) @*/
+     /*@ensures maxRead(buf) >= nbyte @*/;
+     /*@i33*/
+     
        extern int
 rmdir (const char *path)
        /*@modifies fileSystem, errno@*/;