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