diff options
Diffstat (limited to 'runtime')
-rw-r--r-- | runtime/Intrinsic/klee_is_replay.c | 15 | ||||
-rw-r--r-- | runtime/Runtest/intrinsics.c | 4 |
2 files changed, 19 insertions, 0 deletions
diff --git a/runtime/Intrinsic/klee_is_replay.c b/runtime/Intrinsic/klee_is_replay.c new file mode 100644 index 00000000..ac9e541d --- /dev/null +++ b/runtime/Intrinsic/klee_is_replay.c @@ -0,0 +1,15 @@ + +/*===-- klee_is_replay.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" + +unsigned klee_is_replay() { + return 0; +} diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c index cdc8c9d6..f82bd554 100644 --- a/runtime/Runtest/intrinsics.c +++ b/runtime/Runtest/intrinsics.c @@ -146,6 +146,10 @@ uintptr_t klee_choose(uintptr_t n) { return x; } +unsigned klee_is_replay() { + return 1; +} + void klee_assume(uintptr_t x) { if (!x) { report_internal_error("invalid klee_assume"); |