]>
Commit | Line | Data |
---|---|---|
80ee600a | 1 | extern void sockets_initialize (void) |
2 | /*@requires sockets_uninitialized@*/ | |
3 | /*@ensures sockets_initialized@*/ ; | |
4 | ||
5 | extern void sockets_finalize (void) | |
6 | /*@requires sockets_initialized@*/ | |
7 | /*@ensures sockets_uninitialized@*/ ; | |
8 | ||
9 | extern void useSockets (void) /*@requires sockets_initialized@*/ ; | |
10 | ||
11 | void test1 (int x) /*@requires sockets_uninitialized@*/ | |
12 | { | |
13 | if (x > 3) { | |
14 | sockets_initialize (); | |
15 | } | |
16 | ||
17 | useSockets (); /* okay (error before) */ | |
18 | } | |
19 | ||
20 | void test2 (int x) /*@requires sockets_initialized@*/ | |
21 | { | |
22 | if (x > 3) { | |
23 | sockets_finalize (); | |
24 | } /* error */ | |
25 | } |