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 
test1(int x)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 
test2(int x)20 void test2 (int x) /*@requires sockets_initialized@*/
21 {
22   if (x > 3) {
23     sockets_finalize ();
24   } /* error */
25 }
26