]>
Commit | Line | Data |
---|---|---|
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 | } |