On 16 June 2017 at 17:05, Nourah mmm <dnoo...@gmail.com> wrote: > Hi, > > I try to run KLEE on cutcp benchmark from (Parboil Benchmarks). The > benchmark consists from the following program: main.c parboil.c readatom.c > cutcpu.c excl.c output.c > > First I compile it with the following command: > myclang -I /home/klee/klee_src/include -emit-llvm -c -g main.c parboil.c > readatom.c cutcpu.c excl.c output.c > > Then, I run KLEE with this command: > myklee --posix-runtime --libc=uclibc --link-llvm-lib=parboil.bc > --link-llvm-lib=cutcpu.bc --link-llvm-lib=excl.bc --link-llvm-lib=output.bc > --link-llvm-lib=readatom.bc ./main.bc -i > /home/naloboud/parboil/datasets/cutcp/small/input/watbox.sl40.pqr > > However I get this error: > KLEE: NOTE: Using model: > /home//klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca > KLEE: Linking in library: parboil.bc. > > KLEE: Linking in library: cutcpu.bc. > > KLEE: Linking in library: excl.bc. > > KLEE: Linking in library: output.bc. > > KLEE: Linking in library: readatom.bc.
I think the problem is the way you are linking. The `--link-llvm-lib` flag links after klee-uclibc links in. The code that is failing probably comes from `readatom.bc`. This code is calling `fgets()` but because klee-uclibc has already been linked in (note we do "static style" linking so only the parts of klee-uclibc that are needs get linked in) it's too late to get a definition. Arguably this a bug in the `--link-llvm-lib` flag but I'm not particularly interested in fixing it because I voted against adding this feature when it was first introduced. What I'd recommend doing is using wllvm (https://github.com/travitch/whole-program-llvm) to build your program and tell the build system to link everything statically. If you do this everything should be linked together properly. Alternatively if you know which `bc` files you want to link together just use the `llvm-link` tool to link them all together before you give them to KLEE. HTH, Dan. _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev