test/db3/eref.c

   1 # include <stdio.h>
   2 # include <stdlib.h>
   3 # include "eref.h"
   4
   5 typedef enum { ST_USED, ST_AVAIL } erefStatus;
   6 typedef struct {
   7   /*@reldef@*/ /*@only@*/ employee *conts;
   8   /*@only@*/ erefStatus *status;
   9   int size;
  10 } erefTable;
  11
  12 static erefTable eref_Pool;     /* private */
  13 static bool needsInit = TRUE;  /* private */
  14
  15 eref eref_alloc (void)
  16    /*@globals eref_Pool@*/
  17    /*@modifies eref_Pool@*/
  18 {
  19   int i, res;
  20
  21   for (i=0; (eref_Pool.status[i] == ST_USED) && (i < eref_Pool.size); i++)
  22     {
  23       ;
  24     }
  25
  26   res = i;
  27
  28   if (res == eref_Pool.size)
  29     {
  30       eref_Pool.conts =
  31         (employee *) realloc (eref_Pool.conts,
  32                               2 * eref_Pool.size * sizeof (*eref_Pool.conts));
  33
  34       if (eref_Pool.conts == 0)
  35         {
  36           printf ("Malloc returned null in eref_alloc\n");
  37           exit (EXIT_FAILURE);
  38         }
  39
  40       eref_Pool.status =
  41         (erefStatus *) realloc (eref_Pool.status,
  42                                  2 * eref_Pool.size * sizeof (*eref_Pool.status));
  43
  44       if (eref_Pool.status == 0)
  45         {
  46           printf ("Malloc returned null in eref_alloc\n");
  47           exit (EXIT_FAILURE);
  48         }
  49
  50       eref_Pool.size = 2*eref_Pool.size;
  51
  52       for (i = res+1; i < eref_Pool.size; i++)
  53         {
  54           eref_Pool.status[i] = ST_AVAIL;
  55         }
  56     }
  57
  58   eref_Pool.status[res] = ST_USED;
  59   return (eref) res;
  60 }
  61
  62 void eref_initMod (void)
  63    /*@globals undef eref_Pool, needsInit, internalState@*/
  64    /*@modifies eref_Pool, needsInit, internalState@*/
  65 {
  66   int i;
  67   const int size = 16;
  68
  69   if (!needsInit)
  70     {
  71       /*@-compdef@*/ return; /*@=compdef@*/
  72     }
  73
  74   needsInit = FALSE;
  75   bool_initMod ();
  76   employee_initMod ();
  77
  78   eref_Pool.conts = (employee *) malloc (size * sizeof (*eref_Pool.conts));
  79
  80   if (eref_Pool.conts == 0)
  81     {
  82       printf ("Malloc returned null in eref_initMod\n");
  83       exit (EXIT_FAILURE);
  84     }
  85
  86   eref_Pool.status = (erefStatus *) malloc (size * sizeof (*eref_Pool.status));
  87
  88   if (eref_Pool.status == 0)
  89     {
  90       printf ("Malloc returned null in eref_initMod\n");
  91       exit (EXIT_FAILURE);
  92     }
  93
  94   eref_Pool.size = size;
  95
  96   /*@+loopexec@*/
  97   for (i = 0; i < size; i++)
  98     {
  99       eref_Pool.status[i] = ST_AVAIL;
 100     }
 101   /*@=loopexec@*/
 102 }
 103
 104 void eref_free (eref er)
 105   /*@globals eref_Pool@*/
 106   /*@modifies eref_Pool@*/
 107 {
 108   eref_Pool.status[er] = ST_AVAIL;
 109 }
 110
 111 void eref_assign (eref er, employee e)
 112   /*@globals eref_Pool@*/
 113   /*@modifies eref_Pool@*/
 114 {
 115   eref_Pool.conts[er] = e;
 116 }
 117
 118 employee eref_get (eref er)
 119    /*@globals eref_Pool@*/
 120 {
 121   return eref_Pool.conts[er];
 122 }