Changes in drive.c (previous version)


Replaced line 12 with line 12
< int main(int argc, char *argv[]) 
---
> int main (int argc, /*@unused@*/ char *argv[]) 

Replaced line 49 with line 49
<       employee_setName(&e, na);
---
>       check (employee_setName(&e, na));

Replaced line 65 with line 65
<       employee_setName(&e, na);
---
>       check (employee_setName(&e, na));

Replaced line 83 with line 83
<       employee_setName(&e, na);
---
>       check (employee_setName(&e, na));

Replaced line 120 with line 120
<       employee_setName(&e, na);
---
>       check (employee_setName(&e, na));

Replaced line 132 with line 132
<   printf("Should print 4: %d\n", j); 
---
>   printf("Should print 4: %d\n", /*@-usedef@*/ j /*@=usedef@*/); 

Replaced line 135 with line 135
<   fire(17);
---
>   check (fire(17));

Replaced line 159 with line 159
<   fire(empset_choose(em3).ssNum);
---
>   check (fire(empset_choose(em3).ssNum));

Changes in employee.lcl (previous version)


Added line 51 (was line 50)
>   modifies internalState;

Changes in empset.c (previous version)


Replaced line 22 with line 22
< bool empset_insert (empset s, employee e) 
---
> bool /*@alt void@*/ empset_insert (empset s, employee e) 

Replaced line 49 with line 49
< bool empset_delete (empset s, employee e) 
---
> bool /*@alt void@*/ empset_delete (empset s, employee e) 

Changes in empset.lcl (previous version)


Replaced line 21 with line 21
< bool empset_insert(empset s, employee e) 
---
> | bool : void | empset_insert(empset s, employee e) 

Replaced line 34 with line 34
< bool empset_delete(empset s, employee e) 
---
> | bool : void | empset_delete(empset s, employee e) 

Added line 85 (was line 84)
>   modifies internalState;

Changes in erc.c (previous version)


Replaced line 34 with line 34
<       exit (1);
---
>       exit (EXIT_FAILURE);

Replaced line 81 with line 81
<       exit (1);
---
>       exit (EXIT_FAILURE);

Replaced line 134 with line 134
<       exit (1);
---
>       exit (EXIT_FAILURE);

Changes in erc.h (previous version)


Replaced line 14 with line 14
< # define erc_choose(c) ((c->vals)->val)
---
> # define erc_choose(c) (((c)->vals)->val)

Changes in erc.lcl (previous version)


Replaced line 24 with line 24
< bool erc_delete(erc c, eref er) 
---
> | bool : void | erc_delete(erc c, eref er) 

Added line 68 (was line 67)
>   modifies internalState;

Changes in eref.c (previous version)


Replaced line 25 with line 25
<           exit (1);
---
>           exit (EXIT_FAILURE);

Replaced line 35 with line 35
<           exit (1);
---
>           exit (EXIT_FAILURE);

Replaced line 53 with line 53
<   if (needsInit == FALSE) 
---
>   if (!needsInit) 

Replaced line 67 with line 67
<       exit (1);
---
>       exit (EXIT_FAILURE);

Replaced line 75 with line 75
<       exit (1);
---
>       exit (EXIT_FAILURE);

Changes in eref.h (previous version)


Replaced line 24 with line 24
< # define eref_assign(er, e)   (eref_Pool.conts[er] = e) 
---
> # define eref_assign(er, e)   (eref_Pool.conts[er] = (e))

Replaced line 26 with line 26
< # define eref_equal(er1, er2) (er1 == er2) 
---
> # define eref_equal(er1, er2) ((er1) == (er2))

Changes in ereftab.lcl (previous version)


Added line 30 (was line 29)
>   modifies internalState;