1 static void checkOpen (/*@open@*/ /*@null@*/ FILE *);
2 static void checkClosed (/*@closed@*/ /*@null@*/ FILE *);
3 
passOpen(FILE * f)4 void passOpen (/*@open@*/ FILE *f)
5      /*@ensures closed f@*/
6 {
7   (void) fputc (3, f);
8 } /* error: ensures not satisfied, didn't close */
9 
returnOpen(char * s)10 /*@dependent@*/ FILE *returnOpen (char *s)
11      /*@ensures open result@*/
12 {
13   FILE *fle = fopen (s, "r");
14   assert (fle != NULL);
15   (void) fclose (fle);
16   return fle; /* error: ensures not satisfied */
17 }
18 
main(void)19 int main (void)
20 {
21   FILE *fle = NULL;
22   char s[10];
23 
24   checkClosed (fle); /* okay */
25   checkOpen (fle); /* error */
26 
27   fle = fopen ("test", "r");
28 
29   if (fle == NULL)
30     {
31       return 0;
32     }
33 
34   passOpen (fle);
35   (void) fclose (fle); /* error: already closed */
36 
37   return 0;
38 }
39 
40