Replaced line 42 to line 45 with line 42
< eref er;
< ercIter it;
<
< for_ercElems (er, it, c)
---
> erc_elements(c, er)
Replaced line 47 to line 51 with line 44 to line 45
< if (eref_get (er).ssNum == key)
< {
< erc_iterReturn (it, er);
< }
< }
---
> if (eref_get(er).ssNum == key) return (er);
> } end_erc_elements ;
Deleted line 75 to line 76 (matches line 68)
< eref er;
< ercIter it;
Replaced line 81 with line 73
< for_ercElems (er, it, c)
---
> erc_elements (c, er)
Replaced line 89 with line 81
< }
---
> } end_erc_elements ;
Deleted line 134 to line 135 (matches line 125)
< eref er;
< ercIter it;
Replaced line 138 with line 128 to line 130
< for_ercElems (er, it, db[i])
---
> {
> erc_elements(db[i], er)
> {
Deleted line 141 (matches line 132)
< erc_iterFinal (it);
Added line 135 to line 136 (was line 143)
> }
> } end_erc_elements ;
Replaced line 7 to line 11 with line 7
< eref er;
< ercIter it;
< employee e1;
<
< for_ercElems (er, it, s)
---
> erc_elements(s, er)
Replaced line 13 with line 9
< e1 = eref_get (er);
---
> employee e1 = eref_get(er);
Replaced line 15 to line 16 with line 11 to line 12
< erc_iterReturn (it, er);
< }
---
> return er;
> } end_erc_elements ;
Deleted line 69 to line 70 (matches line 64)
< ercIter it;
< eref er;
Deleted line 83 to line 86 (matches line 76)
< /*@-mods@*/
< for_ercElems (er, it, s2)
< empset_insertUnique (result, eref_get (er));
< /*@=mods@*/
Added line 78 to line 82 (was line 87)
> empset_elements(s2, emp)
> {
> empset_insertUnique(result, emp);
> } end_empset_elements ;
>
Deleted line 93 to line 94 (matches line 87)
< eref er;
< ercIter it;
Replaced line 108 to line 112 with line 101 to line 105
< /*@-mods@*/
< for_ercElems (er, it, s1)
< if (!empset_member (eref_get (er), s2))
< erc_insert (result, er);
< /*@=mods@*/
---
> empset_elements (s1, emp)
> {
> if (!empset_member(emp, s2))
> empset_insert(result, emp);
> } end_empset_elements ;
Replaced line 119 to line 121 with line 112
< eref er;
< ercIter it;
< erc toDelete;
---
> erc toDelete = erc_create();
Replaced line 123 with line 114 to line 118
< toDelete = erc_create ();
---
> empset_elements (s2, emp)
> {
> if (!empset_member(emp, s2))
> empset_insert(toDelete, emp);
> } end_empset_elements ;
Replaced line 125 to line 127 with line 120 to line 123
< for_ercElems (er, it, s1)
< if (!empset_member (eref_get (er), s2))
< erc_insert (toDelete, er);
---
> empset_elements (toDelete, emp)
> {
> empset_delete(s1, emp);
> } end_empset_elements;
Deleted line 129 to line 131 (matches line 124)
< for_ercElems (er, it, toDelete)
< erc_delete (s1, er);
<
Replaced line 137 to line 144 with line 130 to line 133
< eref er;
< ercIter it;
<
< /*@-mods@*/
< for_ercElems (er, it, s1)
< if (!empset_member (eref_get (er), s2))
< erc_iterReturn (it, FALSE);
< /*@=mods@*/
---
> empset_elements(s1, emp)
> {
> if (!empset_member(emp, s2)) return FALSE;
> } end_empset_elements ;
Added line 36 to line 39 (was line 35)
> #define empset_elements(e, m_x) \
> erc_elements(e, m_y) { employee m_x = eref_get(m_y);
> #define end_empset_elements } end_erc_elements
>
Added line 87 to line 89 (was line 86)
>
> iter empset_elements (empset s, yield employee x);
>
Deleted line 115 to line 145 (matches line 114)
< ercIter erc_iterStart (erc c)
< {
< ercIter result;
<
< result = (ercIter) malloc (sizeof (ercList));
<
< if (result == 0)
< {
< printf ("Malloc returned null in erc_iterStart\n");
< exit (1);
< }
<
< *result = c->vals;
< return result;
< }
<
< eref erc_yield (ercIter it)
< {
< eref result;
<
< if (*it == 0)
< {
< return erefNIL;
< free (it);
< }
<
< result = (*it)->val;
< *(it) = (*it)->next;
< return result;
< }
<
Deleted line 157 to line 158 (matches line 125)
< eref er;
< ercIter it;
Replaced line 172 to line 173 with line 139
< /*@-mods@*/
< for_ercElems (er, it, c)
---
> erc_elements(c, er)
Replaced line 178 to line 179 with line 144
< }
< /*@=mods@*/
---
> } end_erc_elements;
Deleted line 10 (matches line 9)
< typedef ercList *ercIter;
Replaced line 20 with line 19 to line 22
< # define erc_iterFinal(it) (free(it))
---
> # define erc_elements(c, m_x) \
> { erc m_c = (c); ercElem *m_ec = (m_c)->vals; int m_i = 0; \
> while (m_i < (m_c)->size) { \
> eref m_x = m_ec->val; m_ec = m_ec->next; m_i++;
Replaced line 22 to line 28 with line 24
< # define erc_iterReturn(it, result) \
< do { erc_iterFinal(it); return result; } while (0)
<
< # define for_ercElems(er, it, c)\
< for (er = erc_yield (it = erc_iterStart (c)); \
< !eref_equal (er, erefNIL); \
< er = erc_yield (it))
---
> # define end_erc_elements }}
Deleted line 4 (matches line 3)
< mutable type ercIter;
Deleted line 49 to line 75 (matches line 47)
< ercIter erc_iterStart(erc c)
< {
< modifies c;
< /* ensures fresh(result) /\ result' = [c^.val, c]
< /\ c' = startIter(c^);
< */
< }
<
< eref erc_yield(ercIter it)
< {
< modifies it; /* , it^.eObj */
< /* ensures if it^.toYield \neq { }
< then yielded(result, it^, it')
< /\ (it^.eObj)' = (it^.eObj)^
< else result = erefNIL /\ trashed(it)
< /\ (it^.eObj)' = endIter((it^.eObj)^);
< */
< }
<
< void erc_iterFinal(ercIter it)
< {
< modifies it; /* , it^.eObj; */
< /* ensures trashed(it)
< /\ (it^.eObj)' = endIter((it^.eObj)^);
< */
< }
<
Added line 70 to line 71 (was line 97)
>
> iter erc_elements (erc c, yield eref el);
Deleted line 30 (matches line 29)
< eref er;
Deleted line 32 (matches line 30)
< ercIter it;
Replaced line 34 to line 35 with line 32
< /*@-mods@*/
< for_ercElems (er, it, t)
---
> ereftab_elements(t, er)
Replaced line 38 to line 44 with line 35 to line 36
< if (employee_equal (&e, &e1))
< {
< erc_iterReturn (it, er);
< }
< }
< /*@=mods@*/
<
---
> if (employee_equal(&e, &e1)) return er;
> } end_ereftab_elements ;
Added line 12 to line 14 (was line 11)
> # define ereftab_elements(s, m_x) erc_elements(s, m_x)
> # define end_ereftab_elements end_erc_elements
>
Added line 32 to line 35 (was line 31)
>
> iter ereftab_elements(ereftab s, yield eref x);
>
>