Fixed branch state bug with definitely null values (reported by Jon Wilson).

[splint.git] / lib / posix.lcd

diff --git a/lib/posix.lcd b/lib/posix.lcd
index a829dbc50187ceeb88cdc3a2a22fcbd85b16d762..37a78eda9365f5c84cc528c4a41b94e9b945580d 100644 (file)
--- a/lib/posix.lcd
+++ b/lib/posix.lcd
@@ -1,6 +1,6 @@
-;;LCLint Dump: posix.lcd
-;;LCLint 3.0.0.19 --- 5 October 2001
-;;lib:167
+;;; Splint Library  posix.lcd
+;;Splint 3.0.0.20 --- 29 December 2001
+;;lib:169
 ;;ctTable
 0 u-2 19 38
 0 p1|-2 20 39
@@ -2356,11 +2356,38 @@ l
 2
 Param 23 0
 r
+0
+1
+e1
 2
 2
 Param 63 1
+e2
+2
+3
+-1
+;; end precondition constraints
+post:
+C
+0@1@1
+l
+1
+3
+2
+2
+Param 23 0
+r
+0
+1
+e1
+2
+2
+Param 63 1
+e2
+2
+3
+-1
 ;; end precondition constraints
-post:EMPTY
 read
 pre:
 C