Hi, many programs write their output to stdout, and if this output is symbolic, you might want to check that it respects various properties. For instance, we used this option for the crosschecking study between Coreutils and Busybox utilities in the original KLEE paper.

I agree more documentation would be useful.

Best,
Cristian

On 05/05/18 17:37, Xiao Liang Yu wrote:
Hello,

I have realized there is a|-sym-stdout|argument in KLEE. While the documentation says that it will make the|stdout|symbolic, I don’t see how it is useful. Would be great if there are some example use-cases for which|-sym-stdout|is useful.

Thanks!

Xiao Liang YU


_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to