test/db3/employee.h

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