[klee-dev] All possible paths from source to destination function.

Nguyễn Gia Phong cnx at loang.net
Thu Aug 10 05:12:21 BST 2023


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.



More information about the klee-dev mailing list