]>
Commit | Line | Data |
---|---|---|
ed3a6c22 | 1 | //#include "/home/drl7x/re/LCLintDev/lib/ansi.h" |
2 | ||
3 | static char f [12]; | |
4 | extern void /*@alt char * @*/ | |
5 | mstrcpy (/*@unique@*/ /*@out@*/ /*returned*/ char *s1, char *s2) | |
d9a28762 | 6 | /*@modifies *s1@*/ /*@requires MaxSet(s1) >= MaxRead(s2); @*/; |
ed3a6c22 | 7 | |
8 | ||
d9a28762 | 9 | void copyf (char * c) /*@requires MaxSet(c) >= MaxRead(f); @*/ |
ed3a6c22 | 10 | { |
11 | mstrcpy (c, f); | |
12 | } |