[klee-dev] About -sym-stdout

[Xiao Liang Yu]

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 <c.cadar at imperial.ac.uk>
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
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed