// @(#)$Id: dealloc_int_obj.lh,v 1.7 1998/08/27 22:42:12 leavens Exp $

extern void dealloc_int_obj(int *p) throw();
//@ behavior {
//@   requires isValid(p) /\ allocated(*p, pre);
//@   trashes *p;
//@   ensures ~allocated(*p, post);
//@   ensures redundantly ~allocated(p, post);
//@ }

[Index]

HTML generated using lcpp2html.