5 typedef enum { ST_USED, ST_AVAIL } erefStatus;
7 /*@reldef@*/ /*@only@*/ employee *conts;
8 /*@only@*/ erefStatus *status;
12 static erefTable eref_Pool; /* private */
13 static bool needsInit = TRUE; /* private */
15 eref eref_alloc (void)
16 /*@globals eref_Pool@*/
17 /*@modifies eref_Pool@*/
21 for (i=0; (eref_Pool.status[i] == ST_USED) && (i < eref_Pool.size); i++)
28 if (res == eref_Pool.size)
31 (employee *) realloc (eref_Pool.conts,
32 2 * eref_Pool.size * sizeof (*eref_Pool.conts));
34 if (eref_Pool.conts == 0)
36 printf ("Malloc returned null in eref_alloc\n");
41 (erefStatus *) realloc (eref_Pool.status,
42 2 * eref_Pool.size * sizeof (*eref_Pool.status));
44 if (eref_Pool.status == 0)
46 printf ("Malloc returned null in eref_alloc\n");
50 eref_Pool.size = 2*eref_Pool.size;
52 for (i = res+1; i < eref_Pool.size; i++)
54 eref_Pool.status[i] = ST_AVAIL;
58 eref_Pool.status[res] = ST_USED;
62 void eref_initMod (void)
63 /*@globals undef eref_Pool, needsInit, internalState@*/
64 /*@modifies eref_Pool, needsInit, internalState@*/
71 /*@-compdef@*/ return; /*@=compdef@*/
78 eref_Pool.conts = (employee *) malloc (size * sizeof (*eref_Pool.conts));
80 if (eref_Pool.conts == 0)
82 printf ("Malloc returned null in eref_initMod\n");
86 eref_Pool.status = (erefStatus *) malloc (size * sizeof (*eref_Pool.status));
88 if (eref_Pool.status == 0)
90 printf ("Malloc returned null in eref_initMod\n");
94 eref_Pool.size = size;
97 for (i = 0; i < size; i++)
99 eref_Pool.status[i] = ST_AVAIL;
104 void eref_free (eref er)
105 /*@globals eref_Pool@*/
106 /*@modifies eref_Pool@*/
108 eref_Pool.status[er] = ST_AVAIL;
111 void eref_assign (eref er, employee e)
112 /*@globals eref_Pool@*/
113 /*@modifies eref_Pool@*/
115 eref_Pool.conts[er] = e;
118 employee eref_get (eref er)
119 /*@globals eref_Pool@*/
121 return eref_Pool.conts[er];