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

[高凤娟]

I found the codes that deal with symbolic files in file  "runtime / POSIX/klee_init_env.c" and “ runtime / POSIX / fd_init.c”,
but I don't understand how can klee keep track of  the changes of symbolic files.







At 2014-09-19 15:45:05, "高凤娟" <happygogf at 163.com> wrote:
>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.
-------------- next part --------------
HTML attachment scrubbed and removed