// @(#) $Id: set_to_one.lh,v 1.10 1998/08/27 22:56:52 leavens Exp $
extern void set_to_one(int *p) throw();
//@ behavior {
//@   requires allocated(p, pre);
//@   modifies *p;
//@   ensures assigned(p, post) /\ (*p)' = 1;
//@   ensures redundantly assigned(*p, post);
//@ }

[Index]

HTML generated using lcpp2html.