Changes in employee.lcl (previous version)

Replaced line 37 with line 37

< bool employee_setName(employee *e, char na[]) 
---
> bool employee_setName (employee *e, unique char na[])

Changes in empset-next.lcl (previous version)

Changes in erc.c (previous version)

Replaced line 92 to line 93 with line 92

<   ercList elem;
<   ercList prev;
---
>   ercList elem = c->vals;

Replaced line 95 to line 97 with line 94

<   for (prev = 0, elem = c->vals;
<        elem != 0;
<        prev = elem, elem = elem->next) 
---
>   if (elem != NULL)

Deleted line 101 (matches line 97)

<           if (prev == 0)

Added line 99 to line 102 (was line 102)

>           free (elem);
>           c->size--;
>           return TRUE;
>         }

Replaced line 104 with line 104 to line 106

<             prev->next = elem->next;
---
>         {
>           ercList prev = elem;
>           elem = elem->next;

Added line 108 to line 112 (was line 105)

>           for (; elem != 0; prev = elem, elem = elem->next) 
>             {
>               if (eref_equal (elem->val, er))
>                 { 
>                   prev->next = elem->next;

Added line 116 to line 117 (was line 108)

>                 }
>             }

Changes in erc.h (previous version)

Added line 4 (was line 3)

> # include <assert.h>

Replaced line 8 with line 9

< typedef struct { ercList vals; int size; } ercInfo;
---
> typedef struct { /*@null@*/ ercList vals; int size; } ercInfo;

Changes in erc.lcl (previous version)

Replaced line 5 with line 5

< erc erc_create(void) 
---
> only erc erc_create(void)

Replaced line 55 with line 55

< char *erc_sprint(erc c) 
---
> only char *erc_sprint(erc c)

Replaced line 60 with line 60

< void erc_final(erc c) 
---
> void erc_final (only erc c)

Changes in eref.c (previous version)

Added line 80 (was line 79)

>   /*@+loopexec@*/

Added line 85 (was line 83)

>   /*@=loopexec@*/

Changes in eref.h (previous version)

Replaced line 11 to line 12 with line 11 to line 12

<   employee *conts;
<   eref_status *status;
---
>   /*@reldef@*/ /*@only@*/ employee *conts;
>   /*@only@*/ eref_status *status;