Hi Alastair,
Unless I'm misremembering things, we've never added anything like this,
but this is the right approach, and I'd be happy to accept such a PR. I
think the right way to do this would be to have this as an intrinsic
defined in both runtime/Intrinsic and runtime/Runtest.
Best,
Cristian
On 30/07/2020 16:45, Alastair Reid wrote:
Is there a function that I can use in a program to distinguish between
running under KLEE and replaying a ktest using libkleeRuntest?
The reason that I want this is so that my test harness can print
symbolic values when replaying with concrete values but does not do so
when running under KLEE.
This is especially useful when generating structured symbolic values.
In particular, when using KLEE with Rust, it is much, much better to use
the std::fmt::Debug api to print structure values like Vectors,
BinaryHeaps, BTreeMap, etc. than to run ktest-tool to see the raw
symbolic values that were used to construct the object.
If there is not a standard way of doing this, I propose to submit a PR
that adds the following function to klee.h (with two alternative
implementations).
int klee_is_replay();
// return 1 if replaying under libkleeRuntest
// return 0 if executing symbolically under KLEE
Suggestions for different name, etc. welcome.
--
Alastair
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
