Changes in bool.h (previous version)

Added line 34 (was line 33)

> /*@noaccess bool@*/

Changes in dbase.c (previous version)

Replaced line 6 with line 6

<   mMGRS, fMGRS, mNON, fNON
---
>   KND_MMGRS, KND_FMGRS, KND_MNON, KND_FNON

Replaced line 10 with line 10

< # define firstERC mMGRS
---
> # define firstERC KND_MMGRS

Replaced line 13 with line 13

< # define lastERC fNON
---
> # define lastERC KND_FNON

Replaced line 59 with line 59

<   return erefNIL;
---
>   return eref_undefined;

Replaced line 69 with line 69 to line 70

<       if (!eref_equal (er, erefNIL))
---
> 
>       if (eref_isDefined (er))

Replaced line 75 with line 76

<   return erefNIL;
---
>   return eref_undefined;

Replaced line 98 with line 99

< db_status hire (employee e)
---
> db_status db_hire (employee e)

Replaced line 100 to line 101 with line 101 to line 102

<   if (e.gen == gender_ANY)
<     return genderERR;
---
>   if (e.gen == GENDER_UNKNOWN)
>     return DBS_GENDERERR;

Replaced line 103 to line 104 with line 104 to line 105

<   if (e.j == job_ANY)
<     return jobERR;
---
>   if (e.j == JOB_UNKNOWN)
>     return DBS_JOBERR;

Replaced line 107 with line 108

<     return salERR;
---
>     return DBS_SALERR;

Replaced line 109 to line 110 with line 110 to line 111

<   if (!eref_equal (db_keyGet (e.ssNum), erefNIL))
<     return duplERR;
---
>   if (eref_isDefined (db_keyGet (e.ssNum)))
>     return DBS_DUPLERR;

Replaced line 112 to line 113 with line 113 to line 114

<   uncheckedHire (e);
<   return db_OK;
---
>   db_uncheckedHire (e);
>   return DBS_OK;

Replaced line 116 with line 117

< void uncheckedHire (employee e)
---
> void db_uncheckedHire (employee e)

Replaced line 126 with line 127

<       erc_insert (db[(int) mMGRS], er);
---
>       erc_insert (db[(int) KND_MMGRS], er);

Replaced line 128 with line 129

<       erc_insert (db[(int) mNON], er);
---
>       erc_insert (db[(int) KND_MNON], er);

Replaced line 131 with line 132

<       erc_insert (db[(int) fMGRS], er);
---
>       erc_insert (db[(int) KND_FMGRS], er);

Replaced line 133 with line 134

<       erc_insert (db[(int) fNON], er);
---
>       erc_insert (db[(int) KND_FNON], er);

Replaced line 136 with line 137

< bool fire (int ssNum)
---
> bool db_fire (int ssNum)

Replaced line 154 with line 155

< bool promote (int ssNum)
---
> bool db_promote (int ssNum)

Replaced line 162 with line 163

<   er = db_ercKeyGet (db[(int) mNON], ssNum);
---
>   er = db_ercKeyGet (db[(int) KND_MNON], ssNum);

Replaced line 164 with line 165

<   if (eref_equal (er, erefNIL))
---
>   if (!eref_isDefined (er))

Replaced line 166 to line 167 with line 167 to line 168

<       er = db_ercKeyGet (db[(int) fNON], ssNum);
<       if (eref_equal (er, erefNIL))
---
>       er = db_ercKeyGet (db[(int) KND_FNON], ssNum);
>       if (!eref_isDefined (er))

Replaced line 178 to line 179 with line 179 to line 180

<       erc_delete (db[(int) mNON], er);
<       erc_insert (db[(int) mMGRS], er);
---
>       erc_delete (db[(int) KND_MNON], er);
>       erc_insert (db[(int) KND_MMGRS], er);

Replaced line 183 to line 184 with line 184 to line 185

<       erc_delete (db[(int) fNON], er);
<       erc_insert (db[(int) fMGRS], er);
---
>       erc_delete (db[(int) KND_FNON], er);
>       erc_insert (db[(int) KND_FMGRS], er);

Replaced line 190 with line 191

< db_status setSalary (int ssNum, int sal)
---
> db_status db_setSalary (int ssNum, int sal)

Replaced line 197 with line 198

<       return salERR;
---
>       return DBS_SALERR;

Replaced line 202 with line 203

<   if (eref_equal (er, erefNIL))
---
>   if (!eref_isDefined (er))

Replaced line 204 with line 205

<       return missERR;
---
>       return DBS_MISSERR;

Replaced line 211 with line 212

<   return db_OK;
---
>   return DBS_OK;

Replaced line 214 with line 215

< int query (db_q q, empset s)
---
> int db_query (db_q q, empset s)

