// @(#) $Id: poorly_encrypt.lh,v 1.11 1998/08/27 22:56:51 leavens Exp $
extern void poorly_encrypt(unsigned char *s) throw();
//@ behavior {
//@   uses cpp_unsignedChar_string;
//@   requires nullTerminated(s, pre);
//@   modifies objectsToNull(s, pre);
//@   ensures \A i: int (legalStringIndex(s,pre,i)
//@                        => (*(s + i))' = (*(s + i))^ + 1);
//@   ensures redundantly (legalStringIndex(s,pre,0) /\ (*s)^ = UCHAR_MAX)
//@                       => ((*s)' = 0);
//@ }

[Index]

HTML generated using lcpp2html.