[klee-dev] About -sym-stdout

[Cristian Cadar]

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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>