*** empty log message ***

[splint.git] / test / fileio / filerw.c

diff --git a/test/fileio/filerw.c b/test/fileio/filerw.c
index f1b8ad379eace96c78694cb8ab95cfcb5d2ce2c1..c8a7c4f17af6ffc0c6a08411436a867d0f5ce697 100644 (file)
--- a/test/fileio/filerw.c
+++ b/test/fileio/filerw.c
@@ -1,11 +1,14 @@
 int f (/*@open@*/ /*@read@*/ FILE *f1, /*@open@*/ /*@write@*/ FILE *f2)
 {
-  fgetc (f1);
-  fgetc (f2); /* error: not readable */
-  
-  fputc ('a', f1);
-  fseek (f1, 0, SEEK_CUR); 
-  fputc ('a', f1);
+  int c;
 
-  fgetc (f1); /* error */
+  c = fgetc (f1);
+  c = fgetc (f2); /* error: not readable */
+  
+  (void) fputc ('a', f1); /* error */
+  (void) fseek (f1, 0, SEEK_CUR); 
+  (void) fputc ('a', f1); /* okay */
+ 
+  c = fgetc (f1); /* error */
+  return c;
 }