Hello all, I am performing static analysis on a codebase and for that I am trying to find all the possible paths from function 'A' to function 'B' along with the conditions that are responsible while traversing that path. My input is a large llvm IR file which contains all the functions definitions.

So if we consider the below toy example :- int functionA(int a) { if (a > 0) { return functionB(20, 50); } else { return functionC(100, 500); } } int functionB(int x, int y) { if(x > y){ return multiply(x, y); } else { return divide(y, x); } } int functionC(int x, int y) { if(y > 0){ return divide(x, y); } else { return multiply(y, x); } } int multiply(int a, int b){ return a*b; } int divide(int x, int y){ return x/y; } 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)" or it can be combined as "functionA && ((x < y) || (y > 0)) && divide" I just want to know whether klee is capable of performing such analysis (not exact as I knew I need to modify few things to arrive at the final solution but you get the gist). If yes, can you please provide some references and resources that I can look into. Thank you.

_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev