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

[Cristian Cadar]

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:
> 
> 收件人:klee-dev at imperial.ac.uk <mailto: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!
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev