4 # define maxEmployeeName ((size_t) 20)
5 # define employeePrintSize (63)
8 # define FORMATEMPLOYEE "%9d %-20s %-6s %-11s %6d.00"
11 # include "employee.lh"
13 /*@-incondefs@*/ /*@-redecl@*/
14 extern bool employee_setName (/*@special@*/ employee *p_e, char /* na */[]) /*@sets p_e->name@*/;
15 /*@=incondefs@*/ /*@=redecl@*/
17 # define employee_initMod() bool_initMod()