Hi Lei,

Here are the symbolic arguments for those eight tools:

dd: --sym-args 0 3 10 --sym-files 1 8 --sym-stdout
dircolors: --sym-args 0 3 10 --sym-files 2 12 --sym-stdout
echo: --sym-args 0 4 300 --sym-files 2 30 --sym-stdout
expr: --sym-args 0 1 10 --sym-args 0 3 2 --sym-stdout
mknod: --sym-args 0 1 10 --sym-args 0 3 2 --sym-files 1 8 --sym-stdout
od: --sym-args 0 3 10 --sym-files 2 12 --sym-stdout
pathchk: --sym-args 0 1 2 --sym-args 0 1 300 --sym-files 1 8 --sym-stdout
printf: --sym-args 0 3 10 --sym-files 2 12 --sym-stdout

Hope this helps,
Cristian

On 14/01/13 18:28, Lei Zhang wrote:
Hi Cristian,

Thank you for your quick reply! :-)

Besides, the paper mentions "For eight tools where the coverage results
of these values were unsatisfactory, we consulted the man page and
increased the number and size of arguments and files." Could you give us
more details about that? Thanks!

Best regards,

On Mon, Jan 14, 2013 at 10:44 AM, Cristian Cadar <[email protected]
<mailto:[email protected]>> wrote:

    Hi Lei,

    Our choice was based on a high-level understanding of the Coreutils
    apps: most behavior can be triggered with no more than 2 short
    options,  1 long option, and 2 small files (one of which is stdin).

    Best wishes,
    Cristian


    On 14/01/13 14:58, Lei Zhang wrote:

        Hi All,

        We are working on a possible way to improve KLEE. So it would be
        nice to
        compare our method's results with the original KLEE's. For a fair
        comparison, we need to understand how the parameters used in your
        OSDI'08 paper were chosen. According to your reply on the KLEE
        mailing
        list
        (http://www.mail-archive.com/[email protected]/__msg00162.html
        <http://www.mail-archive.com/[email protected]/msg00162.html>),
        your OSDI paper uses

        --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 2 8 --sym-stdout

        Could you unveil the rationale/intuition behind these settings, such
        like why 10 and 2 are used as the maximal lengths? Any help is
        highly
        appreciated. Thanks in advance!

        Best regards,

        --
        Lei
        Department of Electrical and Computer Engineering
        University of Waterloo
        200 University Avenue West
        Waterloo, Ontario, Canada N2L 3G1


        _________________________________________________
        klee-dev mailing list
        [email protected] <mailto:[email protected]>
        https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
        <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>


    _________________________________________________
    klee-dev mailing list
    [email protected] <mailto:[email protected]>
    https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
    <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>




--
Lei Zhang
Department of Electrical and Computer Engineering
University of Waterloo
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1

_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to