[klee-dev] Mixed concrete-symbolic execution

[Thuan Pham]

Hi,
I think the question of Riyad Parvez was about concolic execution in KLEE
and S2E. Actually, S2E supports concolic execution by keeping a second
value mapping named concolics along with the symbolics one. In KLEE, to the
best of my knowledge, we need to use its "seed mode" in order to run
program under test in concolic mode. In normal mode, KLEE explore program
symbolically. One reference for understanding the concolic mode in KLEE is
the paper:
"make test-zesti: A Symbolic Execution Solution for Improving Regression
Testing".
Regards,
Thuan

On Wed, Sep 30, 2015 at 12:55 AM, Sean Bartell <sean at yotann.org> wrote:

> Riyad Parvez on 2015-09-23:
>
> I was wondering whether it's possible mixed concrete-symbolic execution in
> KLEE? Like S2E, where some of the input to the program will be symbolic and
> other input will be concrete.
>
> All inputs are concrete by default. You can make certain inputs symbolic
> by either calling klee_make_symbolic from within the program, or by using
> uclibc and the POSIX wrapper and using arguments like -sym-args.
>
> Keep in mind KLEE will run the program very slowly, even for parts of the
> code where there are no symbolic values involved.
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
-------------- next part --------------
HTML attachment scrubbed and removed