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

# include "setname.h"

void setName (employee e)
 /*@modifies e->name@*/
{
  strcpy (e->name, "");
}
Commit	Line	Data
77970e15	1	# include "setname.h"
	2
	3	void setName (employee e)
	4	/@modifies e->name@/
	5	{
	6	strcpy (e->name, "");
	7	}