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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
