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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
