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 _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
