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
34
35
36
37
38
39
40
41
42
43
44
|
// validate mempcpy implementation
// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --libc=klee --exit-on-error %t.bc
#include "klee/klee.h"
// do not #define _GNU_SOURCE - just declare mempcpy for all systems
#include <assert.h>
#include <string.h>
void *mempcpy(void *destaddr, void const *srcaddr, size_t len);
int main() {
// char arrays
char s1[] = "foofoo";
char s2[] = "barbar";
char *spos = (char *)mempcpy(s2, s1, 3);
assert(spos == &s2[3]);
assert(!strcmp(s2, "foobar"));
assert(!strcmp(s1, "foofoo"));
// int arrays
int arr1[] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
int arr2[] = {-1, -1, -1, -1, -1, -1, -1, -1, -1, -1};
int *pos = (int *)mempcpy(arr2, arr1, sizeof(int) * 5);
assert(pos == &arr2[5]);
for (int i = 0; i < 10; ++i) assert(arr1[i] == i);
for (int i = 0; i < 5; ++i) assert(arr2[i] == i);
for (int i = 5; i < 10; ++i) assert(arr2[i] == -1);
// symbolic int arrays
int sarr1[10];
int sarr2[10];
klee_make_symbolic(sarr1, sizeof(int) * 10, "sarr1");
klee_make_symbolic(sarr2, sizeof(int) * 10, "sarr2");
pos = (int *)mempcpy(sarr2, sarr1, sizeof(int) * 5);
assert(pos == &sarr2[5]);
assert(!memcmp(sarr2, sarr1, sizeof(int) * 5));
}
|
