X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/28bf4b0bfd405a2057d865910f8589c54a40f17b..210066f9dd04de7d7d2f04d320b39a52f28b290b:/src/Headers/inputStream.h

diff --git a/src/Headers/inputStream.h b/src/Headers/inputStream.h
index 300f28d..5b8b02e 100644
--- a/src/Headers/inputStream.h
+++ b/src/Headers/inputStream.h
@@ -1,5 +1,5 @@
 /*
-** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
+** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
 ** See ../LICENSE for license information.
 */
 /*
@@ -13,8 +13,8 @@
 # define STUBMAXRECORDSIZE 800
 
 struct s_inputStream {
-  cstring name;
-  /*@open@*/ /*@dependent@*/ /*@null@*/ FILE *file;
+  /*@only@*/ cstring name;
+  /*:open:*/ /*@dependent@*/ /*@null@*/ FILE *file;
   char buffer[STUBMAXRECORDSIZE+1];
   int lineNo;
   size_t charNo;
@@ -26,8 +26,8 @@ struct s_inputStream {
 
 /* in forwardTypes.h: abst_typedef null struct _inputStream *inputStream; */
 
-extern /*@falsenull@*/ bool inputStream_isDefined (/*@null@*/ inputStream p_f) /*@*/ ;
-extern /*@truenull@*/ bool inputStream_isUndefined (/*@null@*/ inputStream p_f) /*@*/ ;
+extern /*@falsewhennull@*/ bool inputStream_isDefined (/*@null@*/ inputStream p_f) /*@*/ ;
+extern /*@nullwhentrue@*/ bool inputStream_isUndefined (/*@null@*/ inputStream p_f) /*@*/ ;
 
 /*@constant null inputStream inputStream_undefined; @*/
 # define inputStream_undefined      ((inputStream) NULL)
@@ -37,8 +37,10 @@ extern /*@truenull@*/ bool inputStream_isUndefined (/*@null@*/ inputStream p_f)
 extern void inputStream_free (/*@null@*/ /*@only@*/ inputStream p_s);
 extern bool inputStream_close (inputStream p_s) 
    /*@modifies p_s, fileSystem@*/ ; 
-extern inputStream
+
+extern /*@only@*/ inputStream
   inputStream_create (/*@only@*/ cstring p_name, cstring p_suffix, bool p_echo) /*@*/ ;
+
 extern inputStream inputStream_fromString (cstring p_name, cstring p_str) /*@*/ ;
 extern /*@dependent@*/ /*@null@*/ char *inputStream_nextLine(inputStream p_s) 
    /*@modifies p_s@*/ ;
@@ -59,7 +61,7 @@ extern bool inputStream_getPath (cstring p_path, inputStream p_s)
 extern /*@observer@*/ cstring inputStream_fileName (inputStream p_s) /*@*/ ;
 extern bool inputStream_isOpen (/*@sef@*/ inputStream p_s) /*@*/ ;
 extern int inputStream_thisLineNumber(inputStream p_s) /*@*/ ;
-extern /*@open@*/ /*@exposed@*/ FILE *inputStream_getFile (inputStream p_s) /*@*/ ;
+extern /*:open:*/ /*@exposed@*/ FILE *inputStream_getFile (inputStream p_s) /*@*/ ;
 
 # else
 # error "Multiple include"