Replaced line 225 with line 226

<     case gender_ANY:
---
>     case GENDER_UNKNOWN:

Replaced line 228 with line 229

<         case job_ANY:
---
>         case JOB_UNKNOWN:

Replaced line 238 to line 239 with line 239 to line 240

<           numAdded = db_addEmpls (db[(int) mMGRS], l, h, s);
<           numAdded += db_addEmpls (db[(int) fMGRS], l, h, s);
---
>           numAdded = db_addEmpls (db[(int) KND_MMGRS], l, h, s);
>           numAdded += db_addEmpls (db[(int) KND_FMGRS], l, h, s);

Replaced line 242 to line 243 with line 243 to line 244

<           numAdded = db_addEmpls (db[(int) mNON], l, h, s);
<           numAdded += db_addEmpls (db[(int) fNON], l, h, s);
---
>           numAdded = db_addEmpls (db[(int) KND_MNON], l, h, s);
>           numAdded += db_addEmpls (db[(int) KND_FNON], l, h, s);

Replaced line 249 to line 251 with line 250 to line 252

<         case job_ANY:
<           numAdded = db_addEmpls (db[(int) mMGRS], l, h, s);
<           numAdded += db_addEmpls (db[(int) mNON], l, h, s);
---
>         case JOB_UNKNOWN:
>           numAdded = db_addEmpls (db[(int) KND_MMGRS], l, h, s);
>           numAdded += db_addEmpls (db[(int) KND_MNON], l, h, s);

Replaced line 254 with line 255

<           return db_addEmpls (db[(int) mMGRS], l, h, s);
---
>           return db_addEmpls (db[(int) KND_MMGRS], l, h, s);

Replaced line 256 with line 257

<           return db_addEmpls (db[(int) mNON], l, h, s);
---
>           return db_addEmpls (db[(int) KND_MNON], l, h, s);

Replaced line 261 to line 263 with line 262 to line 264

<         case job_ANY:
<           numAdded = db_addEmpls (db[(int) fMGRS], l, h, s);
<           numAdded += db_addEmpls (db[(int) fNON], l, h, s);
---
>         case JOB_UNKNOWN:
>           numAdded = db_addEmpls (db[(int) KND_FMGRS], l, h, s);
>           numAdded += db_addEmpls (db[(int) KND_FNON], l, h, s);

Replaced line 266 with line 267

<           return db_addEmpls (db[(int) fMGRS], l, h, s);
---
>           return db_addEmpls (db[(int) KND_FMGRS], l, h, s);

Replaced line 268 with line 269

<           return db_addEmpls (db[(int) fNON], l, h, s);
---
>           return db_addEmpls (db[(int) KND_FNON], l, h, s);

Changes in dbase.lcl (previous version)

Replaced line 4 to line 5 with line 4 to line 5

< typedef enum {db_OK, salERR, genderERR, jobERR,
<               duplERR, missERR} db_status;
---
> typedef enum { DBS_OK, DBS_SALERR, DBS_GENDERERR, DBS_JOBERR,
>                DBS_DUPLERR, DBS_MISSERR } db_status;

Replaced line 17 with line 17

< db_status hire(employee e) db d; 
---
> db_status db_hire (employee e) db d;

Replaced line 32 with line 32

< void uncheckedHire(employee e) db d; 
---
> void db_uncheckedHire (employee e) db d;

Replaced line 41 with line 41

< bool fire(int ssNum) db d; 
---
> bool db_fire (int ssNum) db d;

Replaced line 49 with line 49

< int query(db_q q, empset s) db d; 
---
> int db_query (db_q q, empset s) db d;

Replaced line 57 with line 57

< bool promote(int ssNum) db d; 
---
> bool db_promote (int ssNum) db d;

Replaced line 68 with line 68

< db_status setSalary(int ssNum, int sal) db d; 
---
> db_status db_setSalary (int ssNum, int sal) db d;

Added line 97 (was line 96)

Changes in drive.c (previous version)

Replaced line 125 with line 125

<           check (hire(e) == db_OK); 
---
>           check (db_hire(e) == DBS_OK);

Replaced line 129 with line 129

<           uncheckedHire(e); status = hire(e);
---
>           db_uncheckedHire(e); status = db_hire(e);

Replaced line 134 with line 134

<          bool_unparse (/*@-usedef@*/ status == duplERR /*@=usedef@*/)); 
---
>          bool_unparse (/*@-usedef@*/ status == DBS_DUPLERR /*@=usedef@*/));

Replaced line 138 to line 139 with line 138 to line 139

<   check (fire(17));
<   q.g = FEMALE; q.j = job_ANY; q.l = 158; q.h = 185;
---
>   check (db_fire(17));
>   q.g = FEMALE; q.j = JOB_UNKNOWN; q.l = 158; q.h = 185;

