]>
Commit | Line | Data |
---|---|---|
41320549 | 1 | extern /*@null@*/ /*@out@*/ /*@only@*/ void *mymalloc (size_t size) /*@*/ |
d9a28762 | 2 | /*@ensures MaxSet(result) == (size - 1) @*/ ; |
41320549 | 3 | |
4 | void t() | |
5 | { | |
6 | char *f; | |
7 | ||
8 | f = mymalloc (3); | |
9 | f[2] = '2'; | |
10 | free (f); | |
11 | } |