Changes in dbase.c (previous version)

Replaced line 16 with line 16

< # define numERCS (lastERC - firstERC + 1)
---
> # define numERCS (/*@+enumint@*/ (lastERC - firstERC + 1) /*@=enumint@*/)

Replaced line 18 with line 18 to line 19

< erc db[numERCS];
---
> typedef /*@only@*/ erc o_erc;
> static o_erc db[numERCS];

Replaced line 20 with line 21 to line 23

< bool initDone = FALSE;
---
> /*@iter employeeKinds_all (yield employeeKinds ek); @*/
> # define employeeKinds_all(m_ek) \
>   { employeeKinds m_ek; for (m_ek = firstERC; m_ek <= lastERC; m_ek++) {

Added line 25 to line 28 (was line 21)

> # define end_employeeKinds_all }}
> 
> static bool initDone = FALSE;
>

Added line 30 to line 31 (was line 22)

>   /*@globals initDone, undef db@*/
>   /*@modifies initDone, db@*/

Deleted line 24 to line 25 (matches line 32)

<   int i;
<

Replaced line 37 with line 44

<   for (i = firstERC; i <= lastERC; i++)
---
>   employeeKinds_all (ek)

Replaced line 39 to line 40 with line 46 to line 47

<       db[i] = erc_create ();
<     }
---
>       db[(int)ek] = erc_create ();
>     } end_employeeKinds_all ;

Replaced line 45 with line 52

< eref _db_ercKeyGet (erc c, int key) 
---
> static eref db_ercKeyGet(erc c, int key)

Replaced line 55 with line 62

< eref _db_keyGet (int key)
---
> static eref db_keyGet (int key)

Deleted line 57 (matches line 63)

<   int i;

Replaced line 60 with line 66

<   for (i = firstERC; i <= lastERC; i++)
---
>   employeeKinds_all (ek)

Replaced line 62 with line 68

<       er = _db_ercKeyGet (db[i], key);
---
>       er = db_ercKeyGet (db[(int) ek], key);

Replaced line 67 with line 73

<     }
---
>     } end_employeeKinds_all ;

Replaced line 72 with line 78 to line 79

< int _db_addEmpls (erc c, int l, int h, empset s)
---
> static int db_addEmpls (erc c, int l, int h, empset s)
>   /*@modifies s@*/

Replaced line 102 with line 109

<   if (!eref_equal (_db_keyGet (e.ssNum), erefNIL))
---
>   if (!eref_equal (db_keyGet (e.ssNum), erefNIL))

Added line 117 (was line 109)

>    /*@globals db@*/

Replaced line 118 with line 126

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

Replaced line 120 with line 128

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

Replaced line 123 with line 131

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

Replaced line 125 with line 133

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

Added line 137 (was line 128)

>   /*@globals db@*/

Replaced line 130 to line 132 with line 139

<   int i;
<   
<   for (i = firstERC; i <= lastERC; i++)
---
>   employeeKinds_all (ek)

Replaced line 134 with line 141

<       erc_elements(db[i], er)
---
>       erc_elements (db[(int) ek], er)

Replaced line 138 with line 145

<               erc_delete(db[i], er);
---
>               erc_delete (db[(int) ek], er);

Replaced line 142 with line 149

<     }
---
>     } end_employeeKinds_all ;

Added line 155 (was line 147)

>   /*@globals db@*/

Replaced line 154 with line 162

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

Replaced line 158 with line 166

<       er = _db_ercKeyGet (db[fNON], ssNum);
---
>       er = db_ercKeyGet (db[(int) fNON], ssNum);

Replaced line 170 to line 171 with line 178 to line 179

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

Replaced line 175 to line 176 with line 183 to line 184

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

Replaced line 192 with line 200

<   er = _db_keyGet (ssNum);
---
>   er = db_keyGet (ssNum);

Added line 215 (was line 206)

>   /*@globals db@*/

Deleted line 210 (matches line 218)

<   int i;

Replaced line 222 to line 223 with line 230 to line 235

<           for (i = firstERC; i <= lastERC; i++)
<             numAdded += _db_addEmpls (db[i], l, h, s);
---
> 
>           employeeKinds_all (ek)
>             {
>               numAdded += db_addEmpls (db[(int) ek], l, h, s);
>             } end_employeeKinds_all
>

Replaced line 226 to line 227 with line 238 to line 239

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

Replaced line 230 to line 231 with line 242 to line 243

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

Replaced line 238 to line 239 with line 250 to line 251

