[klee-dev] Logging the Symbolic Values of Variables

[Luke Dramko]

Hello,

My research group is looking to output the value of each variable's
symbolic representation after the execution of each line in the source
program. Alternatively, the symbolic values of only the variables whose
values are modified on that line would be sufficient as well.

For example, given the following function is being executed symbolically:

1. int fn(int x) {
2.     if (x > 1) {
3.         x++;
4.         x = x * x;
5.     }
6.     return x;
7. }

We would like to know that
- after line 2 (on the true branch) that x is constrained by x > 1.
- after line 3, that x is constrained by x > 2.
- after line 4, that x is constrained by x = y * 2 where y > 2.
etc.

(The above ignores overflow semantics but constraints that capture them
would be welcome.)

Is there a way to do this with Klee? If not, what part of the codebase
should we modify to add this capability?

Thank you for your help!

Best regards,
Luke
-------------- next part --------------
HTML attachment scrubbed and removed