]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | # include <strings.h> |
2 | # include "dbase.h" | |
3 | ||
4 | typedef enum | |
5 | { | |
6 | KND_MMGRS, KND_FMGRS, KND_MNON, KND_FNON | |
7 | } employeeKinds; | |
8 | ||
9 | /*@constant static employeeKinds firstERC;@*/ | |
10 | # define firstERC KND_MMGRS | |
11 | ||
12 | /*@constant static employeeKinds lastERC;@*/ | |
13 | # define lastERC KND_FNON | |
14 | ||
15 | /*@constant static int numERCS;@*/ | |
16 | # define numERCS (/*@+enumint@*/ (lastERC - firstERC + 1) /*@=enumint@*/) | |
17 | ||
18 | typedef /*@only@*/ erc o_erc; | |
19 | static o_erc db[numERCS]; | |
20 | ||
21 | /*@iter employeeKinds_all (yield employeeKinds ek); @*/ | |
22 | # define employeeKinds_all(m_ek) \ | |
23 | { employeeKinds m_ek; for (m_ek = firstERC; m_ek <= lastERC; m_ek++) { | |
24 | ||
25 | # define end_employeeKinds_all }} | |
26 | ||
27 | static bool initDone = FALSE; | |
28 | ||
29 | void db_initMod (void) | |
30 | /*@globals initDone, undef db, internalState@*/ | |
31 | /*@modifies initDone, db, internalState@*/ | |
32 | { | |
33 | if (initDone) | |
34 | { | |
3120b462 | 35 | /*@-compdef@*/ return; /*@=compdef@*/ |
885824d3 | 36 | } |
37 | ||
38 | bool_initMod (); | |
39 | employee_initMod (); | |
40 | eref_initMod (); | |
41 | erc_initMod (); | |
42 | empset_initMod (); | |
43 | ||
44 | employeeKinds_all (ek) | |
45 | { | |
3120b462 | 46 | /*@-mustfree@*/ db[(int)ek] = erc_create (); /*@=mustfree@*/ |
885824d3 | 47 | } end_employeeKinds_all ; |
48 | ||
3120b462 | 49 | initDone = TRUE; /*@-compdef@*/ /* db[] is really defined */ |
50 | } /*@=compdef@*/ | |
885824d3 | 51 | |
52 | static eref db_ercKeyGet(erc c, int key) /*@*/ | |
53 | { | |
54 | erc_elements(c, er) | |
55 | { | |
56 | if (eref_get(er).ssNum == key) | |
57 | { | |
58 | return (er); | |
59 | } | |
60 | } end_erc_elements ; | |
61 | ||
62 | return eref_undefined; | |
63 | } | |
64 | ||
65 | static eref db_keyGet (int key) /*@globals db@*/ | |
66 | { | |
67 | eref er; | |
68 | ||
69 | employeeKinds_all (ek) | |
70 | { | |
71 | er = db_ercKeyGet (db[(int) ek], key); | |
72 | ||
73 | if (eref_isDefined (er)) | |
74 | { | |
75 | return er; | |
76 | } | |
77 | } end_employeeKinds_all ; | |
78 | ||
79 | return eref_undefined; | |
80 | } | |
81 | ||
82 | static int db_addEmpls (erc c, int l, int h, empset s) | |
83 | /*@globals internalState@*/ | |
84 | /*@modifies s, internalState@*/ | |
85 | { | |
86 | employee e; | |
87 | int numAdded; | |
88 | numAdded = 0; | |
89 | ||
90 | erc_elements (c, er) | |
91 | { | |
92 | e = eref_get(er); | |
93 | if ((e.salary >= l) && (e.salary <= h)) | |
94 | { | |
95 | empset_insert(s, e); | |
96 | numAdded++; | |
97 | } | |
98 | } end_erc_elements ; | |
99 | ||
100 | return numAdded; | |
101 | } | |
102 | ||
103 | db_status db_hire (employee e) /*@globals db@*/ | |
104 | { | |
105 | if (e.gen == GENDER_UNKNOWN) | |
106 | { | |
107 | return DBS_GENDERERR; | |
108 | } | |
109 | ||
110 | if (e.j == JOB_UNKNOWN) | |
111 | { | |
112 | return DBS_JOBERR; | |
113 | } | |
114 | ||
115 | if (e.salary < 0) | |
116 | { | |
117 | return DBS_SALERR; | |
118 | } | |
119 | ||
120 | if (eref_isDefined (db_keyGet (e.ssNum))) | |
121 | { | |
122 | return DBS_DUPLERR; | |
123 | } | |
124 | ||
125 | db_uncheckedHire (e); | |
126 | return DBS_OK; | |
127 | } | |
128 | ||
129 | void db_uncheckedHire (employee e) | |
130 | /*@globals db@*/ /*@modifies db@*/ | |
131 | { | |
132 | eref er; | |
133 | ||
134 | er = eref_alloc (); | |
135 | eref_assign (er, e); | |
136 | ||
137 | if (e.gen == MALE) | |
138 | { | |
139 | if (e.j == MGR) | |
140 | { | |
141 | erc_insert (db[(int) KND_MMGRS], er); | |
142 | } | |
143 | else | |
144 | { | |
145 | erc_insert (db[(int) KND_MNON], er); | |
146 | } | |
147 | } | |
148 | else | |
149 | { | |
150 | if (e.j == MGR) | |
151 | { | |
152 | erc_insert (db[(int) KND_FMGRS], er); | |
153 | } | |
154 | else | |
155 | { | |
156 | erc_insert (db[(int) KND_FNON], er); | |
157 | } | |
158 | } | |
159 | } | |
160 | ||
161 | bool db_fire (int ssNum) | |
162 | /*@globals db@*/ /*@modifies db@*/ | |
163 | { | |
164 | employeeKinds_all (ek) | |
165 | { | |
166 | erc_elements (db[(int) ek], er) | |
167 | { | |
168 | if (eref_get(er).ssNum == ssNum) | |
169 | { | |
170 | erc_delete (db[(int) ek], er); | |
171 | return TRUE; | |
172 | } | |
173 | } end_erc_elements ; | |
174 | } end_employeeKinds_all ; | |
175 | ||
176 | return FALSE; | |
177 | } | |
178 | ||
179 | bool db_promote (int ssNum) | |
180 | /*@globals db@*/ /*@modifies db@*/ | |
181 | { | |
182 | eref er; | |
183 | employee e; | |
184 | gender g; | |
185 | ||
186 | g = MALE; | |
187 | er = db_ercKeyGet (db[(int) KND_MNON], ssNum); | |
188 | ||
189 | if (!eref_isDefined (er)) | |
190 | { | |
191 | er = db_ercKeyGet (db[(int) KND_FNON], ssNum); | |
192 | ||
193 | if (!eref_isDefined (er)) | |
194 | { | |
195 | return FALSE; | |
196 | } | |
197 | ||
198 | g = FEMALE; | |
199 | } | |
200 | ||
201 | e = eref_get (er); | |
202 | e.j = MGR; | |
203 | eref_assign (er, e); | |
204 | ||
205 | if (g == MALE) | |
206 | { | |
207 | erc_delete (db[(int) KND_MNON], er); | |
208 | erc_insert (db[(int) KND_MMGRS], er); | |
209 | } | |
210 | else | |
211 | { | |
212 | erc_delete (db[(int) KND_FNON], er); | |
213 | erc_insert (db[(int) KND_FMGRS], er); | |
214 | } | |
215 | ||
216 | return TRUE; | |
217 | } | |
218 | ||
219 | db_status db_setSalary (int ssNum, int sal) /*@globals db@*/ | |
220 | { | |
221 | eref er; | |
222 | employee e; | |
223 | ||
224 | if (sal < 0) | |
225 | { | |
226 | return DBS_SALERR; | |
227 | } | |
228 | ||
229 | er = db_keyGet (ssNum); | |
230 | ||
231 | if (!eref_isDefined (er)) | |
232 | { | |
233 | return DBS_MISSERR; | |
234 | } | |
235 | ||
236 | e = eref_get (er); | |
237 | e.salary = sal; | |
238 | eref_assign (er, e); | |
239 | ||
240 | return DBS_OK; | |
241 | } | |
242 | ||
243 | int db_query (db_q q, empset s) | |
244 | /*@globals db@*/ | |
245 | { | |
246 | int numAdded; | |
247 | int l, h; | |
248 | ||
249 | l = q.l; | |
250 | h = q.h; | |
251 | ||
252 | switch (q.g) | |
253 | { | |
254 | case GENDER_UNKNOWN: | |
255 | switch (q.j) | |
256 | { | |
257 | case JOB_UNKNOWN: | |
258 | numAdded = 0; | |
259 | ||
260 | employeeKinds_all (ek) | |
261 | { | |
262 | numAdded += db_addEmpls (db[(int) ek], l, h, s); | |
263 | } end_employeeKinds_all | |
264 | ||
265 | return numAdded; | |
266 | case MGR: | |
267 | numAdded = db_addEmpls (db[(int) KND_MMGRS], l, h, s); | |
268 | numAdded += db_addEmpls (db[(int) KND_FMGRS], l, h, s); | |
269 | return numAdded; | |
270 | case NONMGR: | |
271 | numAdded = db_addEmpls (db[(int) KND_MNON], l, h, s); | |
272 | numAdded += db_addEmpls (db[(int) KND_FNON], l, h, s); | |
273 | return numAdded; | |
274 | } | |
275 | case MALE: | |
276 | switch (q.j) | |
277 | { | |
278 | case JOB_UNKNOWN: | |
279 | numAdded = db_addEmpls (db[(int) KND_MMGRS], l, h, s); | |
280 | numAdded += db_addEmpls (db[(int) KND_MNON], l, h, s); | |
281 | return numAdded; | |
282 | case MGR: | |
283 | return db_addEmpls (db[(int) KND_MMGRS], l, h, s); | |
284 | case NONMGR: | |
285 | return db_addEmpls (db[(int) KND_MNON], l, h, s); | |
286 | } | |
287 | case FEMALE: | |
288 | switch (q.j) | |
289 | { | |
290 | case JOB_UNKNOWN: | |
291 | numAdded = db_addEmpls (db[(int) KND_FMGRS], l, h, s); | |
292 | numAdded += db_addEmpls (db[(int) KND_FNON], l, h, s); | |
293 | return numAdded; | |
294 | case MGR: | |
295 | return db_addEmpls (db[(int) KND_FMGRS], l, h, s); | |
296 | case NONMGR: | |
297 | return db_addEmpls (db[(int) KND_FNON], l, h, s); | |
298 | } | |
299 | } | |
300 | } | |
301 | ||
302 | void db_print (void) | |
303 | /*@globals db@*/ | |
304 | { | |
305 | char *printVal; | |
306 | ||
307 | printf ("Employees:\n"); | |
308 | ||
309 | employeeKinds_all (ek) | |
310 | { | |
311 | printVal = erc_sprint (db[(int) ek]); | |
312 | printf ("%s", printVal); | |
313 | free (printVal); | |
314 | } end_employeeKinds_all ; | |
315 | } |