[klee-dev] symbolic arguments

[Yu Qiang]

Hello,

I'am  running klee on the follwing program:

int t6( int argc, char* argv[])
{
if(argc < 2)
{
printf("argc<2\r\n");
return;
}

printf("argc>=2(%d)\r\n", argc);

char* arg1 = argv[1];
if(arg1[0]=='v')
printf("arg1[0]==v\r\n");
else
printf("arg1[0]!=v(%s)\r\n",arg1);

return 1;
}
int main( int argc, char* argv[])
{
t6( argc, argv);
return 1;
}

using this command:
klee -search=nurs:md2u -allow-external-sym-calls -libc=uclibc
-posix-runtime a.out.bc -sym-argvs 1 2 2

i expected 3 path will be explored:
1: argv<2
2: argv>=2, arg1[0]==v
3: argv>=2, arg1[0]!=v

but only 1 path is explored:
1: argv>=2, arg1[0]!=v.

it seems that "-sym-argvs 1 2 2" are real parameters, not symbolic
parameters!
Any ideas on where i'm going wrong?

My klee version:
test at test-virtual-machine:~/klee/examples/test$ klee -version
Low Level Virtual Machine (http://llvm.org/):
  llvm version 2.9
  Optimized build with assertions.
  Built Jan  6 2015 (03:45:15).
  Host: x86_64-unknown-linux-gnu
  Host CPU: i686

  Registered Targets:
    x86    - 32-bit X86: Pentium-Pro and above
    x86-64 - 64-bit X86: EM64T and AMD64


Thanks.

jgj212
-------------- next part --------------
HTML attachment scrubbed and removed