1 static void checkOpen (/*@open@*/ /*@null@*/ FILE *);
2 static void checkClosed (/*@closed@*/ /*@null@*/ FILE *);
3 
main(void)4 int main (void)
5 {
6   FILE *fle = NULL;
7   char s[10];
8 
9   checkClosed (fle); /* okay */
10   checkOpen (fle); /* error */
11 
12   fle = fopen ("test", "r");
13   checkClosed (fle); /* error */
14   checkOpen (fle); /* okay */
15 
16 
17   (void) fclose (fle);
18   checkOpen (fle); /* error */
19   checkClosed (fle); /* okay */
20 
21   return 0; /* error: f is not closed */
22 }
23 
24 
25 
26 # if 0
27 
28 @.S
29   (void) fgets (s, 3, fle);
30   (void) fclose (fle);
31   (void) fgets (s, 3, fle); /* error: f is not open */
32   (void) freopen ("test", "r", fle);
33   (void) fgets (s, 3, fle);
34 # endif
35