]>
Commit | Line | Data |
---|---|---|
98ed3b22 | 1 | void mystrncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, int n) |
2 | /*@modifies *s1@*/ /*@requires MaxSet(s1) >= ( MaxRead(s1) + n); @*/ | |
3 | /*@ensures MaxRead(result) >= (MaxRead(s1) + n); @*/; | |
4 | ||
5 | void func(char *str) | |
6 | { | |
7 | char buffer[256]; | |
8 | char *b; | |
9 | ||
10 | b = malloc(256); | |
11 | assert(b != NULL); | |
12 | mystrncat(buffer, str, sizeof(buffer) - 1); | |
13 | mystrncat(b, str, sizeof(buffer) - 1); | |
14 | ||
15 | free (b); | |
16 | return; | |
17 | } | |
18 |