[klee-dev] How to distinguish klee's print of different execution paths

樊雨鑫 fanyx at shanghaitech.edu.cn
Wed Sep 1 16:38:16 BST 2021


Hi,
    I am new to Klee, use it to do program analysis. 
    I want some intermediate variables' symbolic expressions. So I use klee_print_expr() and klee_print_range() to make that. 
    But Klee prints all messages together, and no information show whether two messages belong to the same execution path.
    for a very simple example: there are many massages printed but they looks have no difference except for the symbolic expressiones.
```for (int8_t i = 0; i < size; i++) {
        for (int8_t j = 0; j < size; j++) {
            bool omatch = (aarr[i] == barr[j]);
            klee_print_expr("omatch", omatch);
            if ( omatch ) {
                int8_tersection[i] = barr[j];
                break;
            }
        } 
    }
```
    I tried to add random value as an id(by seed srand(time(0)))  at the end of the program, but different paths still may have the same random seeds. 
    How to make it that make messages of klee_print_expr can be classified by their execution paths?  
    
    Waiting for your reply.


More information about the klee-dev mailing list