[klee-dev] KLEE "hang" while executing a system call

Sean Bartell sean at yotann.org
Sat Oct 24 08:26:13 BST 2015


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


More information about the klee-dev mailing list