[klee-dev] Klee See Mode Concretization

[Ridwan Shariffdeen]

Hi,

I am running Klee in seed mode using a generated ktest file, in order to
capture the symbolic expression for the path given by the ktest file.
However in trying to execute klee, when it comes to external calls it needs
to pass concretized values instead of the symbolic value. From my
understanding, currently, Klee tries to compute a concrete value for the
symbolic variable from the path constraints and pass to the external
function.

Since I am using seed mode with pre-defined values, I need to change the
way Klee concretize the symbolic value by using the current value given in
the ktest file, instead of resolving through path constraints. But, I have
no idea how to achieve this.

Is there a reference I can look into or is this achievable?
Any help in this regard would be much appreciated.

Thanks
Regards
-------------- next part --------------
HTML attachment scrubbed and removed