*** empty log message ***

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

diff --git a/src/Headers/inputStream.h b/src/Headers/inputStream.h
index 300f28d46cc9a763ad302ea8491b4019c1ff8f9d..fa8c5c403b77934a18d2a8ba23acac2a9c167e8d 100644 (file)
--- a/src/Headers/inputStream.h
+++ b/src/Headers/inputStream.h
@@ -14,7 +14,7 @@
 
 struct s_inputStream {
   cstring name;
-  /*@open@*/ /*@dependent@*/ /*@null@*/ FILE *file;
+  /*:open:*/ /*@dependent@*/ /*@null@*/ FILE *file;
   char buffer[STUBMAXRECORDSIZE+1];
   int lineNo;
   size_t charNo;
@@ -59,7 +59,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"