Hi Jiaqi,

I believe the problem here is that our POSIX model doesn't support
pipe() yet. Note that the execution is never forking, for example.

 - Daniel

On Wed, Mar 17, 2010 at 11:23 PM, Jiaqi Tan <tanjiaqi at gmail.com> wrote:
> Hi,
>
> I'm trying to run KLEE on GNU tar, but I keep running into this error
> with symbolic file input. This problem occurs regardless of the size
> of the symbolic input files.
>
> Attached is my call to KLEE, and the output from KLEE:
>
> $ time klee -libc=uclibc -posix-runtime -init-env ./a.out.bc -x -j
> --sym-files 1 100
> KLEE: NOTE: Using model:
> /home/jiaqi/llvm/build/klee-src/klee/Release/lib/libkleeRuntimePOSIX.bca
> KLEE: output directory = "klee-out-45"
> WARNING: this target does not support the llvm.stacksave intrinsic.
> KLEE: WARNING: undefined reference to function: __xstat64
> KLEE: WARNING: undefined reference to function: creat64
> KLEE: WARNING: undefined reference to function: fdopendir
> KLEE: WARNING: undefined reference to function: fstatat64
> KLEE: WARNING: undefined reference to function: futimesat
> KLEE: WARNING: undefined reference to function: openat64
> KLEE: WARNING: undefined reference to variable: program_invocation_name
> KLEE: WARNING: undefined reference to variable: program_invocation_short_name
> KLEE: WARNING: undefined reference to function: rpmatch
> KLEE: WARNING: executable has module level assembly (ignoring)
> KLEE: WARNING: calling external: syscall(54, 0, 21505, 197282816)
> KLEE: WARNING: calling __user_main with extra arguments.
> KLEE: WARNING: calling external: __xstat64(3, 197158616, 197351208)
> KLEE: WARNING: calling external: gettimeofday(197357744, 0)
> KLEE: WARNING: __syscall_rt_sigaction: silently ignoring
> KLEE: WARNING: calling external: geteuid()
> KLEE: WARNING: calling external: getpagesize()
> KLEE: WARNING: pipe: ignoring (ENFILE)
> interprocess channel: Cannot pipeKLEE: WARNING: calling external:
> vprintf(188423912, 197344000)
>
> Error is not recoverable: exiting now
> : Too many open files in system
> KLEE: done: total instructions = 690615
> KLEE: done: completed paths = 1
> KLEE: done: generated tests = 1
>
> Any idea what the problem is, if I'm running KLEE wrongly, or if
> there's some problem with KLEE?
>
> Thanks,
> Jiaqi Tan
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>

Reply via email to