Fixed problem with NULL being changed.

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

diff --git a/src/Headers/reader.h b/src/Headers/reader.h
index dadb0835a58a769c5cd6d14ce917fa7b2c34b76e..2899ce3b9c12b85eac14daf4831a0c419c14ec97 100644 (file)
--- a/src/Headers/reader.h
+++ b/src/Headers/reader.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.
 **
 */
@@ -7,7 +7,7 @@
 # ifndef READER_H
 # define READER_H
 
-extern /*@null@*/ char *reader_readLine (FILE *p_f, /*@returned@*/ char *p_s, int p_max) 
+extern /*@null@*/ char *reader_readLine (FILE *p_f, /*@returned@*/ /*@out@*/ char *p_s, int p_max) 
    /*@modifies *p_f, p_s@*/ ;
 
 extern int reader_getInt (char **p_s) /*@modifies *p_s@*/ ;