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

Reply via email to