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
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
