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
