// @(#)$Id: dec_ref.lh,v 1.7 1997/09/16 02:56:30 leavens Exp $
extern void dec_ref(char *cp, int & ref_count) throw();
//@ behavior {
//@   requires allocated(cp, pre) /\ assigned(ref_count, pre)
//@            /\ ref_count^ >= 1;
//@   modifies ref_count;
//@   trashes *cp;
//@   ensures ref_count' = ref_count^ - 1
//@           /\ (if ref_count' = 0 then trashed(*cp)
//@               else ~trashed(*cp));
//@ }

[Index]

HTML generated using lcpp2html.