[klee-dev] how to use concrete value to replace symbolic value when solving failed

[Kuchta, Tomasz]

Hi,

When you say failed, do you mean that the branch was not feasible?
If that is the case, it means that there are no such values in the program input that would make the program execute certain path.
Or do you want to just replace symbolic data with concrete values?
If that is the case, one way to do it is to modify the Executor::executeMemoryOperation function in such a way that whenever you 
are about to read or write symbolic value, you replace it with a concrete one, so that in doesn’t further propagate into the program.

Hope that helps,
Tomek


> On 19 May 2015, at 16:48, Qixue Xiao <s2exqx at gmail.com> wrote:
> 
> hi,
> 
> when constraints are solved failed during symbolic execution, I want
> to use concrete value (like seeds) to replace the related symbolic
> value. So that the execution could continue.
> 
> How could I use this feature in KLEE ?
> 
> thanks.
> 
> xqx
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: winmail.dat
Type: application/ms-tnef
Size: 4455 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150520/f525eb6b/attachment.bin>