Changes in bool.h (previous version)

Added line 34 to line 37 (was line 33)

> extern /*@falseexit@*/ void check (bool x);
> # define check(x) \
>   do { bool m_res = x; assert (m_res); } while (FALSE)
>

Changes in dbase.c (previous version)

Deleted line 210 to line 211 (matches line 209)

<   eref er;             
<   employee e;

Changes in drive.c (previous version)

Added line 6 (was line 5)

> # include <assert.h>

Replaced line 123 with line 124

<           hire(e); 
---
>           check (hire(e) == db_OK);

Changes in employee.c (previous version)

Replaced line 7 with line 7

<   int i;
---
>   size_t i;

Changes in employee.lcl (previous version)

Replaced line 1 with line 1 to line 3

< constant int maxEmployeeName;
---
> imports <stdio> ;
> 
> constant size_t maxEmployeeName;

Changes in empset.c (previous version)

Deleted line 28 to line 29 (matches line 27)

<   eref er; 
<

Added line 83 (was line 84)

>   /*@-mods@*/

Added line 86 (was line 86)

>   /*@=mods@*/

Added line 108 (was line 107)

>   /*@-mods@*/

Added line 112 (was line 110)

>   /*@=mods@*/

Deleted line 135 (matches line 136)

<   employee e;

Added line 140 (was line 138)

>   /*@-mods@*/

Added line 144 (was line 141)

>   /*@=mods@*/

Changes in erc.c (previous version)

Added line 4 to line 24 (was line 3)

> static size_t int_toSize (int x)
> {
>   if (x < 0)
>     {
>       fprintf (stderr, "Error: int_toSize is negative: %d", x);
>       return 0;
>     }
>   else
>     {
>       size_t s = (size_t) x;
> 
>       if ((int) s != x)
>         {
>           fprintf (stderr, "Error: int_toSize is inconsistent: %d", x);
>           return 0;
>         }
> 
>       return s;
>     }
> }
>

Replaced line 47 with line 68

<     if (tmpc->val == er) return TRUE; 
---
>     if (eref_equal (tmpc->val, er)) return TRUE;

Replaced line 78 with line 99

<       if (elem->val == er) 
---
>       if (eref_equal (elem->val, er))

Replaced line 141 with line 162

<     malloc (erc_size (c) * (employeePrintSize + 1) + 1);
---
>     malloc (int_toSize (erc_size (c) * (employeePrintSize + 1) + 1));

Added line 172 (was line 150)

>   /*@-mods@*/

Added line 179 (was line 156)

>   /*@=mods@*/

Changes in ereftab.c (previous version)

Added line 34 (was line 33)

>   /*@-mods@*/

Replaced line 37 with line 38 to line 40

<       if (employee_equal (&e, &e1)) return er;
---
>       if (employee_equal (&e, &e1))
>         {
>           erc_iterReturn (it, er);

Added line 42 to line 43 (was line 38)

>     }
>   /*@=mods@*/