Replaced line 20 with line 20 to line 21
< extern /*@unused@*/ void bool_initMod (void) /*@modifies internalState@*/ ;
---
> extern /*@unused@*/ void bool_initMod (void)
> /*@globals internalState@*/ /*@modifies internalState@*/ ;
Replaced line 22 with line 23
< # define bool_initMod()
---
> # define bool_initMod() do { ; } while (FALSE)
Replaced line 29 to line 30 with line 29 to line 30
< /*@globals initDone, undef db@*/
< /*@modifies initDone, db@*/
---
> /*@globals initDone, undef db, internalState@*/
> /*@modifies initDone, db, internalState@*/
Replaced line 51 with line 51
< static eref db_ercKeyGet(erc c, int key)
---
> static eref db_ercKeyGet(erc c, int key) /*@*/
Replaced line 55 with line 55 to line 58
< if (eref_get(er).ssNum == key) return (er);
---
> if (eref_get(er).ssNum == key)
> {
> return (er);
> }
Replaced line 61 with line 64
< static eref db_keyGet (int key)
---
> static eref db_keyGet (int key) /*@globals db@*/
Replaced line 79 with line 82 to line 83
< /*@modifies s@*/
---
> /*@globals internalState@*/
> /*@modifies s, internalState@*/
Replaced line 98 with line 102
< db_status db_hire (employee e)
---
> db_status db_hire (employee e) /*@globals db@*/
Added line 105 (was line 100)
> {
Added line 107 (was line 101)
> }
Added line 110 (was line 103)
> {
Added line 112 (was line 104)
> }
Added line 115 (was line 106)
> {
Added line 117 (was line 107)
> }
Added line 120 (was line 109)
> {
Added line 122 (was line 110)
> }
Replaced line 117 with line 129
< /*@globals db@*/
---
> /*@globals db@*/ /*@modifies db@*/
Added line 137 (was line 124)
> {
Added line 139 (was line 125)
> {
Added line 141 (was line 126)
> }
Added line 143 (was line 127)
> {
Added line 145 to line 146 (was line 128)
> }
> }
Added line 148 (was line 129)
> {
Added line 150 (was line 130)
> {
Added line 152 (was line 131)
> }
Added line 154 (was line 132)
> {
Added line 157 to line 158 (was line 134)
> }
> }
Replaced line 137 with line 161
< /*@globals db@*/
---
> /*@globals db@*/ /*@modifies db@*/
Replaced line 155 with line 179
< /*@globals db@*/
---
> /*@globals db@*/ /*@modifies db@*/
Added line 191 (was line 166)
>
Added line 193 (was line 167)
> {
Added line 195 to line 196 (was line 168)
> }
>
Replaced line 190 with line 218
< db_status db_setSalary (int ssNum, int sal)
---
> db_status db_setSalary (int ssNum, int sal) /*@globals db@*/
Replaced line 41 with line 41
< bool db_fire (int ssNum) db d;
---
> bool db_fire (int ssNum) db d; internalState;
Replaced line 43 with line 43
< modifies d;
---
> modifies d, internalState;
Replaced line 49 with line 49
< int db_query (db_q q, empset s) db d;
---
> int db_query (db_q q, empset s) db d; internalState;
Replaced line 51 with line 51
< modifies s;
---
> modifies s, internalState;
Replaced line 92 with line 92
< void db_initMod(void) db d;
---
> void db_initMod(void) db d; internalState;
Replaced line 94 with line 94
< modifies d;
---
> modifies d, internalState;
Added line 13 (was line 12)
> /*@globals internalState@*/ /*@modifies internalState@*/
Replaced line 118 to line 119 with line 119 to line 137
< if (i < 10) e.gen = MALE; else e.gen = FEMALE;
< if (i < 15) e.j = NONMGR; else e.j = MGR;
---
>
> if (i < 10)
> {
> e.gen = MALE;
> }
> else
> {
> e.gen = FEMALE;
> }
>
> if (i < 15)
> {
> e.j = NONMGR;
> }
> else
> {
> e.j = MGR;
> }
>
Replaced line 11 with line 11 to line 14
< if (i == maxEmployeeName) return FALSE;
---
> if (i == maxEmployeeName)
> {
> return FALSE;
> }
Replaced line 49 with line 49
< void employee_initMod(void)
---
> void employee_initMod(void) internalState;
Replaced line 6 with line 6
< static eref empset_get (employee e, erc s)
---
> static eref empset_get (employee e, erc s) /*@*/
Added line 11 (was line 10)
>
Added line 13 (was line 11)
> {
Added line 15 (was line 12)
> }
Added line 32 to line 33 (was line 28)
> /*@globals internalState@*/
> /*@modifies internalState@*/
Added line 120 (was line 114)
> {
Added line 122 (was line 115)
> }
Added line 135 (was line 127)
> {
Added line 137 (was line 128)
> }
Replaced line 143 with line 152 to line 155
< if (!empset_member(emp, s2)) return FALSE;
---
> if (!empset_member(emp, s2))
> {
> return FALSE;
> }
Replaced line 21 with line 21
< | bool : void | empset_insert(empset s, employee e)
---
> | bool : void | empset_insert (empset s, employee e) internalState;
Replaced line 23 with line 23
< modifies s;
---
> modifies s, internalState;
Replaced line 27 with line 27
< void empset_insertUnique(empset s, employee e)
---
> void empset_insertUnique (empset s, employee e) internalState;
Replaced line 40 with line 40
< only empset empset_union(empset s1, empset s2)
---
> only empset empset_union(empset s1, empset s2) internalState;
Added line 42 (was line 41)
> modifies internalState;
Replaced line 45 with line 46
< only empset empset_disjointUnion(empset s1, empset s2)
---
> only empset empset_disjointUnion (empset s1, empset s2) internalState;
Replaced line 52 with line 53
< void empset_intersect(empset s1, empset s2)
---
> void empset_intersect (empset s1, empset s2) internalState;
Replaced line 54 with line 55
< modifies s1;
---
> modifies s1, internalState;
Replaced line 84 with line 85
< void empset_initMod(void)
---
> void empset_initMod (void) internalState;
Added line 2 (was line 1)
>
Replaced line 4 with line 5
< static size_t int_toSize (int x)
---
> static size_t int_toSize (int x) /*@*/
Replaced line 21 with line 22
< c = (erc) malloc (sizeof (ercInfo));
---
> c = (erc) malloc (sizeof (*c));
Replaced line 60 with line 61 to line 66
< if (eref_equal (tmpc->val, er)) return TRUE;
---
> {
> if (eref_equal (tmpc->val, er))
> {
> return TRUE;
> }
> }
Replaced line 68 with line 74
< newElem = (ercElem *) malloc (sizeof (ercElem));
---
> newElem = (ercElem *) malloc (sizeof (*newElem));
Added line 128 (was line 121)
> {
Added line 130 (was line 122)
> }
Added line 7 (was line 6)
> /*@-exporttype@*/ /* These types should not be exported, but are used in macros. */
Added line 11 to line 12 (was line 9)
> /*@=exporttype@*/
>
Replaced line 66 with line 66
< void erc_initMod(void)
---
> void erc_initMod (void) internalState;
Added line 5 to line 11 (was line 4)
> typedef enum { ST_USED, ST_AVAIL } erefStatus;
> typedef struct {
> /*@reldef@*/ /*@only@*/ employee *conts;
> /*@only@*/ erefStatus *status;
> int size;
> } erefTable;
>
Replaced line 14 with line 21 to line 24
< for (i=0; (eref_Pool.status[i] == ST_USED) && (i < eref_Pool.size); i++);
---
> for (i=0; (eref_Pool.status[i] == ST_USED) && (i < eref_Pool.size); i++)
> {
> ;
> }
Replaced line 22 with line 32
< 2 * eref_Pool.size * sizeof (employee));
---
> 2 * eref_Pool.size * sizeof (*eref_Pool.conts));
Replaced line 32 with line 42
< 2 * eref_Pool.size * sizeof (erefStatus));
---
> 2 * eref_Pool.size * sizeof (*eref_Pool.status));
Added line 53 (was line 42)
> {
Added line 56 (was line 44)
> }
Replaced line 51 to line 52 with line 63 to line 64
< /*@globals undef eref_Pool, needsInit@*/
< /*@modifies eref_Pool, needsInit@*/
---
> /*@globals undef eref_Pool, needsInit, internalState@*/
> /*@modifies eref_Pool, needsInit, internalState@*/
Replaced line 66 with line 78
< eref_Pool.conts = (employee *) malloc (size * sizeof (employee));
---
> eref_Pool.conts = (employee *) malloc (size * sizeof (*eref_Pool.conts));
Replaced line 74 with line 86
< eref_Pool.status = (erefStatus *) malloc (size * sizeof (erefStatus));
---
> eref_Pool.status = (erefStatus *) malloc (size * sizeof (*eref_Pool.status));
Deleted line 8 to line 15 (matches line 7)
< /* Private typedefs used in macros */
< typedef enum { ST_USED, ST_AVAIL } erefStatus;
< typedef struct {
< /*@reldef@*/ /*@only@*/ employee *conts;
< /*@only@*/ erefStatus *status;
< int size;
< } erefTable;
<
Replaced line 43 with line 43
< void eref_initMod(void) map m;
---
> void eref_initMod(void) map m; internalState;
Replaced line 45 with line 45
< modifies m;
---
> modifies m, internalState;
Replaced line 35 with line 35 to line 39
< if (employee_equal(&e, &e1)) return er;
---
>
> if (employee_equal(&e, &e1))
> {
> return er;
> }
Replaced line 28 with line 28
< void ereftab_initMod(void)
---
> void ereftab_initMod (void) internalState;