[klee-dev] Question about --sym-argv

[李永超]

Hi,
I intended to feed symbolic program arguments to the .bc file using --sym-argvs. The source code is:
#include <stdio.h>
#include <string.h>
int main(int argc, char * argv[]) {
	char buf[10];
	char buf_2[10];
	int i = 1;
	printf("%s", argv[1]);
	if(argv[1][0] == 'l')
		strcpy(buf, argv[1]);
	else
		buf[i] = 'l';
	return 0;
}



My command invoking KLEE is: klee ./src.bc --libc=uclibc -posix-runtime --sym-argv 2.
However, after KLEE finishing the execution, only 1 path is covered and the output of KLEE is:


--libc=uclibc
KLEE: done: total instructions = 33
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1



indicating that argv[1] is actually the argument I exactly used in the command line(--libc=uclibc) rather than symbolic values.


Could anyone point out the cause of my problem?
Thanks,
Yongchao.
-------------- next part --------------
HTML attachment scrubbed and removed