> empset_final (em1);
> empset_final (em2);
> empset_final (em3);
> empset_final (em1); > empset_final (em2); > empset_final (em3);
> assert (prev != NULL);
< return; --- > /*@-compdef@*/ return; /*@=compdef@*/