[klee-dev] Mixed concrete-symbolic execution

[Sean Bartell]

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.
-------------- next part --------------
HTML attachment scrubbed and removed