Added line 4 (was line 3)
> #include <assert.h>
Replaced line 18 to line 19 with line 18
< typedef /*@only@*/ erc o_erc;
< static o_erc db[numERCS];
---
> static erc db[numERCS];
Replaced line 83 to line 84 with line 82 to line 83
< /*@globals internalState@*/
< /*@modifies s, internalState@*/
---
> /*@globals internalState, stderr@*/
> /*@modifies s, internalState, *stderr@*/
Replaced line 307 with line 306
< printf ("Employees:\n");
---
> check (printf ("Employees:\n") >= 0);
Replaced line 312 with line 311
< printf ("%s", printVal);
---
> check (printf ("%s", printVal) >= 0);
Replaced line 17 with line 17
< db_status db_hire (employee e) db d;
---
> db_status db_hire (employee e) db d; FILE *stderr;
Replaced line 19 with line 19
< modifies d;
---
> modifies d, *stderr^;
Replaced line 32 with line 32
< void db_uncheckedHire (employee e) db d;
---
> void db_uncheckedHire (employee e) db d; FILE *stderr;
Replaced line 37 with line 37
< modifies d;
---
> modifies d, *stderr^;
Replaced line 49 with line 49
< int db_query (db_q q, empset s) db d; internalState;
---
> int db_query (db_q q, empset s) db d; internalState; FILE *stderr;
Replaced line 51 with line 51
< modifies s, internalState;
---
> modifies s, internalState, *stderr^;
Replaced line 57 with line 57
< bool db_promote (int ssNum) db d;
---
> bool db_promote (int ssNum) db d; FILE *stderr;
Replaced line 59 with line 59
< modifies d;
---
> modifies d, *stderr^;
Replaced line 83 with line 83
< void db_print(void) db d; FILE *stdout;
---
> void db_print(void) db d; FILE *stdout; FILE *stderr;
Replaced line 85 with line 85
< modifies *stdout^;
---
> modifies *stdout^, *stderr^;
Replaced line 92 with line 92
< void db_initMod(void) db d; internalState;
---
> void db_initMod(void) db d; internalState; FILE *stderr;
Replaced line 94 with line 94
< modifies d, internalState;
---
> modifies d, internalState, *stderr^;
Replaced line 13 with line 13 to line 14
< /*@globals internalState@*/ /*@modifies internalState@*/
---
> /*@globals internalState, stderr, stdout@*/
> /*@modifies internalState, *stderr, *stdout@*/
Replaced line 31 to line 32 with line 32 to line 33
< printf ("FormatPos: Wrong number of arguments. Given %d needs 0.\n",
< argc - 1);
---
> check (fprintf (stderr, "FormatPos: Wrong number of arguments. "
> "Given %d needs 0.\n", argc - 1) >= 0);
Replaced line 41 with line 42
< printf("Size should be 0.\n");
---
> check (printf("Size should be 0.\n") >= 0);
Replaced line 57 with line 58
< printf("Size should be 500.\n");
---
> check (printf("Size should be 500.\n") >= 0);
Replaced line 73 with line 74
< printf("Size should be 250.\n");
---
> check (printf("Size should be 250.\n") >= 0);
Replaced line 93 with line 94
< printf("Size should be 350.\n");
---
> check (printf("Size should be 350.\n") >= 0);
Replaced line 100 with line 101
< printf("Size should be 350.\n");
---
> check (printf("Size should be 350.\n") >= 0);
Replaced line 103 with line 104
< printf("Print two different employees:\n");
---
> check (printf("Print two different employees:\n") >= 0);
Replaced line 109 with line 110
< printf("%s\n", &(na[0]));
---
> check (printf("%s\n", &(na[0])) >= 0);
Replaced line 151 to line 152 with line 152 to line 154
< printf("Should print true: %s\n",
< bool_unparse (/*@-usedef@*/ status == DBS_DUPLERR /*@=usedef@*/));
---
> check (printf("Should print true: %s\n",
> bool_unparse (/*@-usedef@*/ status == DBS_DUPLERR /*@=usedef@*/))
> >= 0);
Replaced line 154 with line 156
< printf("Employees 0 - 19\n");
---
> check (printf("Employees 0 - 19\n") >= 0);
Replaced line 158 with line 160
< printf("Employees 0 - 16, 18 - 19\n");
---
> check (printf("Employees 0 - 16, 18 - 19\n") >= 0);
Replaced line 164 with line 166
< printf("Should get two females: %d\n%s\n", i, sprintResult);
---
> check (printf("Should get two females: %d\n%s\n", i, sprintResult) >= 0);
Replaced line 174 with line 176 to line 177
< printf("Should get two females and ten males: %d\n%s\n", i, sprintResult);
---
> check (printf("Should get two females and ten males: %d\n%s\n", i, sprintResult)
> >= 0);
Replaced line 180 with line 183
< printf("Should get two females: %d\n%s\n", i, sprintResult);
---
> check (printf("Should get two females: %d\n%s\n", i, sprintResult) >= 0);
Replaced line 184 with line 187
< printf("Should get 18 employees\n");
---
> check (printf("Should get 18 employees\n") >= 0);
Replaced line 1 with line 1
< imports employee;
---
> imports employee, <stdio>;
Replaced line 4 with line 4
< only empset empset_create(void)
---
> only empset empset_create(void) FILE *stderr;
Added line 6 (was line 5)
> modifies *stderr^;
Replaced line 21 with line 22 to line 23
< | bool : void | empset_insert (empset s, employee e) internalState;
---
> | bool : void | empset_insert (empset s, employee e)
> internalState; FILE *stderr;
Replaced line 23 with line 25
< modifies s, internalState;
---
> modifies s, internalState, *stderr^;
Replaced line 27 with line 29
< void empset_insertUnique (empset s, employee e) internalState;
---
> void empset_insertUnique (empset s, employee e) internalState; FILE *stderr;
Replaced line 30 with line 32
< modifies s, internalState;
---
> modifies s, internalState, *stderr^;
Replaced line 40 with line 42 to line 43
< only empset empset_union(empset s1, empset s2) internalState;
---
> only empset empset_union(empset s1, empset s2)
> internalState; FILE *stderr;
Replaced line 42 with line 45
< modifies internalState;
---
> modifies internalState, *stderr^;
Replaced line 46 with line 49 to line 50
< only empset empset_disjointUnion (empset s1, empset s2) internalState;
---
> only empset empset_disjointUnion (empset s1, empset s2)
> internalState; FILE *stderr;
Replaced line 48 with line 52
< modifies internalState;
---
> modifies internalState, *stderr^;
Replaced line 53 with line 57
< void empset_intersect (empset s1, empset s2) internalState;
---
> void empset_intersect (empset s1, empset s2) internalState; FILE *stderr;
Replaced line 55 with line 59
< modifies s1, internalState;
---
> modifies s1, internalState, *stderr^;
Replaced line 80 with line 84
< only char *empset_sprint(empset s)
---
> only char *empset_sprint(empset s) FILE *stderr;
Added line 86 (was line 81)
> modifies *stderr^;
Replaced line 85 with line 90
< void empset_initMod (void) internalState;
---
> void empset_initMod (void) internalState; FILE *stderr;
Replaced line 87 with line 92
< modifies internalState;
---
> modifies internalState, *stderr^;
Replaced line 2 with line 2
<
---
> # include <assert.h>
Replaced line 5 with line 5
< static size_t int_toSize (int x) /*@*/
---
> static size_t int_toSize (int x) /*@globals stderr@*/ /*@modifies *stderr@*/
Replaced line 9 with line 9
< fprintf (stderr, "Error: int_toSize is negative: %d", x);
---
> check (fprintf (stderr, "Error: int_toSize is negative: %d", x) >= 0);
Replaced line 26 with line 26
< printf ("Malloc returned null in erc_create\n");
---
> check (fprintf (stderr, "Malloc returned null in erc_create\n") >= 0);
Replaced line 78 with line 78
< printf ("Malloc returned null in erc_insert\n");
---
> check (fprintf (stderr, "Malloc returned null in erc_insert\n") >= 0);
Replaced line 143 with line 143
< printf ("Malloc returned null in erc_sprint\n");
---
> check (fprintf (stderr, "Malloc returned null in erc_sprint\n") >= 0);
Replaced line 1 with line 1
< imports eref;
---
> imports eref, <stdio>;
Replaced line 5 with line 5
< only erc erc_create(void)
---
> only erc erc_create(void) FILE *stderr;
Added line 7 (was line 6)
> modifies *stderr^;
Replaced line 17 with line 18
< void erc_insert(erc c, eref er)
---
> void erc_insert(erc c, eref er) FILE *stderr;
Replaced line 20 with line 21
< modifies c;
---
> modifies c, *stderr^;
Replaced line 48 with line 49
< void erc_join(erc c1, erc c2)
---
> void erc_join(erc c1, erc c2) FILE *stderr;
Replaced line 51 with line 52
< modifies c1;
---
> modifies c1, *stderr^;
Replaced line 55 with line 56
< only char *erc_sprint(erc c)
---
> only char *erc_sprint(erc c) FILE *stderr;
Added line 58 (was line 56)
> modifies *stderr^;
Replaced line 66 with line 68
< void erc_initMod (void) internalState;
---
> void erc_initMod (void) internalState; FILE *stderr;
Replaced line 68 with line 70
< modifies internalState;
---
> modifies internalState, *stderr^;
Replaced line 36 with line 36
< printf ("Malloc returned null in eref_alloc\n");
---
> check (fprintf (stderr, "Malloc returned null in eref_alloc\n") >= 0);
Replaced line 46 with line 46
< printf ("Malloc returned null in eref_alloc\n");
---
> check (fprintf (stderr, "Malloc returned null in eref_alloc\n") >= 0);
Replaced line 82 with line 82
< printf ("Malloc returned null in eref_initMod\n");
---
> check (fprintf (stderr, "Malloc returned null in eref_initMod\n") >= 0);
Replaced line 90 with line 90
< printf ("Malloc returned null in eref_initMod\n");
---
> check (fprintf (stderr, "Malloc returned null in eref_initMod\n") >= 0);
Replaced line 1 with line 1
< imports employee;
---
> imports employee, <stdio>;
Replaced line 10 with line 10
< eref eref_alloc(void) map m;
---
> eref eref_alloc(void) map m; FILE *stderr;
Replaced line 12 with line 12
< modifies m;
---
> modifies m, *stderr^;
Replaced line 43 with line 43
< void eref_initMod(void) map m; internalState;
---
> void eref_initMod(void) map m; FILE *stderr; internalState;
Replaced line 45 with line 45
< modifies m, internalState;
---
> modifies m, internalState, *stderr^;
Replaced line 5 with line 5
< only ereftab ereftab_create(void)
---
> only ereftab ereftab_create(void) FILE *stderr;
Added line 7 (was line 6)
> modifies *stderr^;
Replaced line 10 with line 11
< void ereftab_insert(ereftab t, employee e, eref er)
---
> void ereftab_insert(ereftab t, employee e, eref er) FILE *stderr;
Replaced line 13 with line 14
< modifies t;
---
> modifies t, *stderr^;
Replaced line 28 with line 29
< void ereftab_initMod (void) internalState;
---
> void ereftab_initMod (void) internalState; FILE *stderr;
Replaced line 30 with line 31
< modifies internalState;
---
> modifies internalState, *stderr^;