X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/ccf0a4a84a5a030c02e90d914b3f152b29826737..7bf960677344d11a101697c76672a0be4b3759f2:/lib/unix.h

diff --git a/lib/unix.h b/lib/unix.h
index 5ac86d4..e6db35e 100644
--- a/lib/unix.h
+++ b/lib/unix.h
@@ -242,10 +242,7 @@ typedef long segsz_t;
 typedef /*@abstract@*/ fd_set;
 
 /* Check ISO C99 inttypes.h ... */
-typedef unsigned int u_int32_t;
 typedef unsigned int uint32_t;
-
-typedef unsigned short int u_int16_t;
 typedef unsigned short int uint16_t;
 
 int ttyname_r (int fg, /*@out@*/ char *buffer, int len) /*@modifies buffer@*/ ;
@@ -831,7 +828,7 @@ lchown (const char *path, uid_t owner, gid_t group)
 
 	extern int
 readlink (const char *path, /*@out@*/ char *buf, int size)
-	/*@modifies *buf, errno@*/;
+     /*@modifies *buf, errno@*/ /*@ensures result <= size @*/;
 
 	extern int
 select (int mfd, fd_set /*@null@*/ *r, fd_set /*@null@*/ *w, fd_set /*@null@*/ *e, struct timeval *t)