Replaced line 144 with line 144

<   i = query(q, em1 = empset_create());
---
>   i = db_query(q, em1 = empset_create());

Replaced line 151 with line 151

<   i = query(q, em2 = empset_create());
---
>   i = db_query(q, em2 = empset_create());

Replaced line 165 with line 165

<   check (fire(empset_choose(em3).ssNum));
---
>   check (db_fire(empset_choose(em3).ssNum));

Changes in employee.c (previous version)

Replaced line 34 with line 34

<   (void) sprintf (s, employeeFormat, e.ssNum, e.name,
---
>   (void) sprintf (s, FORMATEMPLOYEE, e.ssNum, e.name,

Changes in employee.h (previous version)

Replaced line 8 with line 8

< # define employeeFormat "%9d  %-20s  %-6s  %-11s  %6d.00"
---
> # define FORMATEMPLOYEE "%9d  %-20s  %-6s  %-11s  %6d.00"

Changes in employee.lcl (previous version)

Replaced line 6 to line 7 with line 6 to line 7

< typedef enum { MALE, FEMALE, gender_ANY } gender;
< typedef enum { MGR, NONMGR, job_ANY } job;
---
> typedef enum { MALE, FEMALE, GENDER_UNKNOWN } gender;
> typedef enum { MGR, NONMGR, JOB_UNKNOWN } job;

Changes in empset.c (previous version)

Replaced line 15 with line 15

<   return erefNIL;
---
>   return eref_undefined;

Replaced line 20 with line 20

<   return (!eref_equal(empset_get (e, s), erefNIL));
---
>   return (eref_isDefined (empset_get (e, s)));

Replaced line 30 with line 30

<   if (!eref_equal (empset_get (e, s), erefNIL)) 
---
>   if (eref_isDefined (empset_get (e, s)))

Replaced line 47 with line 47

<   if (eref_equal (er, erefNIL)) 
---
>   if (!eref_isDefined (er))

Replaced line 63 with line 63

<   if (eref_equal (er, erefNIL)) 
---
>   if (!eref_isDefined (er))

Added line 67 (was line 66)

Changes in eref.c (previous version)

Replaced line 5 with line 5

< static eref_ERP eref_Pool;     /* private */
---
> static erefTable eref_Pool;     /* private */

Replaced line 14 with line 14

<   for (i=0; (eref_Pool.status[i] == used) && (i < eref_Pool.size); i++);
---
>   for (i=0; (eref_Pool.status[i] == ST_USED) && (i < eref_Pool.size); i++);

Replaced line 31 to line 32 with line 31 to line 32

<         (eref_status *) realloc (eref_Pool.status,
<                                  2 * eref_Pool.size * sizeof (eref_status));
---
>         (erefStatus *) realloc (eref_Pool.status,
>                                  2 * eref_Pool.size * sizeof (erefStatus));

Replaced line 43 with line 43

<         eref_Pool.status[i] = avail;
---
>         eref_Pool.status[i] = ST_AVAIL;

Replaced line 46 with line 46

<   eref_Pool.status[res] = used;
---
>   eref_Pool.status[res] = ST_USED;

Replaced line 74 with line 74

<   eref_Pool.status = (eref_status *) malloc (size * sizeof (eref_status));
---
>   eref_Pool.status = (erefStatus *) malloc (size * sizeof (erefStatus));

Replaced line 87 with line 87

<       eref_Pool.status[i] = avail;
---
>       eref_Pool.status[i] = ST_AVAIL;

Replaced line 96 with line 96

<   eref_Pool.status[er] = avail;
---
>   eref_Pool.status[er] = ST_AVAIL;

Changes in eref.h (previous version)

Replaced line 9 with line 9

< typedef enum { used, avail } eref_status;
---
> typedef enum { ST_USED, ST_AVAIL } erefStatus;

Replaced line 12 with line 12

<   /*@only@*/ eref_status *status;
---
>   /*@only@*/ erefStatus *status;

Replaced line 14 with line 14

< } eref_ERP;
---
> } erefTable;

Replaced line 18 with line 18 to line 20

< # define erefNIL -1
---
> # define eref_undefined -1
> 
> # define eref_isDefined(e)    ((e) != eref_undefined)

Added line 24 (was line 21)

Changes in eref.lcl (previous version)

Added line 4 to line 5 (was line 3)

> constant eref eref_undefined;
>

Deleted line 7 (matches line 8)

< constant eref erefNIL;

Added line 15 to line 16 (was line 13)

> 
> bool eref_isDefined (eref er) map m; { }

Changes in ereftab.c (previous version)

Replaced line 37 with line 37 to line 38

<   return erefNIL;
---
> 
>   return eref_undefined;