diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/Runtime/FreeStanding/freestanding_only.c | 33 | ||||
-rw-r--r-- | test/Runtime/POSIX/Replay.c | 1 |
2 files changed, 34 insertions, 0 deletions
diff --git a/test/Runtime/FreeStanding/freestanding_only.c b/test/Runtime/FreeStanding/freestanding_only.c new file mode 100644 index 00000000..7bdf6c97 --- /dev/null +++ b/test/Runtime/FreeStanding/freestanding_only.c @@ -0,0 +1,33 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -g -c -D_FORTIFY_SOURCE=0 -o %t2.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t2.bc 2> %t.log +// RUN: FileCheck %s --input-file=%t.log +// RUN: rm -rf %t.klee-out +// RUN: %klee --optimize --output-dir=%t.klee-out %t2.bc 2> %t.log +// RUN: FileCheck %s --input-file=%t.log + +#include <assert.h> +#include <stdlib.h> +#include <string.h> + +#define LENGTH 5 +int main(int argc, char **argv) { + char *src = (char *)malloc(LENGTH); + char *dst = (char *)malloc(LENGTH); + + memset(src, 42, LENGTH); + // CHECK-NOT: calling external: memset + + memcpy(dst, src, LENGTH); + // CHECK-NOT: calling external: memcpy + + memmove(dst, src, LENGTH); + // CHECK-NOT: calling external: memmove + + assert(memcmp(src, dst, LENGTH) == 0); + // CHECK-NOT: calling external: memcmp + + assert(*src == 42); + assert(*src == *dst); + return 0; +} diff --git a/test/Runtime/POSIX/Replay.c b/test/Runtime/POSIX/Replay.c index ba11f05f..2b166e1f 100644 --- a/test/Runtime/POSIX/Replay.c +++ b/test/Runtime/POSIX/Replay.c @@ -13,6 +13,7 @@ #ifdef KLEE_EXECUTION #define EXIT klee_silent_exit #else +#include <stdlib.h> #define EXIT exit #endif |