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. 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. 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? Cheers Chris Hobbs QNX Kernel Development
