[klee-dev] How can I get the contents of a symbolic file

[高凤娟]

Hi,
I'm trying to detect whether the function read(int fd,void *buf,int count) has a buffer overflow.
For example:
#define BUFSIZE 10
int main(int argc,char *argv[]){    
char buf[BUFSIZE];
int fd = open(argv[1],O_RDONLY);
unsigned numchars = 0;
ssize_t r = read(fd,buf,BUFSIZE);
unsigned i;
for(i=0;i<r;i++){
if(buf[i]!='\0'){
    numchars++;
}
}
close(fd);
printf("numchars:%d\n",numchars);
printf("%s\n", buf);
return 0;
}
I invoked klee with --libc=uclibc --posix-runtime src.o --sym-arg 1 --sym-files 1 32.
How can I  show every character of the symbolic file with klee's symbolic expression?
Thank you very much.
Rachel Gao.