[klee-dev] question about symbolic fs

[Alvin Cheung]

Hello,

I am trying to use the klee symbolic file system to explore all paths in a 
simple program:

char buf[10];
FILE * file = fopen(argv[1], "r");

if (file != NULL) {
   fread(buf, sizeof(char), 1, file);
   if (buf[0] == 'a') printf("path 0\n");
   else printf("path 1\n");
}
else printf("path 2\n");

I invoked klee with --libc=uclibc --posix-runtime --init-env prog.bc --sym-arg 
1 
and it explored 3 paths: path 1, and path 2 for 2 times.  I am wondering why 
path 0 is not explored in this case?  I thought buf would be symbolic given 
that 
it was read from a symbolic file?

Thanks,
Alvin