# include "setname.h"

void setName (employee e)
 /*@modifies e->name@*/
{
  strcpy (e->name, "");
}


syntax highlighted by Code2HTML, v. 0.9.1