// @(#)$Id: done_with.lh,v 1.5 1997/06/03 20:30:02 leavens Exp $ extern void done_with(int & ir) throw(); //@ behavior { //@ trashes ir; //@ ensures trashed(ir); //@ }
[Index]
HTML generated using lcpp2html.