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 <[email protected]> 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 > [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
