Fixed problem with NULL being changed.

[splint.git] / src / Headers / inputStream.h

diff --git a/src/Headers/inputStream.h b/src/Headers/inputStream.h
index 300f28d46cc9a763ad302ea8491b4019c1ff8f9d..5b8b02e683812f14eb8b24d6503ffe6d0c52e95c 100644 (file)
--- 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"