[klee-dev] Dummy pthread library?

2020-07-30 Thread Alastair Reid
Is there a dummy pthread library that I can use with single-threaded programs that only use a single thread but are linked against thread-safe libraries (i.e., threads that call pthread_* functions). I am 99.9% sure that I don't need any actual thread support - just an implementation that

[klee-dev] Distinguishing klee from runtest

2020-07-30 Thread Alastair Reid
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.

Re: [klee-dev] Dummy pthread library?

2020-07-30 Thread Cristian Cadar
Hi again Alastair, I'm not aware of anything like this, but it would be a nice extension of KLEE's POSIX environment. Best, Cristian On 30/07/2020 17:37, Alastair Reid wrote: Is there a dummy pthread library that I can use with single-threaded programs that only use a single thread but are

Re: [klee-dev] Distinguishing klee from runtest

2020-07-30 Thread 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,

Re: [klee-dev] Checking Tool Equivalence

2020-07-30 Thread Cristian Cadar
Hi Linda, I cannot find that infrastructure anymore, but as explained in the paper, the idea was to rename global symbols and link the two tools together, accompanied by a new main function that looks similar in spirit to the one in Figure 11. The only tricky part is to capture and compare