[klee-dev] Distinguishing klee from runtest

[Cristian Cadar]

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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>