Please confirm the first two command lines. You indicate that flags are switched, but the argument order is identical.
If by filename, you mean the bit-code program to execute, then the difference is order determines who processes the argument. klee ... --max-time 10s ./echo.bc ... -> max-time is an argument to klee klee ... ./echo.bc --max-time 10s ... -> max-time is an argument passed to echo.bc. ________________________________ From: klee-dev-boun...@imperial.ac.uk <klee-dev-boun...@imperial.ac.uk> on behalf of Shaheen Cullen-Baratloo <shah...@gmail.com> Sent: Friday, May 22, 2020 17:47 To: klee-dev@imperial.ac.uk <klee-dev@imperial.ac.uk> Subject: [klee-dev] How to use the max-time flag Hi, I'm trying to run klee on a compiled bytecode version of the coreutils, somewhat replicating the experiment that klee did a while back. I'm having some trouble figuring out how to use the --max-time flag. When I run this command, it takes around 3 minutes, despite the max-time being 10 seconds: klee --optimize --libc=uclibc --posix-runtime --max-time 10s ./echo.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout When I run this command, it takes around 3 seconds. The command is identical, except for the fact that the filename and the --max-time flag are switched. klee --optimize --libc=uclibc --posix-runtime --max-time 10s ./echo.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout Finally, when I run it without the --max-time flag klee --optimize --libc=uclibc --posix-runtime ./echo.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout it takes at least 30 minutes, at which point I gave up and killed it. Clearly, the flag before and after the filename are both doing something, but I'm not sure what. The standard usage for --max-time puts it before the filename according to the documentation. Can anyone help me understand what's happening? Thanks in advance.
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
