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;