From 135ea728d1546bf3618663eb389be0c447ecc3d8 Mon Sep 17 00:00:00 2001
From: drl7x <drl7x>
Date: Thu, 29 Nov 2001 06:20:46 +0000
Subject: [PATCH] Fixed double requires clauses in posix.h

---
 lib/posix.h         | 2 +-
 lib/posix.lcd       | 3 ++-
 lib/posixstrict.lcd | 3 ++-
 lib/unix.lcd        | 3 ++-
 lib/unixstrict.lcd  | 3 ++-
 5 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/lib/posix.h b/lib/posix.h
index 7fea224..6eafec4 100644
--- a/lib/posix.h
+++ b/lib/posix.h
@@ -759,7 +759,7 @@ fpathconf (int fd, int name)
 
 extern /*@null@*/ char *getcwd (/*@returned@*/ /*@out@*/ /*@notnull@*/ char *buf, size_t size)
      /*@requires maxSet(buf) >= (size - 1)@*/
-     /*@requires maxRead(buf) <= (size - 1)*/
+     /*@ensures  maxRead(buf) <= (size - 1)@*/
 
      /*@modifies errno, *buf@*/ ;
 
diff --git a/lib/posix.lcd b/lib/posix.lcd
index af345cc..2574988 100644
--- a/lib/posix.lcd
+++ b/lib/posix.lcd
@@ -2366,6 +2366,8 @@ e2
 2
 3
 -1
+;; end precondition constraints
+post:
 C
 0@1@1
 l
@@ -2386,7 +2388,6 @@ e2
 3
 -1
 ;; end precondition constraints
-post:EMPTY
 read
 pre:
 C
diff --git a/lib/posixstrict.lcd b/lib/posixstrict.lcd
index 24d1f2c..4bd9935 100644
--- a/lib/posixstrict.lcd
+++ b/lib/posixstrict.lcd
@@ -2329,6 +2329,8 @@ e2
 2
 3
 -1
+;; end precondition constraints
+post:
 C
 0@1@1
 l
@@ -2349,7 +2351,6 @@ e2
 3
 -1
 ;; end precondition constraints
-post:EMPTY
 read
 pre:
 C
diff --git a/lib/unix.lcd b/lib/unix.lcd
index 037c431..599f3dd 100644
--- a/lib/unix.lcd
+++ b/lib/unix.lcd
@@ -3348,6 +3348,8 @@ e2
 2
 3
 -1
+;; end precondition constraints
+post:
 C
 0@1@1
 l
@@ -3368,7 +3370,6 @@ e2
 3
 -1
 ;; end precondition constraints
-post:EMPTY
 read
 pre:
 C
diff --git a/lib/unixstrict.lcd b/lib/unixstrict.lcd
index 574ab20..f3bd610 100644
--- a/lib/unixstrict.lcd
+++ b/lib/unixstrict.lcd
@@ -3304,6 +3304,8 @@ e2
 2
 3
 -1
+;; end precondition constraints
+post:
 C
 0@1@1
 l
@@ -3324,7 +3326,6 @@ e2
 3
 -1
 ;; end precondition constraints
-post:EMPTY
 read
 pre:
 C
-- 
2.45.2