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
