[splint.git] / test / db3 / employee.h

# ifndef EMPLOYEE_H
# define EMPLOYEE_H

# define maxEmployeeName   ((size_t) 20)
# define employeePrintSize (63)

/*@notfunction@*/
# define FORMATEMPLOYEE "%9d  %-20s  %-6s  %-11s  %6d.00"


# include "employee.lh"

/*@-incondefs@*/ /*@-redecl@*/
extern bool employee_setName (/*@special@*/ employee *p_e, char  /* na */[]) /*@sets p_e->name@*/;
/*@=incondefs@*/ /*@=redecl@*/

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