about summary refs log tree commit diff homepage
path: root/runtime/klee-libc
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2017-07-22 23:09:44 +0100
committerDan Liew <delcypher@gmail.com>2017-07-24 21:41:09 +0100
commitc06cc05adc7eac45ff16d7e488576d479811d7a8 (patch)
tree08e836bf6cec4d0661b5e3edd7da7072c847f7bf /runtime/klee-libc
parent6b94e7721e12cf5d99722278adf2ba9c0bbde995 (diff)
downloadklee-c06cc05adc7eac45ff16d7e488576d479811d7a8.tar.gz
Moved klee_choose from klee-libc to KLEE intrinsics.
Diffstat (limited to 'runtime/klee-libc')
-rw-r--r--runtime/klee-libc/klee-choose.c20
1 files changed, 0 insertions, 20 deletions
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;
-}