On 2023-07-25 at 18:50+05:30, Sailesh Sai Teja wrote: > So lets say I want to trace the execution path from function > "functionA" to function "divide", the following is the output > I am expecting > > 1. "functionA && ((x < y) && divide)" > 2. "functionA && ((y > 0) && divide)"
Since no one gave any suggestion, you can try the following (very cursed) idea if instrumenting each function with something like bool __trace_tmp; klee_make_symbolic(&__trace_tmp, 1, "function!name"); klee_assert(__trace_tmp); and then analyse the path conditions. Alternatively, in Executor::executeInstruction for Instruction::Call, you can get the function name and manually log it as well as handling the ordering of call trace and path conditions, e.g. x < y. _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
