Replaced line 4 with line 4
< empset empset_create(void)
---
> only empset empset_create(void)
Replaced line 9 with line 9
< void empset_final(empset s)
---
> void empset_final (only empset s)
Replaced line 40 with line 40
< empset empset_union(empset s1, empset s2)
---
> only empset empset_union(empset s1, empset s2)
Replaced line 45 with line 45
< empset empset_disjointUnion(empset s1, empset s2)
---
> only empset empset_disjointUnion(empset s1, empset s2)
Replaced line 78 with line 78
< char *empset_sprint(empset s)
---
> only char *empset_sprint(empset s)
Deleted line 90 (matches line 89)
<
Added line 159 to line 163 (was line 158)
> eref erc_choose (erc c)
> {
> assert (c->vals != NULL);
> return c->vals->val;
> }
Replaced line 7 with line 7
< typedef struct _elem { eref val; struct _elem *next; } ercElem;
---
> typedef struct _elem { eref val; /*@null@*/ struct _elem *next; } ercElem;
Replaced line 15 with line 15
< # define erc_choose(c) (((c)->vals)->val)
---
>
Replaced line 23 with line 23
< eref m_x = m_ec->val; m_ec = m_ec->next; m_i++;
---
> eref m_x; assert (m_ec != NULL); m_x = m_ec->val; m_ec = m_ec->next; m_i++;
Replaced line 5 with line 5
< eref_ERP eref_Pool; /* private */
---
> static eref_ERP eref_Pool; /* private */
Added line 49 (was line 48)
> /*@globals undef eref_Pool@*/
Added line 89 to line 102 (was line 87)
> void eref_free (eref er)
> {
> eref_Pool.status[er] = avail;
> }
>
> void eref_assign (eref er, employee e)
> {
> eref_Pool.conts[er] = e;
> }
>
> employee eref_get (eref er)
> {
> return eref_Pool.conts[er];
> }
Deleted line 16 to line 18 (matches line 15)
< /* Declared here so that macros can use it */
< extern eref_ERP eref_Pool;
<
Deleted line 22 to line 25 (matches line 18)
<
< # define eref_free(er) (eref_Pool.status[er] = avail)
< # define eref_assign(er, e) (eref_Pool.conts[er] = (e))
< # define eref_get(er) (eref_Pool.conts[er])
Replaced line 5 with line 5
< ereftab ereftab_create(void)
---
> only ereftab ereftab_create(void)