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
