KLEE doesn't do any concretization is this case. My experience with
this suggests that the main challenge is to choose a general strategy
for the bytes to concretize and the number/kind of iterations to
perform. While I can't seem to find the code in question, adding
another Solver pass of this type is relatively easy. KLEE already
concretizes values in various cases (calls to external functions,
floating-point code), so all the needed basic blocks are there.
Best,
Cristian
On 19/11/13 01:37, Sandeep wrote:
Hello All,
I am aware of the query optimizations strategies that KLEE follows to
simplify the expressions before they each STP.
But what if even after applying these, the query is still complex. Will
KLEE simply give up by time out or it will try something like
concertizing some of the values of the complex constraint to make that
simpler (and thereby give up on exploring some of the paths).
Thanks in advance.
--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
_______________________________________________
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
