[splint.git] / test / manual / exposure.c

# include "employee.h"
 
char *
employee_getName (employee e) 
{ 
  return e->name; 
}

/*@observer@*/ char *
employee_obsName (employee e) 
{ return e->name; }
 
/*@exposed@*/ char *
employee_exposeName (employee e)
{ return e->name; }
 
void 
employee_capName (employee e)
{
  char *name;
  
  name = employee_obsName (e);
  *name = toupper (*name);
}
Commit	Line	Data
77970e15	1	# include "employee.h"
	2
	3	char *
	4	employee_getName (employee e)
	5	{
	6	return e->name;
	7	}
	8
	9	/@observer@/ char *
	10	employee_obsName (employee e)
	11	{ return e->name; }
	12
	13	/@exposed@/ char *
	14	employee_exposeName (employee e)
	15	{ return e->name; }
	16
	17	void
	18	employee_capName (employee e)
	19	{
	20	char *name;
	21
	22	name = employee_obsName (e);
	23	name = toupper (name);
	24	}
	25
	26