From c06cc05adc7eac45ff16d7e488576d479811d7a8 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <c.cadar@imperial.ac.uk>
Date: Sat, 22 Jul 2017 23:09:44 +0100
Subject: Moved klee_choose from klee-libc to KLEE intrinsics.

---
 runtime/Intrinsic/klee_choose.c                      | 20 ++++++++++++++++++++
 runtime/klee-libc/klee-choose.c                      | 20 --------------------
 .../libkleeruntest/replay_invalid_klee_choose.c      |  2 +-
 3 files changed, 21 insertions(+), 21 deletions(-)
 create mode 100644 runtime/Intrinsic/klee_choose.c
 delete mode 100644 runtime/klee-libc/klee-choose.c

diff --git a/runtime/Intrinsic/klee_choose.c b/runtime/Intrinsic/klee_choose.c
new file mode 100644
index 00000000..44e5cea2
--- /dev/null
+++ b/runtime/Intrinsic/klee_choose.c
@@ -0,0 +1,20 @@
+/*===-- klee-choose.c -----------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===*/
+
+#include "klee/klee.h"
+
+uintptr_t klee_choose(uintptr_t n) {
+  uintptr_t x;
+  klee_make_symbolic(&x, sizeof x, "klee_choose");
+
+  /* NB: this will *not* work if they don't compare to n values. */
+  if(x >= n)
+    klee_silent_exit(0);
+  return x;
+}
diff --git a/runtime/klee-libc/klee-choose.c b/runtime/klee-libc/klee-choose.c
deleted file mode 100644
index 44e5cea2..00000000
--- a/runtime/klee-libc/klee-choose.c
+++ /dev/null
@@ -1,20 +0,0 @@
-/*===-- klee-choose.c -----------------------------------------------------===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===*/
-
-#include "klee/klee.h"
-
-uintptr_t klee_choose(uintptr_t n) {
-  uintptr_t x;
-  klee_make_symbolic(&x, sizeof x, "klee_choose");
-
-  /* NB: this will *not* work if they don't compare to n values. */
-  if(x >= n)
-    klee_silent_exit(0);
-  return x;
-}
diff --git a/test/Replay/libkleeruntest/replay_invalid_klee_choose.c b/test/Replay/libkleeruntest/replay_invalid_klee_choose.c
index 62cdcec3..c64f913d 100644
--- a/test/Replay/libkleeruntest/replay_invalid_klee_choose.c
+++ b/test/Replay/libkleeruntest/replay_invalid_klee_choose.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc -DBOUND_VALUE=32 -DFORCE_VALUE=20 %s -emit-llvm -g -O0 -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --libc=klee --search=dfs %t.bc
+// RUN: %klee --output-dir=%t.klee-out --search=dfs %t.bc
 // RUN: test -f %t.klee-out/test000001.ktest
 // RUN: test ! -f %t.klee-out/test000002.ktest
 
-- 
cgit 1.4.1