diff options
author | Alastair Reid <adreid@google.com> | 2020-07-30 17:02:20 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-08-07 19:27:34 +0100 |
commit | 07148eeb5ea4d1c6c51e6aa5a666811ef9f50b90 (patch) | |
tree | bf296395b4bac7f3958aa146ce11a51eef84fbc6 /runtime | |
parent | 088fc21e12c9675161172899be5ef5051f1ae96b (diff) | |
download | klee-07148eeb5ea4d1c6c51e6aa5a666811ef9f50b90.tar.gz |
New intrinsic: klee_is_replay
This instrinsic detects whether the program is being executed symbolically or concretely (i.e., using the libkleeRuntest library). The intended usage (illustrated in the test program) is to allow the test program to display the input values by invoking any libraries it wants to. This is especially valuable if you are constructing complex, structured values and for languages like Rust (or C++) that have rich libraries and print libraries. For example, you might pick a symbolic value N with the assumption "0 <= N < 10" and then pick N symbolic values and write them to an array. The resulting ktest file is a bit hard to understand compared with the output of the standard print function in Rust/C++.
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"); |