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 d50c82640defbb4fbb8915d989f9a4aedfafd9d2..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,7 +13,7 @@
 # define STUBMAXRECORDSIZE 800
 
 struct s_inputStream {
-  cstring name;
+  /*@only@*/ cstring name;
   /*:open:*/ /*@dependent@*/ /*@null@*/ FILE *file;
   char buffer[STUBMAXRECORDSIZE+1];
   int lineNo;
@@ -37,8 +37,10 @@ extern /*@nullwhentrue@*/ bool inputStream_isUndefined (/*@null@*/ inputStream p
 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@*/ ;