functionClause_alloc (functionClauseKind kind) /*@defines result->kind@*/
{
functionClause res = (functionClause) dmalloc (sizeof (*res));
functionClause_alloc (functionClauseKind kind) /*@defines result->kind@*/
{
functionClause res = (functionClause) dmalloc (sizeof (*res));