]>
Commit | Line | Data |
---|---|---|
80ee600a | 1 | static void checkOpen (/*@open@*/ /*@null@*/ FILE *); |
2 | static void checkClosed (/*@closed@*/ /*@null@*/ FILE *); | |
3 | ||
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 |