<           numAdded = _db_addEmpls (db[mMGRS], l, h, s);
<           numAdded += _db_addEmpls (db[mNON], l, h, s);
---
>           numAdded = db_addEmpls (db[(int) mMGRS], l, h, s);
>           numAdded += db_addEmpls (db[(int) mNON], l, h, s);

Replaced line 242 with line 254

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

Replaced line 244 with line 256

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

Replaced line 250 to line 251 with line 262 to line 263

<           numAdded = _db_addEmpls (db[fMGRS], l, h, s);
<           numAdded += _db_addEmpls (db[fNON], l, h, s);
---
>           numAdded = db_addEmpls (db[(int) fMGRS], l, h, s);
>           numAdded += db_addEmpls (db[(int) fNON], l, h, s);

Replaced line 254 with line 266

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

Replaced line 256 with line 268

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

Added line 274 (was line 261)

>   /*@globals db@*/

Deleted line 263 (matches line 275)

<   int i;

Replaced line 268 with line 280

<   for (i = firstERC; i <= lastERC; i++)
---
>   employeeKinds_all (ek)

Replaced line 270 with line 282

<       printVal = erc_sprint (db[i]);
---
>       printVal = erc_sprint (db[(int) ek]);

Replaced line 273 with line 285

<     }
---
>     } end_employeeKinds_all ;

Changes in drive.c (previous version)

Replaced line 18 with line 18 to line 19

<   int i, j;
---
>   int i;
>   db_status status;

Replaced line 128 with line 129

<           uncheckedHire(e); j = hire(e);
---
>           uncheckedHire(e); status = hire(e);

Replaced line 132 with line 133 to line 135

<   printf("Should print 4: %d\n", /*@-usedef@*/ j /*@=usedef@*/); 
---
>   printf("Should print true: %s\n", 
>          bool_unparse (/*@-usedef@*/ status == duplERR /*@=usedef@*/)); 
>

Changes in employee.c (previous version)

Added line 27 to line 28 (was line 26)

> typedef /*@observer@*/ char *obscharp;
>

Replaced line 29 to line 30 with line 31 to line 32

<   static char *gender[] ={ "male", "female", "?" };
<   static char *jobs[] = { "manager", "non-manager", "?" };
---
>   static obscharp gender[] ={ "male", "female", "?" };
>   static obscharp jobs[] = { "manager", "non-manager", "?" };

Replaced line 33 with line 35

<                   gender[e.gen], jobs[e.j], e.salary);
---
>                   gender[(int) e.gen], jobs[(int) e.j], e.salary);

Changes in empset-mod.c (previous version)

Changes in empset.c (previous version)

Replaced line 5 with line 5

< eref _empset_get (employee e, erc s) 
---
> static eref empset_get (employee e, erc s)

Added line 17 to line 21 (was line 16)

> bool empset_member (employee e, erc s)
> {
>   return (!eref_equal(empset_get (e, s), erefNIL));
> }
>

Replaced line 24 with line 29

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

Added line 39 (was line 33)

>    /*@globals known@*/

Replaced line 53 with line 59

<   er = _empset_get (e, s);
---
>   er = empset_get (e, s);

Added line 145 to line 146 (was line 138)

>   /*@globals initDone, undef known@*/
>   /*@modifies initDone, known@*/

Changes in empset.h (previous version)

Replaced line 10 with line 10

< ereftab known;
---
> /*@only@*/ ereftab known;

Deleted line 30 to line 31 (matches line 29)

< # define empset_member(e, s) \
<          (!(eref_equal(_empset_get(e, s), erefNIL)))

Changes in erc.c (previous version)

Replaced line 13 to line 21 with line 13

<       size_t s = (size_t) x;
< 
<       if ((int) s != x)
<         {
<           fprintf (stderr, "Error: int_toSize is inconsistent: %d", x);
<           return 0;
<         }
< 
<       return s;
---
>       return (size_t) x;

Changes in eref.c (previous version)

Added line 9 to line 10 (was line 8)

>    /*@globals eref_Pool@*/
>    /*@modifies eref_Pool@*/

Replaced line 49 with line 51 to line 52

<    /*@globals undef eref_Pool@*/
---
>    /*@globals undef eref_Pool, needsInit@*/
>    /*@modifies eref_Pool, needsInit@*/

Added line 93 to line 94 (was line 89)

>   /*@globals eref_Pool@*/
>   /*@modifies eref_Pool@*/

Added line 100 to line 101 (was line 94)

>   /*@globals eref_Pool@*/
>   /*@modifies eref_Pool@*/

Added line 107 (was line 99)

>    /*@globals eref_Pool@*/