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, "高凤娟" <[email protected]> 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.
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
