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

[Thuan Pham]

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 <sean at yotann.org> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed