diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2017-07-22 23:09:44 +0100 |
---|---|---|
committer | Dan Liew <delcypher@gmail.com> | 2017-07-24 21:41:09 +0100 |
commit | c06cc05adc7eac45ff16d7e488576d479811d7a8 (patch) | |
tree | 08e836bf6cec4d0661b5e3edd7da7072c847f7bf /runtime/klee-libc | |
parent | 6b94e7721e12cf5d99722278adf2ba9c0bbde995 (diff) | |
download | klee-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.c | 20 |
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; -} |