diff options
author | Martin Nowack <martin.nowack@gmail.com> | 2018-05-15 15:12:12 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-07-04 15:13:02 +0100 |
commit | ef90f1e219fec27a3d594158ae5f380a9e9a2f37 (patch) | |
tree | 0a02b5da762b4bc59f7f6bd2453a2a6591f00062 /test/Runtime/FreeStanding | |
parent | 6803c37be83f0c97c95870a18cb230e135a131c9 (diff) | |
download | klee-ef90f1e219fec27a3d594158ae5f380a9e9a2f37.tar.gz |
Reorder linking and optimizations
Link intrinsic library before executing optimizations. This makes sure that any optimization run by KLEE on the module is executed for the intrinsic library as well. Support .ll files as input for KLEE as well.
Diffstat (limited to 'test/Runtime/FreeStanding')
-rw-r--r-- | test/Runtime/FreeStanding/freestanding_only.c | 33 |
1 files changed, 33 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; +} |