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

/* Output from Splint 3.0.0.20 */

# include <stdio.h>
# include "bool.h"


# ifndef EXPOSED_TYPE_gender
typedef enum {MALE, FEMALE, GENDER_UNKNOWN} gender;
# endif


# ifndef EXPOSED_TYPE_job
typedef enum {MGR, NONMGR, JOB_UNKNOWN} job;
# endif


# ifndef EXPOSED_TYPE_employee
typedef struct {
    int ssNum;
    char name[maxEmployeeName];
    int salary;
    gender gen;
    job j;
    } employee;
# endif

extern void employee_sprint (/*@out@*/ char  /* s */[], employee  /* e */);
extern bool employee_equal (employee * /* e1 */, employee * /* e2 */);
extern bool employee_setName (employee * /* e */, /*@unique@*/ char  /* na */[]);
extern void employee_initMod (void);
Commit	Line	Data
11db3170	1	/* Output from Splint 3.0.0.20 */
885824d3	2
	3	# include <stdio.h>
	4	# include "bool.h"
	5
	6
	7	# ifndef EXPOSED_TYPE_gender
	8	typedef enum {MALE, FEMALE, GENDER_UNKNOWN} gender;
	9	# endif
	10
	11
	12	# ifndef EXPOSED_TYPE_job
	13	typedef enum {MGR, NONMGR, JOB_UNKNOWN} job;
	14	# endif
	15
	16
	17	# ifndef EXPOSED_TYPE_employee
	18	typedef struct {
	19	int ssNum;
	20	char name[maxEmployeeName];
	21	int salary;
	22	gender gen;
	23	job j;
	24	} employee;
	25	# endif
	26
	27	extern void employee_sprint (/@out@/ char /* s /[], employee / e */);
	28	extern bool employee_equal (employee * /* e1 /, employee /* e2 */);
	29	extern bool employee_setName (employee * /* e /, /@unique@/ char / na */[]);
	30	extern void employee_initMod (void);