X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/990ec8680b4718e26f8774a8f2ccff44fb97b3c5..e32d75272dc7aa26b4d74cc183310346c3095258:/lib/file.mts

diff --git a/lib/file.mts b/lib/file.mts
index 0e50032..f19f21b 100644
--- a/lib/file.mts
+++ b/lib/file.mts
@@ -1,24 +1,24 @@
-state file
+attribute openness
    context reference FILE *
-   oneof unopen, open
+   oneof closed, open, anyopen
    annotations
       open ==> open
-      closed ==> unopen
-
+      closed ==> closed
+      anyopen ==> anyopen
    merge
-      open + unopen ==> error "files merge in inconsistent state"
-      unopen + open ==> error "files merge in inconsistent state"
+      open + closed ==> error 
 
    transfers
-      open as unopen ==> error "open file passed as unopen"
-      unopen as open ==> error "unopen file passed as open"
+      open as closed ==> error
+      closed as open ==> error
 
    losereference
       open ==> error "open file not closed"
 
    defaults 
+      reference ==> open
       parameter ==> open
-
+      result ==> open
 end