Hi Sean, Thank you very much. I have just added the option for symbolic files and it works now. Thuan
On Sat, Oct 24, 2015 at 3:26 PM, Sean Bartell <[email protected]> wrote: > Hi, > > Thuan Pham on 2015-10-24: > >> I am implementing a customized search strategy for KLEE and facing a >> strange problem. Although my search strategy can work quite well with some >> subject programs, KLEE "hang" while testing the "paste" utility in >> Coreutils 6.10. Precisely, KLEE still be alive (because it can handle >> Ctrl+C to terminate and finalize the execution), however when I try to >> insert some printf statements at some points, the printf functions do not >> work after KLEE reach the following statement in fd.c. >> >> r = syscall(__NR_read, f->fd, buf, count); //line 372, fd.c >> > > Paste is reading from standard input. By default, KLEE passes the read on > to the operating system. So KLEE didn't hang---it's just waiting for you to > type something. > > If you want standard input to have a concrete value, pipe a file into KLEE: > > klee --libc=uclibc --posix-runtime paste.bc < input-file > > If you want standard input to have symbolic values, use -sym-files: > > klee --libc=uclibc --posix-runtime paste.bc -sym-files 2 32 > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
