Replaced line 1 with line 1
< #if !defined(BOOL_H)
---
> #ifndef BOOL_H
Added line 3 to line 4 (was line 2)
>
> #ifndef FALSE
Added line 6 to line 8 (was line 3)
> #endif
>
> #ifndef TRUE
Added line 10 to line 11 (was line 4)
> #endif
>
Added line 13 to line 21 (was line 5)
>
> /*
> ** bool_initMod has no real effect
> ** Declared with modifies internalState, so no noeffect errors are
> ** reported when it is called.)
> */
>
> extern /*@unused@*/ void bool_initMod (void) /*@modifies internalState@*/ ;
> /*@-mustmod@*/
Added line 23 to line 33 (was line 6)
> /*@=mustmod@*/
>
> extern /*@unused@*/ /*@observer@*/ char *bool_unparse (bool b) /*@*/ ;
> # define bool_unparse(b) ((b) ? "true" : "false" )
>
> extern /*@unused@*/ bool bool_not (bool b) /*@*/ ;
> # define bool_not(b) ((b) ? FALSE : TRUE)
>
> extern /*@unused@*/ bool bool_equal (bool b1, bool b2) /*@*/ ;
> # define bool_equal(a,b) ((a) ? (b) : !(b))
>
Replaced line 8 with line 8 to line 11
< typedef enum {mMGRS, fMGRS, mNON, fNON} employeeKinds;
---
> typedef enum
> {
> mMGRS, fMGRS, mNON, fNON
> } employeeKinds;
Replaced line 14 with line 17 to line 18
< void db_initMod(void) {
---
> void db_initMod (void)
> {
Replaced line 16 with line 20 to line 25
< if (initDone) return;
---
>
> if (initDone)
> {
> return;
> }
>
Added line 31 (was line 21)
>
Added line 33 (was line 22)
> {
Added line 35 to line 36 (was line 23)
> }
>
Replaced line 27 with line 40 to line 41
< eref _db_ercKeyGet(erc c, int key) {
---
> eref _db_ercKeyGet (erc c, int key)
> {
Added line 44 (was line 29)
>
Replaced line 31 with line 46 to line 52
< if (eref_get(er).ssNum == key) erc_iterReturn(it, er);
---
> {
> if (eref_get (er).ssNum == key)
> {
> erc_iterReturn (it, er);
> }
> }
>
Replaced line 35 to line 36 with line 56 to line 57
<
< eref _db_keyGet(int key) {
---
> eref _db_keyGet (int key)
> {
Replaced line 39 with line 60 to line 62
< for (i = firstERC; i <= lastERC; i++) {
---
>
> for (i = firstERC; i <= lastERC; i++)
> {
Replaced line 41 with line 64 to line 66
< if (!eref_equal(er, erefNIL)) return er;
---
> if (!eref_equal (er, erefNIL))
> {
> return er;
Added line 68 to line 69 (was line 42)
> }
>
Replaced line 46 with line 73 to line 74
< int _db_addEmpls(erc c, int l, int h, empset s) {
---
> int _db_addEmpls (erc c, int l, int h, empset s)
> {
Replaced line 52 with line 80 to line 82
< for_ercElems (er, it, c) {
---
>
> for_ercElems (er, it, c)
> {
Replaced line 54 with line 84 to line 85
< if ((e.salary >= l) && (e.salary <= h)) {
---
> if ((e.salary >= l) && (e.salary <= h))
> {
Added line 90 (was line 58)
>
Replaced line 62 to line 65 with line 94 to line 104
< db_status hire(employee e) {
< if (e.gen == gender_ANY) return genderERR;
< if (e.j == job_ANY) return jobERR;
< if (e.salary < 0) return salERR;
---
> db_status hire (employee e)
> {
> if (e.gen == gender_ANY)
> return genderERR;
>
> if (e.j == job_ANY)
> return jobERR;
>
> if (e.salary < 0)
> return salERR;
>
Added line 107 (was line 67)
>
Replaced line 72 with line 112 to line 113
< void uncheckedHire(employee e) {
---
> void uncheckedHire (employee e)
> {
Added line 115 (was line 73)
>
Added line 118 (was line 75)
>
Replaced line 79 to line 80 with line 122 to line 125
< else erc_insert(db[mNON], er);
< else if (e.j == MGR)
---
> else
> erc_insert (db[mNON], er);
> else
> if (e.j == MGR)
Replaced line 82 with line 127 to line 128
< else erc_insert(db[fNON], er);
---
> else
> erc_insert (db[fNON], er);
Replaced line 85 with line 131 to line 132
< bool fire(int ssNum) {
---
> bool fire (int ssNum)
> {
Added line 136 (was line 88)
>
Replaced line 91 with line 139 to line 140
< if (eref_get(er).ssNum == ssNum) {
---
> if (eref_get (er).ssNum == ssNum)
> {
Added line 145 (was line 95)
>
Replaced line 99 with line 149 to line 150
< bool promote(int ssNum) {
---
> bool promote (int ssNum)
> {
Added line 154 (was line 102)
>
Replaced line 105 with line 157 to line 159
< if (eref_equal(er, erefNIL)) {
---
>
> if (eref_equal (er, erefNIL))
> {
Replaced line 107 with line 161 to line 162
< if (eref_equal(er, erefNIL)) return FALSE;
---
> if (eref_equal (er, erefNIL))
> return FALSE;
Added line 165 (was line 109)
>
Replaced line 113 with line 169 to line 171
< if (g == MALE) {
---
>
> if (g == MALE)
> {
Replaced line 117 with line 175 to line 176
< else {
---
> else
> {
Added line 180 (was line 120)
>
Replaced line 124 with line 184 to line 185
< db_status setSalary(int ssNum, int sal) {
---
> db_status setSalary (int ssNum, int sal)
> {
Replaced line 127 with line 188 to line 193
< if (sal < 0) return salERR;
---
>
> if (sal < 0)
> {
> return salERR;
> }
>
Replaced line 129 with line 195 to line 200
< if (eref_equal(er, erefNIL)) return missERR;
---
>
> if (eref_equal (er, erefNIL))
> {
> return missERR;
> }
>
Added line 204 (was line 132)
>
Replaced line 136 with line 208 to line 209
< int query(db_q q, empset s) {
---
> int query (db_q q, empset s)
> {
Added line 215 (was line 141)
>
Replaced line 144 with line 218 to line 220
< switch(q.g) {
---
>
> switch (q.g)
> {
Replaced line 146 with line 222 to line 223
< switch(q.j) {
---
> switch (q.j)
> {
Replaced line 162 with line 239 to line 240
< switch(q.j) {
---
> switch (q.j)
> {
Replaced line 173 with line 251 to line 252
< switch(q.j) {
---
> switch (q.j)
> {
Replaced line 186 with line 265 to line 266
< void db_print(void) {
---
> void db_print (void)
> {
Added line 269 (was line 188)
>
Replaced line 190 with line 271 to line 273
< for (i = firstERC; i <= lastERC; i++) {
---
>
> for (i = firstERC; i <= lastERC; i++)
> {
Replaced line 1 with line 1
< #if !defined(DBASE_H)
---
> # ifndef DBASE_H
Replaced line 1 with line 1
< imports employee, empset, stdio;
---
> imports employee, empset, <stdio>;
Replaced line 9 to line 12 with line 9 to line 11
< uses dbase, sprint(ioStream, db);
<
< claims UniqueKeys(employee e1, employee e2) db d; {
< ensures
---
> claims UniqueKeys (employee e1, employee e2) db d;
> {
> /* ensures
Added line 14 (was line 14)
> */
Replaced line 17 with line 17 to line 18
< db_status hire(employee e) db d; {
---
> db_status hire(employee e) db d;
> {
Replaced line 19 with line 20
< ensures
---
> /* ensures
Added line 29 (was line 27)
> */
Replaced line 29 to line 30 with line 31 to line 34
< void uncheckedHire(employee e) db d; {
< requires e.gen \neq gender_ANY /\ e.j \neq job_ANY
---
>
> void uncheckedHire(employee e) db d;
> {
> /* requires e.gen \neq gender_ANY /\ e.j \neq job_ANY
Added line 36 (was line 31)
> */
Replaced line 33 with line 38
< ensures d' = hire(e, d^);
---
> /* ensures d' = hire(e, d^); */
Replaced line 35 with line 40 to line 42
< bool fire(int ssNum) db d; {
---
>
> bool fire(int ssNum) db d;
> {
Replaced line 37 with line 44
< ensures result = employed(d^, ssNum)
---
> /* ensures result = employed(d^, ssNum)
Added line 46 (was line 38)
> */
Replaced line 40 with line 48 to line 50
< int query(db_q q, empset s) db d; {
---
>
> int query(db_q q, empset s) db d;
> {
Replaced line 42 with line 52
< ensures s' = s^ \U query(d^, q)
---
> /* ensures s' = s^ \U query(d^, q)
Added line 54 (was line 43)
> */
Replaced line 45 with line 56 to line 58
< bool promote(int ssNum) db d; {
---
>
> bool promote(int ssNum) db d;
> {
Replaced line 47 with line 60
< ensures
---
> /* ensures
Added line 65 (was line 51)
> */
Replaced line 53 with line 67 to line 69
< db_status setSalary(int ssNum, int sal) db d; {
---
>
> db_status setSalary(int ssNum, int sal) db d;
> {
Added line 71 (was line 54)
> /*
Added line 80 (was line 62)
> */
Replaced line 64 with line 82 to line 84
< void db_print(void) db d; FILE *stdout; {
---
>
> void db_print(void) db d; FILE *stdout;
> {
Added line 86 (was line 65)
> /*
Replaced line 68 with line 89
<
---
> */
Replaced line 70 with line 91 to line 93
< void db_initMod(void) db d; {
---
>
> void db_initMod(void) db d;
> {
Replaced line 72 with line 95
< ensures d' = new;
---
> /* ensures d' = new; */
Replaced line 11 to line 12 with line 11 to line 12
< int main(int argc, char *argv[]) {
<
---
> int main(int argc, char *argv[])
> {
Replaced line 26 with line 26 to line 27
< if (argc != 1) {
---
> if (argc != 1)
> {
Replaced line 34 to line 35 with line 35 to line 42
< if (!(empset_size(em1) == 0)) printf("Size should be 0.\n");
< for (i = 0; i < 500; i++) {
---
>
> if (!(empset_size(em1) == 0))
> {
> printf("Size should be 0.\n");
> }
>
> for (i = 0; i < 500; i++)
> {
Replaced line 44 to line 45 with line 51 to line 58
< if (!(empset_size(em1) == 500)) printf("Size should be 500.\n");
< for (i = 0; i < 250; i++) {
---
>
> if (!(empset_size(em1) == 500))
> {
> printf("Size should be 500.\n");
> }
>
> for (i = 0; i < 250; i++)
> {
Replaced line 54 with line 67 to line 72
< if (!(empset_size(em1) == 250)) printf("Size should be 250.\n");
---
>
> if (!(empset_size(em1) == 250))
> {
> printf("Size should be 250.\n");
> }
>
Replaced line 56 with line 74 to line 76
< for (i = 0; i < 100; i++) {
---
>
> for (i = 0; i < 100; i++)
> {
Added line 85 (was line 64)
>
Replaced line 66 with line 87 to line 92
< if (!(empset_size(em3) == 350)) printf("Size should be 350.\n");
---
>
> if (!(empset_size(em3) == 350))
> {
> printf("Size should be 350.\n");
> }
>
Replaced line 68 with line 94 to line 99
< if (!(empset_size(em3) == 350)) printf("Size should be 350.\n");
---
>
> if (!(empset_size(em3) == 350))
> {
> printf("Size should be 350.\n");
> }
>
Replaced line 70 with line 101 to line 103
< for (i = 0; i < 2; i++) {
---
>
> for (i = 0; i < 2; i++)
> {
Deleted line 77 to line 78 (matches line 109)
<
<
Replaced line 80 with line 111 to line 113
< for (i = 0; i < 20; i++) {
---
>
> for (i = 0; i < 20; i++)
> {
Replaced line 87 to line 88 with line 120 to line 123
< if ( (i/2)*2 == i) hire(e);
< else {uncheckedHire(e); j = hire(e);}
---
>
> if ((i/2)*2 == i)
> {
> hire(e);
Added line 125 to line 130 (was line 89)
> else
> {
> uncheckedHire(e); j = hire(e);
> }
> }
>
Added line 138 (was line 96)
>
Added line 143 (was line 100)
>
Added line 151 (was line 107)
>
Added line 157 (was line 112)
>
Added line 161 (was line 115)
>
Added line 2 (was line 1)
> # include <string.h>
Replaced line 4 with line 5 to line 6
< bool employee_setName(employee *e, char na []) {
---
> bool employee_setName (employee *e, char na [])
> {
Added line 10 (was line 7)
> {
Added line 12 to line 13 (was line 8)
> }
>
Replaced line 12 with line 17 to line 19
< bool employee_equal(employee * e1, employee * e2) {
---
>
> bool employee_equal (employee * e1, employee * e2)
> {
Replaced line 17 to line 18 with line 24
< && (strncmp(e1->name, e2->name,
< maxEmployeeName) == 0));
---
> && (strncmp (e1->name, e2->name, maxEmployeeName) == 0));
Replaced line 20 with line 26 to line 28
< void employee_sprint(char s[], employee e) {
---
>
> void employee_sprint (char s[], employee e)
> {
Replaced line 24 to line 30 with line 32 to line 33
< (void) sprintf(s,
< employeeFormat,
< e.ssNum,
< e.name,
< gender[e.gen],
< jobs[e.j],
< e.salary);
---
> (void) sprintf (s, employeeFormat, e.ssNum, e.name,
> gender[e.gen], jobs[e.j], e.salary);
Replaced line 1 with line 1
< #if !defined(EMPLOYEE_H)
---
> # ifndef EMPLOYEE_H
Replaced line 6 with line 6 to line 9
< typedef struct {int ssNum;
---
>
> typedef struct
> {
> int ssNum;
Replaced line 10 with line 13 to line 14
< job j;} employee;
---
> job j;
> } employee;
Replaced line 12 to line 15 with line 16 to line 18
< uses employeeConstants, sprint(employee, char[]);
<
< void employee_sprint(char s[], employee e) {
< requires maxIndex(s) >= employeePrintSize;
---
> void employee_sprint (out char s[], employee e)
> {
> /* requires maxIndex(s) >= employeePrintSize; */
Replaced line 17 with line 20
< ensures isSprint(s', e)
---
> /* ensures isSprint(s', e)
Added line 22 (was line 18)
> */
Replaced line 20 to line 21 with line 24 to line 27
< bool employee_equal(employee *e1, employee *e2) {
< ensures result = sameStr(e1->name^, e2->name^)
---
>
> bool employee_equal (employee *e1, employee *e2)
> {
> /* ensures result = sameStr(e1->name^, e2->name^)
Added line 32 (was line 25)
> */
Replaced line 27 to line 28 with line 34 to line 37
< bool employee_setName(employee *e, char na[]) {
< requires nullTerminated(na^);
---
>
> bool employee_setName(employee *e, char na[])
> {
> /* requires nullTerminated(na^); */
Replaced line 30 with line 39
< ensures result = lenStr(na^) < maxEmployeeName
---
> /* ensures result = lenStr(na^) < maxEmployeeName
Added line 44 (was line 34)
> */
Replaced line 36 with line 46 to line 48
< void employee_initMod(void) {
---
>
> void employee_initMod(void)
> {
Replaced line 5 with line 5 to line 6
< eref _empset_get(employee e, erc s) {
---
> eref _empset_get (employee e, erc s)
> {
Replaced line 9 with line 10 to line 12
< for_ercElems(er, it, s) {
---
>
> for_ercElems (er, it, s)
> {
Added line 17 (was line 13)
>
Replaced line 17 with line 21 to line 22
< void empset_clear(empset s) {
---
> void empset_clear (empset s)
> {
Replaced line 21 with line 26 to line 27
< bool empset_insert(empset s, employee e) {
---
> bool empset_insert (empset s, employee e)
> {
Replaced line 23 with line 29 to line 34
< if (!eref_equal(_empset_get(e, s), erefNIL)) return FALSE;
---
>
> if (!eref_equal (_empset_get (e, s), erefNIL))
> {
> return FALSE;
> }
>
Replaced line 28 with line 39 to line 40
< void empset_insertUnique(empset s, employee e) {
---
> void empset_insertUnique (empset s, employee e)
> {
Added line 42 (was line 29)
>
Replaced line 31 with line 44 to line 46
< if (eref_equal(er, erefNIL)) {
---
>
> if (eref_equal (er, erefNIL))
> {
Added line 51 (was line 35)
>
Replaced line 39 with line 55 to line 56
< bool empset_delete(empset s, employee e) {
---
> bool empset_delete (empset s, employee e)
> {
Added line 58 (was line 40)
>
Replaced line 42 with line 60 to line 64
< if (eref_equal(er, erefNIL)) return FALSE;
---
>
> if (eref_equal (er, erefNIL))
> {
> return FALSE;
> }
Replaced line 46 with line 68 to line 69
< empset empset_disjointUnion(empset s1, empset s2) {
---
> empset empset_disjointUnion (empset s1, empset s2)
> {
Added line 74 (was line 50)
>
Replaced line 52 with line 76 to line 78
< if (erc_size(s1) > erc_size(s2)) {
---
>
> if (erc_size (s1) > erc_size (s2))
> {
Added line 83 (was line 56)
>
Added line 87 (was line 59)
>
Replaced line 63 with line 91 to line 92
< empset empset_union(empset s1, empset s2) {
---
> empset empset_union (empset s1, empset s2)
> {
Added line 97 (was line 67)
>
Replaced line 69 with line 99 to line 101
< if (erc_size(s1) > erc_size(s2)) {
---
>
> if (erc_size (s1) > erc_size (s2))
> {
Added line 107 (was line 74)
>
Added line 111 (was line 77)
>
Replaced line 81 with line 115 to line 116
< void empset_intersect(empset s1, empset s2) {
---
> void empset_intersect (empset s1, empset s2)
> {
Added line 120 (was line 84)
>
Added line 122 (was line 85)
>
Added line 126 (was line 88)
>
Added line 129 (was line 90)
>
Replaced line 94 with line 133 to line 134
< bool empset_subset(empset s1, empset s2) {
---
> bool empset_subset (empset s1, empset s2)
> {
Added line 142 (was line 101)
>
Replaced line 105 with line 146 to line 147
< void empset_initMod(void) {
---
> void empset_initMod (void)
> {
Added line 149 (was line 106)
>
Replaced line 1 with line 1
< #if !defined(EMPSET_H)
---
> # ifndef EMPSET_H
Added line 35 (was line 34)
>
Deleted line 3 to line 4 (matches line 2)
< uses Set(employee, empset),
< sprint(empset, char[]);
Replaced line 6 to line 7 with line 4 to line 6
< empset empset_create(void) {
< ensures fresh(result) /\ result' = { };
---
> empset empset_create(void)
> {
> /* ensures fresh(result) /\ result' = { }; */
Replaced line 9 with line 8 to line 10
< void empset_final(empset s) {
---
>
> void empset_final(empset s)
> {
Replaced line 11 with line 12
< ensures trashed(s);
---
> /* ensures trashed(s); */
Replaced line 13 with line 14 to line 16
< void empset_clear(empset s) {
---
>
> void empset_clear(empset s)
> {
Replaced line 15 with line 18
< ensures s' = { };
---
> /* ensures s' = { }; */
Replaced line 17 with line 20 to line 22
< bool empset_insert(empset s, employee e) {
---
>
> bool empset_insert(empset s, employee e)
> {
Replaced line 19 with line 24
< ensures result = ~(e \in s^) /\ s' = insert(e, s^);
---
> /* ensures result = ~(e \in s^) /\ s' = insert(e, s^); */
Replaced line 21 to line 22 with line 26 to line 29
< void empset_insertUnique(empset s, employee e) {
< requires ~(e \in s^);
---
>
> void empset_insertUnique(empset s, employee e)
> {
> /* requires ~(e \in s^); */
Replaced line 24 with line 31
< ensures s' = insert(e, s^);
---
> /* ensures s' = insert(e, s^); */
Replaced line 26 with line 33 to line 35
< bool empset_delete(empset s, employee e) {
---
>
> bool empset_delete(empset s, employee e)
> {
Replaced line 28 with line 37
< ensures result = e \in s^ /\ s' = delete(e, s^);
---
> /* ensures result = e \in s^ /\ s' = delete(e, s^); */
Replaced line 30 to line 31 with line 39 to line 42
< empset empset_union(empset s1, empset s2) {
< ensures result' = s1^ \U s2^ /\ fresh(result);
---
>
> empset empset_union(empset s1, empset s2)
> {
> /* ensures result' = s1^ \U s2^ /\ fresh(result); */
Replaced line 33 to line 35 with line 44 to line 48
< empset empset_disjointUnion(empset s1, empset s2) {
< requires s1^ \I s2^ = { };
< ensures result' = s1^ \U s2^ /\ fresh(result);
---
>
> empset empset_disjointUnion(empset s1, empset s2)
> {
> /* requires s1^ \I s2^ = { }; */
> /* ensures result' = s1^ \U s2^ /\ fresh(result); */
Replaced line 37 with line 50 to line 52
< void empset_intersect(empset s1, empset s2) {
---
>
> void empset_intersect(empset s1, empset s2)
> {
Replaced line 39 with line 54
< ensures s1' = s1^ \I s2^;
---
> /* ensures s1' = s1^ \I s2^; */
Replaced line 41 to line 42 with line 56 to line 59
< int empset_size(empset s) {
< ensures result = size(s^);
---
>
> int empset_size(empset s)
> {
> /* ensures result = size(s^); */
Replaced line 44 to line 45 with line 61 to line 64
< bool empset_member(employee e, empset s) {
< ensures result = e \in s^;
---
>
> bool empset_member(employee e, empset s)
> {
> /* ensures result = e \in s^; */
Replaced line 47 to line 48 with line 66 to line 69
< bool empset_subset(empset s1, empset s2) {
< ensures result = s1^ \subseteq s2^;
---
>
> bool empset_subset(empset s1, empset s2)
> {
> /* ensures result = s1^ \subseteq s2^; */
Replaced line 50 to line 52 with line 71 to line 75
< employee empset_choose(empset s) {
< requires s^ \neq { };
< ensures result \in s^;
---
>
> employee empset_choose(empset s)
> {
> /* requires s^ \neq { }; */
> /* ensures result \in s^; */
Replaced line 54 to line 55 with line 77 to line 80
< char *empset_sprint(empset s) {
< ensures isSprint(result[]', s^) /\ fresh(result[]);
---
>
> char *empset_sprint(empset s)
> {
> /* ensures isSprint(result[]', s^) /\ fresh(result[]); */
Replaced line 57 with line 82 to line 84
< void empset_initMod(void) {
---
>
> void empset_initMod(void)
> {
Added line 1 (was line 0)
> # include <stdlib.h>
Replaced line 3 with line 4 to line 5
< erc erc_create(void) {
---
> erc erc_create (void)
> {
Added line 7 (was line 4)
>
Replaced line 6 with line 9 to line 11
< if (c == 0) {
---
>
> if (c == 0)
> {
Added line 15 (was line 9)
>
Replaced line 15 with line 21 to line 22
< void erc_clear(erc c) {
---
> void erc_clear (erc c)
> {
Replaced line 18 with line 25 to line 27
< for (elem = c->vals; elem != 0; elem = next) {
---
>
> for (elem = c->vals; elem != 0; elem = next)
> {
Added line 31 (was line 21)
>
Replaced line 26 with line 36 to line 37
< void erc_final(erc c) {
---
> void erc_final (erc c)
> {
Replaced line 31 with line 42 to line 43
< bool erc_member(eref er, erc c) {
---
> bool erc_member (eref er, erc c)
> {
Added line 45 (was line 32)
>
Added line 48 (was line 34)
>
Replaced line 38 with line 52 to line 53
< void erc_insert(erc c, eref er) {
---
> void erc_insert (erc c, eref er)
> {
Replaced line 41 with line 56 to line 58
< if (newElem == 0) {
---
>
> if (newElem == 0)
> {
Added line 62 (was line 44)
>
Replaced line 51 with line 69 to line 70
< bool erc_delete(erc c, eref er) {
---
> bool erc_delete (erc c, eref er)
> {
Replaced line 57 to line 58 with line 76 to line 79
< prev = elem, elem = elem->next) {
< if (elem->val == er) {
---
> prev = elem, elem = elem->next)
> {
> if (elem->val == er)
> {
Replaced line 61 with line 82 to line 84
< else {prev->next = elem->next;}
---
> else
> prev->next = elem->next;
>
Added line 90 (was line 66)
>
Replaced line 70 with line 94 to line 95
< ercIter erc_iterStart(erc c) {
---
> ercIter erc_iterStart (erc c)
> {
Added line 97 (was line 71)
>
Replaced line 73 with line 99 to line 101
< if (result == 0) {
---
>
> if (result == 0)
> {
Added line 105 (was line 76)
>
Replaced line 81 with line 110 to line 111
< eref erc_yield(ercIter it) {
---
> eref erc_yield (ercIter it)
> {
Replaced line 83 with line 113 to line 115
< if (*it == 0) {
---
>
> if (*it == 0)
> {
Added line 119 (was line 86)
>
Replaced line 92 with line 125 to line 126
< void erc_join(erc c1, erc c2) {
---
> void erc_join (erc c1, erc c2)
> {
Added line 128 (was line 93)
>
Replaced line 98 with line 133 to line 134
< char * erc_sprint(erc c) {
---
> char *erc_sprint (erc c)
> {
Replaced line 103 to line 105 with line 139 to line 144
< result = (char*)malloc(erc_size(c)
< *(employeePrintSize+1)+1);
< if (result == 0) {
---
>
> result = (char *)
> malloc (erc_size (c) * (employeePrintSize + 1) + 1);
>
> if (result == 0)
> {
Added line 148 (was line 108)
>
Replaced line 110 with line 150 to line 152
< for_ercElems (er, it, c) {
---
>
> for_ercElems (er, it, c)
> {
Added line 157 (was line 114)
>
Replaced line 1 with line 1
< #if !defined(ERC_H)
---
> # ifndef ERC_H
Added line 19 (was line 18)
>
Added line 21 (was line 19)
>
Added line 24 (was line 21)
>
Added line 29 (was line 25)
>
Replaced line 6 to line 9 with line 6 to line 8
< uses erc(obj erc for ercObj), sprint(erc, char[]);
<
< erc erc_create(void) {
< ensures fresh(result) /\ result' = { };
---
> erc erc_create(void)
> {
> /* ensures fresh(result) /\ result' = { }; */
Replaced line 11 to line 12 with line 10 to line 13
< void erc_clear(erc c) {
< requires c^.activeIters = 0;
---
>
> void erc_clear(erc c)
> {
> /* requires c^.activeIters = 0; */
Replaced line 14 with line 15
< ensures c' = { };
---
> /* ensures c' = { }; */
Replaced line 16 to line 17 with line 17 to line 20
< void erc_insert(erc c, eref er) {
< requires c^.activeIters = 0 /\ er \neq erefNIL;
---
>
> void erc_insert(erc c, eref er)
> {
> /* requires c^.activeIters = 0 /\ er \neq erefNIL; */
Replaced line 19 with line 22
< ensures c' = [insert(er, c^.val), 0];
---
> /* ensures c' = [insert(er, c^.val), 0]; */
Replaced line 21 to line 22 with line 24 to line 27
< bool erc_delete(erc c, eref er) {
< requires c^.activeIters = 0;
---
>
> bool erc_delete(erc c, eref er)
> {
> /* requires c^.activeIters = 0; */
Replaced line 24 to line 25 with line 29 to line 30
< ensures result = er \in c^.val
< /\ c' = [delete(er, c^.val), 0];
---
> /* ensures result = er \in c^.val
> /\ c' = [delete(er, c^.val), 0]; */
Replaced line 27 to line 28 with line 32 to line 35
< bool erc_member(eref er, erc c) {
< ensures result = er \in c^.val;
---
>
> bool erc_member(eref er, erc c)
> {
> /* ensures result = er \in c^.val; */
Replaced line 30 to line 32 with line 37 to line 41
< eref erc_choose(erc c) {
< requires size(c^.val) \neq 0;
< ensures result \in c^.val;
---
>
> eref erc_choose(erc c)
> {
> /* requires size(c^.val) \neq 0; */
> /* ensures result \in c^.val; */
Replaced line 34 to line 35 with line 43 to line 46
< int erc_size(erc c) {
< ensures result = size(c^.val);
---
>
> int erc_size(erc c)
> {
> /* ensures result = size(c^.val); */
Replaced line 37 with line 48 to line 50
< ercIter erc_iterStart(erc c) {
---
>
> ercIter erc_iterStart(erc c)
> {
Replaced line 39 with line 52
< ensures fresh(result) /\ result' = [c^.val, c]
---
> /* ensures fresh(result) /\ result' = [c^.val, c]
Added line 54 (was line 40)
> */
Replaced line 42 to line 44 with line 56 to line 60
< eref erc_yield(ercIter it) {
< modifies it, it^.eObj;
< ensures if it^.toYield \neq { }
---
>
> eref erc_yield(ercIter it)
> {
> modifies it; /* , it^.eObj */
> /* ensures if it^.toYield \neq { }
Added line 65 (was line 48)
> */
Replaced line 50 to line 52 with line 67 to line 71
< void erc_iterFinal(ercIter it) {
< modifies it, it^.eObj;
< ensures trashed(it)
---
>
> void erc_iterFinal(ercIter it)
> {
> modifies it; /* , it^.eObj; */
> /* ensures trashed(it)
Added line 73 (was line 53)
> */
Replaced line 55 to line 56 with line 75 to line 78
< void erc_join(erc c1, erc c2) {
< requires c1^.activeIters = 0;
---
>
> void erc_join(erc c1, erc c2)
> {
> /* requires c1^.activeIters = 0; */
Replaced line 58 with line 80
< ensures c1' = [c1^.val \U c2^.val, 0];
---
> /* ensures c1' = [c1^.val \U c2^.val, 0]; */
Replaced line 60 to line 61 with line 82 to line 85
< char *erc_sprint(erc c) {
< ensures isSprint(result[]', c^) /\ fresh(result[]);
---
>
> char *erc_sprint(erc c)
> {
> /* ensures isSprint(result[]', c^) /\ fresh(result[]); */
Replaced line 63 with line 87 to line 89
< void erc_final(erc c) {
---
>
> void erc_final(erc c)
> {
Replaced line 65 with line 91
< ensures trashed(c);
---
> /* ensures trashed(c); */
Replaced line 67 with line 93 to line 95
< void erc_initMod(void) {
---
>
> void erc_initMod(void)
> {
Added line 2 (was line 1)
> # include <stdlib.h>
Replaced line 7 with line 8 to line 9
< eref eref_alloc(void) {
---
> eref eref_alloc (void)
> {
Replaced line 10 to line 13 with line 12 to line 13
< for (i=0;
< (eref_Pool.status[i] == used)
< && (i < eref_Pool.size);
< i++);
---
> for (i=0; (eref_Pool.status[i] == used) && (i < eref_Pool.size); i++);
>
Replaced line 15 with line 15 to line 17
< if (res == eref_Pool.size) {
---
>
> if (res == eref_Pool.size)
> {
Replaced line 20 with line 22 to line 23
< if (eref_Pool.conts == 0) {
---
> if (eref_Pool.conts == 0)
> {
Added line 27 (was line 23)
>
Replaced line 27 with line 31 to line 33
< if (eref_Pool.status == 0) {
---
>
> if (eref_Pool.status == 0)
> {
Added line 37 (was line 30)
>
Added line 39 (was line 31)
>
Added line 43 (was line 34)
>
Replaced line 38 with line 47 to line 49
< void eref_initMod(void) {
---
>
> void eref_initMod (void)
> {
Replaced line 42 with line 53 to line 57
< if (needsInit == FALSE) return;
---
> if (needsInit == FALSE)
> {
> return;
> }
>
Replaced line 46 to line 48 with line 61 to line 65
< eref_Pool.conts =
< (employee *) malloc(size*sizeof(employee));
< if (eref_Pool.conts == 0) {
---
>
> eref_Pool.conts = (employee *) malloc (size * sizeof (employee));
>
> if (eref_Pool.conts == 0)
> {
Replaced line 52 to line 54 with line 69 to line 73
< eref_Pool.status =
< (eref_status *) malloc(size*sizeof(eref_status));
< if (eref_Pool.status == 0) {
---
>
> eref_Pool.status = (eref_status *) malloc (size * sizeof (eref_status));
>
> if (eref_Pool.status == 0)
> {
Added line 77 (was line 57)
>
Replaced line 59 with line 79 to line 83
< for (i = 0; i < size; i++) eref_Pool.status[i] = avail;
---
>
> for (i = 0; i < size; i++)
> {
> eref_Pool.status[i] = avail;
> }
Replaced line 1 with line 1
< #if !defined(EREF_H)
---
> # ifndef EREF_H
Replaced line 10 with line 10 to line 11
< typedef struct {employee *conts;
---
> typedef struct {
> employee *conts;
Replaced line 12 with line 13 to line 14
< int size;} eref_ERP;
---
> int size;
> } eref_ERP;
Added line 22 (was line 19)
>
Added line 27 (was line 23)
>
Deleted line 6 to line 7 (matches line 5)
< uses refTable(eref, employee, map);
<
Replaced line 9 with line 7
< constant eref erefNIL = nil;
---
> constant eref erefNIL;
Replaced line 11 with line 9 to line 10
< eref eref_alloc(void) map m; {
---
> eref eref_alloc(void) map m;
> {
Replaced line 13 with line 12
< ensures newInd(result, m^, m');
---
> /* ensures newInd(result, m^, m'); */
Replaced line 15 to line 16 with line 14 to line 17
< void eref_free(eref er) map m; {
< requires er \in domain(m^);
---
>
> void eref_free(eref er) map m;
> {
> /* requires er \in domain(m^); */
Replaced line 18 with line 19
< ensures m' = delete(m^, er);
---
> /* ensures m' = delete(m^, er); */
Replaced line 20 to line 21 with line 21 to line 24
< void eref_assign(eref er, employee e) map m; {
< requires er \in domain(m^);
---
>
> void eref_assign(eref er, employee e) map m;
> {
> /* requires er \in domain(m^); */
Replaced line 23 with line 26
< ensures m' = assign(m^, er, e);
---
> /* ensures m' = assign(m^, er, e); */
Replaced line 25 to line 27 with line 28 to line 32
< employee eref_get(eref er) map m; {
< requires er \in domain(m^);
< ensures result = m^[er];
---
>
> employee eref_get(eref er) map m;
> {
> /* requires er \in domain(m^); */
> /* ensures result = m^[er]; */
Replaced line 29 to line 30 with line 34 to line 37
< bool eref_equal(eref er1, eref er2) {
< ensures result = (er1 = er2);
---
>
> bool eref_equal(eref er1, eref er2)
> {
> /* ensures result = (er1 = er2); */
Replaced line 32 with line 39 to line 41
< void eref_initMod(void) map m; {
---
>
> void eref_initMod(void) map m;
> {
Replaced line 34 with line 43
< ensures m' = new;
---
> /* ensures m' = new; */
Replaced line 1 with line 1 to line 4
< /* ereftab.c */
---
> /*
> ** This is not a good implementation. I should probably replace
> ** the erc with a hash table.
> */
Deleted line 3 to line 5 (matches line 5)
< /* This is not a good implementation. I should probably replace
< the erc with a hash table. */
<
Replaced line 8 with line 8 to line 9
< ereftab ereftab_create(void) {
---
> ereftab ereftab_create (void)
> {
Replaced line 12 with line 13 to line 14
< void ereftab_insert(ereftab t, employee e, eref er) {
---
> void ereftab_insert (ereftab t, employee e, eref er)
> {
Replaced line 17 with line 19 to line 20
< bool ereftab_delete(ereftab t, eref er) {
---
> bool ereftab_delete (ereftab t, eref er)
> {
Replaced line 25 with line 28 to line 29
< eref ereftab_lookup(employee e, ereftab t) {
---
> eref ereftab_lookup (employee e, ereftab t)
> {
Replaced line 30 with line 34 to line 35
< for_ercElems(er, it, t) {
---
> for_ercElems (er, it, t)
> {
Added line 39 (was line 33)
>
Replaced line 37 with line 43 to line 44
< void ereftab_initMod(void) {
---
> void ereftab_initMod (void)
> {
Replaced line 3 with line 3
< #if !defined(EREFTAB_H)
---
> # ifndef EREFTAB_H
Replaced line 5 to line 8 with line 5 to line 7
< uses ereftab;
<
< ereftab ereftab_create(void) {
< ensures result' = empty;
---
> ereftab ereftab_create(void)
> {
> /* ensures result' = empty; */
Replaced line 10 to line 11 with line 9 to line 12
< void ereftab_insert(ereftab t, employee e, eref er) {
< requires getERef(t^, e) = erefNIL;
---
>
> void ereftab_insert(ereftab t, employee e, eref er)
> {
> /* requires getERef(t^, e) = erefNIL; */
Replaced line 13 with line 14
< ensures t' = add(t^, e, er);
---
> /* ensures t' = add(t^, e, er); */
Replaced line 15 with line 16 to line 18
< bool ereftab_delete(ereftab t, eref er) {
---
>
> bool ereftab_delete(ereftab t, eref er)
> {
Replaced line 17 with line 20
< ensures result = in(t^, er) /\ t' = delete(t^, er);
---
> /* ensures result = in(t^, er) /\ t' = delete(t^, er); */
Replaced line 19 to line 20 with line 22 to line 25
< eref ereftab_lookup(employee e, ereftab t) {
< ensures result = getERef(t^, e);
---
>
> eref ereftab_lookup(employee e, ereftab t)
> {
> /* ensures result = getERef(t^, e); */
Replaced line 22 with line 27 to line 29
< void ereftab_initMod(void) {
---
>
> void ereftab_initMod(void)
> {