-attribute 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