From ef90f1e219fec27a3d594158ae5f380a9e9a2f37 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Tue, 15 May 2018 15:12:12 +0100 Subject: 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. --- test/Runtime/FreeStanding/freestanding_only.c | 33 +++++++++++++++++++++++++++ test/Runtime/POSIX/Replay.c | 1 + 2 files changed, 34 insertions(+) create mode 100644 test/Runtime/FreeStanding/freestanding_only.c (limited to 'test') 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 +#include +#include + +#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 #define EXIT exit #endif -- cgit 1.4.1