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

[Cristian Cadar]

Hi, you would need to modify the code associated with those klee_ 
intrinsics to also output state information (see 
https://github.com/klee/klee/blob/master/lib/Core/SpecialFunctionHandler.cpp).

Best,
Cristian

On 01/09/2021 16:38, 樊雨鑫 wrote:
> 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.
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>