Hi, I'm trying to run KLEE with tar 1.19. I have managed to compile tar with KLEE, and I'm trying to generate one symbolic file input to represent/simulate an input tar file.
I'm currently running KLEE with the following command line call: $ klee --libc=uclibc --posix-runtime --max-time 30 --init-env ./src/a.out.bc -xz --sym-files 1 100000 I have two questions regarding symbolic file inputs: 1. Is the first symbolic file input always passed to stdin of the program being called? 2. For the subsequent symbolic input files beyond the first, how do these get passed to the program/how does the program access these files? Or are the multiple symbolic input files passed to the program one after another, with as many runs of the program as there are symbolic input files specified? Also, I got this error from (the LLVM-compiled version of) tar: ===== BEGIN OUTPUT ===== KLEE: WARNING: pipe: ignoring (ENFILE) interprocess channel: Cannot pipeKLEE: WARNING: calling external: vprintf(188424464, 202253304) Error is not recoverable: exiting now : Too many open files in system KLEE: done: total instructions = 690302 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 ===== END OUTPUT ===== Any ideas what this means? Thanks, Jiaqi Tan
