Hi,
KLEE does not provide this information, although you could add such
metadata when adding a new constraint. However, because constraint
solving optimisations could combine constraints, obtaining the origin of
a constraint might not be possible in the general case.
Best,
Cristian
On 25/01/2024 04:07, Bohan wrote:
收件人:[email protected] <mailto:[email protected]>
周三 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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
