*** empty log message ***

[splint.git] / lib / unix.h

diff --git a/lib/unix.h b/lib/unix.h
index 5ac86d463c926301785129bd9423a418d14184cd..e6db35e01561f9fa7ea90d72a4c44617057ba58d 100644 (file)
--- 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)