// @(#)$Id: decr_ptr.lh,v 1.2 1998/08/27 21:53:51 leavens Exp $
extern void decr_ptr(int *p);
//@ behavior {
//@   requires assigned(p, pre) /\ (*p)^ > 0;
//@   requires redundantly notNull(p);
//@   modifies *p;
//@   ensures returns /\ (*p)' = (*p)^ - 1;
//@ }

[Index]

HTML generated using lcpp2html.