test/metastate/sockets.c

   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 (void) /*@requires sockets_uninitialized@*/
  12 {
  13   useSockets (); /* error */
  14 }
  15
  16 void test2 (void) /*@requires sockets_initialized@*/
  17 {
  18   useSockets (); /* okay */
  19 }
  20
  21 void test3 (void) /*@requires sockets_uninitialized@*/
  22 {
  23   sockets_initialize ();
  24   useSockets (); /* okay */
  25 }
  26
  27 void test4 (void) /*@requires sockets_uninitialized@*/ /*@ensures sockets_uninitialized@*/
  28 {
  29   sockets_initialize ();
  30   useSockets (); /* okay */
  31 } /* error not finzalized */
  32
  33 void test5 (void) /*@requires sockets_uninitialized@*/ /*@ensures sockets_uninitialized@*/
  34 {
  35   sockets_initialize ();
  36   sockets_finalize ();
  37   useSockets (); /* error */
  38 } /* okay */
  39
  40 void test6 (void)
  41 {
  42   useSockets (); /* error (default is uninitialized) */
  43 }
  44
  45 void test7 (void)
  46 {
  47   sockets_initialize (); /* okay (default is uninitialized) */
  48 }
  49
  50