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 58 with line 58

<   return erefNIL;
---
>   return eref_undefined;

Replaced line 68 with line 68 to line 69

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

Replaced line 74 with line 75

<   return erefNIL;
---
>   return eref_undefined;

Replaced line 97 with line 98

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

Replaced line 99 to line 100 with line 100 to line 101

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

Replaced line 102 to line 103 with line 103 to line 104

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

Replaced line 106 with line 107

<     return salERR;
---
>     return DBS_SALERR;

Replaced line 108 to line 109 with line 109 to line 110

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

Replaced line 111 to line 112 with line 112 to line 113

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

Replaced line 115 with line 116

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

Replaced line 125 with line 126

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

Replaced line 127 with line 128

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

Replaced line 130 with line 131

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

Replaced line 132 with line 133

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

Replaced line 135 with line 136

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

Replaced line 153 with line 154

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

Replaced line 161 with line 162

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

Replaced line 163 with line 164

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

Replaced line 165 to line 166 with line 166 to line 167

<       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 177 to line 178 with line 178 to line 179

<       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 182 to line 183 with line 183 to line 184

<       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 189 with line 190

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

Replaced line 196 with line 197

<       return salERR;
---
>       return DBS_SALERR;

Replaced line 201 with line 202

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

Replaced line 203 with line 204

<       return missERR;
---
>       return DBS_MISSERR;

Replaced line 210 with line 211

<   return db_OK;
---
>   return DBS_OK;

Replaced line 213 with line 214

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

Replaced line 224 with line 225

<     case gender_ANY:
---
>     case GENDER_UNKNOWN:

Replaced line 227 with line 228

<         case job_ANY:
---
>         case JOB_UNKNOWN:

Replaced line 237 to line 238 with line 238 to line 239

<           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 241 to line 242 with line 242 to line 243

<           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 248 to line 250 with line 249 to line 251

<         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 253 with line 254

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

Replaced line 255 with line 256

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

Replaced line 260 to line 262 with line 261 to line 263

<         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 265 with line 266

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

Replaced line 267 with line 268

<           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;