1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
void*
memcpy (char* dst, char* src, unsigned n)
{
unsigned i;
char* q;
char* eos;
char* p;
#ifndef NDEBUG
unsigned j, old, new;
assume (j < n);
assume (0 <= j); /* only makes sense if size_t is signed */
old = src[j];
#endif
assume (src <= src + n);
assume (dst <= dst + n);
/* This assumption is dropped if we allow src and dst to overlap.
*/
assume (dst + n <= src || src + n <= dst);
for (p = src, q = dst, eos = src + n; p < eos; p++, q++) *q = *p;
#ifndef NDEBUG
new = dst[j];
assert (old == new);
#endif
return dst;
}
|
