// @(#)$Id: annotations.lh,v 1.3 1997/06/03 20:29:57 leavens Exp $
int returns7() throw();
//@ behavior {  // this is the behavior of returns7
//@   ensures result = 7;    /* a gratituous comment */
//@ }

[Index]

HTML generated using lcpp2html.