about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
authorMartin Nowack <martin.nowack@gmail.com>2018-05-15 15:12:12 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2018-07-04 15:13:02 +0100
commitef90f1e219fec27a3d594158ae5f380a9e9a2f37 (patch)
tree0a02b5da762b4bc59f7f6bd2453a2a6591f00062 /test
parent6803c37be83f0c97c95870a18cb230e135a131c9 (diff)
downloadklee-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')
-rw-r--r--test/Runtime/FreeStanding/freestanding_only.c33
-rw-r--r--test/Runtime/POSIX/Replay.c1
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