// @(#)$Id: strcpy.lh,v 1.12 1997/06/03 20:30:21 leavens Exp $
extern char* strcpy(char *s1, const char *s2) throw();
//@ behavior {
//@   uses cpp_char_string, cpp_const_char_string;
//@   requires nullTerminated(s2, pre)
//@            /\ allocatedUpTo(s1, lengthToNull(s2, pre) + 1, pre);
//@   modifies objectsInRange(s1, 0, lengthToNull(s2, pre));
//@   ensures result = s1 /\ nullTerminated(s1,post)
//@           /\ sameCharsThroughNull(s1, post, s2, pre);
//@ }

[Index]

HTML generated using lcpp2html.