[klee-dev] Klee and Kleaver interface

[Anitha B Gollamudi]

Hi,

I am debugging klee to understand the control flow of constraint
generation and solving there of. I have 2-3 basic questions which can
help me cut short the debugging time.

1. So I created a debug build of klee using
--with-runtime=Debug+Asserts. I expected the entire debug build of
KLEE to be in Debug+Asserts. But looks like my debug+Asserts has only
lib directory. Timestamps suggest that klee is still built in
Release+Asserts directory. Why?

2. As I single step, I figured that functions in Executor.cpp try to
execute/interpret each instruction. What is the effective place to put
a breakpoint to understand the control flow to kleaver? (I am
expecting some functions in lib/Solver to get invoked)

3. Will the process of debugging differ if I am using metaSMT? (I am
indeed using --use-metasmt=Z3)


Thanks

-- 
 Anitha