*** empty log message ***

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

diff --git a/src/Headers/reader.h b/src/Headers/reader.h
index dadb0835a58a769c5cd6d14ce917fa7b2c34b76e..fc138a613ebd791a2dc7e54284dd84e1a3478934 100644 (file)
--- a/src/Headers/reader.h
+++ b/src/Headers/reader.h
@@ -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@*/ ;