Hi Chris, On Fri, Jun 25, 2010 at 11:52 AM, Chris Hobbs <chobbs at qnx.com> wrote: > In the documentation and literature, there seems to be some confusion > about the -sym-args (or --sym-args) argument to -init-env. > > "klee ... -init-env ... --help" > > gives > > -sym-args <MIN> <MAX> <N> - Replace by at least MIN arguments and at > most MAX arguments, each with maximum length N > > The Cadar, Dunbar, Engler paper says that "--sym-args 1 10 10" means use > zero to three command line arguments, the first 1 character and the > other two 10 characters long. > > In any case, it is not clear whether argv[0] (the program name) is to be > counted or not.
No, argv[0] is not counted. The way sym-args works is to add some number symbolic arguments to the argument vector, you can have multiple instances. So: '--sym-args 1 1 10" will add one arg, '--sym-args 1 1 10 --sym-args 1 1 10' would add two (as would '--sym-args 2 2 10'), and '--sym-args 1 2 10' would add one or two. > > Question 1 > ========== > > If I have a program that takes exactly two runtime parameters > > ./doit first second > > then do I specify "-sym-args 2 2 10" or -sym-args 3 3 10" or even > "--sym-args 10 10 10" or "--sym-args 10 10"? > > I have done various experiments printing argc and it appears that > "-sym-args 2 2 10" is correct. However, that leads to question 2. Yes, '--sym-args 2 2 10' is correct. If you don't want a variable number of arguments, you can also use '--sym-arg 10 --sym-arg 10'. > Question 2 > ========== > > When I run klee on one of my programs with "-sym-args 2 2 5" I get the > following error reported by klee-replay: > > $ klee-replay --create-files-only klee-last/test000070.ktest > make_symbolic mismatch, different sizes: 6 in input file, 4 in code > > With "-sym-args 2 3 5" exactly the same klee-reply command seems to work > (certainly it creates a file). > > Is this a bug that I should drop into Bugzilla or is it my lack of > understanding? This seems like a bug, I would need to see a test case. - Daniel > > Cheers > > Chris Hobbs > QNX Kernel Development > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >
