收件人:klee-dev@imperial.ac.uk
周三 2024/1/24 19:18
Hi,
I am new to Klee. I have a question about how to determine which path
constraints generated in the KQuery file correspond to specific paths or
lines of code in the original source code or in the IR?
For example; I have a dummy c code that have 3 path,
#include <klee/klee.h>
#include <stdio.h>
int main() {
int num;
int a = 10;
// Make 'num' a symbolic variable
klee_make_symbolic(&num, sizeof(num), "num");
if (num > a + 3) {
printf("branch 0.\n");
} else if (num < a) {
printf("branch 1.\n");
} else {
printf("branch 2.\n");
}
return 0;
}
And here is the Kquery file for a ktest file where the num = 2147483647,
and it goes to branch 0.
array num[4] : w32 -> w8 = symbolic
(query [(Slt 13
(ReadLSB w32 0 num))]
false)
My question is there any info from Klee that tells this query is for the
branch 0.
Thank you very much for help!
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
