[klee-dev] Mapping Path Constraint to the Actual Path in Source Code

[Bohan]

收件人:klee-dev at 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!
-------------- next part --------------
HTML attachment scrubbed and removed