[klee-dev] Distinguishing klee from runtest

Alastair Reid adreid at google.com
Thu Jul 30 16:45:59 BST 2020


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
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list