Thanks Cristian, So, you mean that by default, the -std-out option does nothing useful and it will be useful only when property checks are added via modifying KLEE?
Thanks! Xiao Liang YU On Wed, May 9, 2018 at 7:30 PM, Cristian Cadar <[email protected]> wrote: > 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 >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> >> > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
