Hi, Dan Liew, Thank you for your advice. Now I can use *wllvm *to generate bash.bc successfully based on the next steps:
$ export LLVM_COMPILER=llvm-gcc $ export LLVM_GCC_PREFIX=llvm- $ cd bash-4.0 $ ./configure --disable-nls CFLAGS="-g" $ make CC=wllvm $ extract-bc bash however, I cannot run klee on the generated 'bash.bc'. when I carry out: $ klee *--libc=uclibc --posix-runtime *./bash.sh test.sh I got the next error messag: KLEE: ERROR: unable to load symbol(PC) while initializing globals. Could you tell me what should I do then? Thank you very much. -------------------------------------------- Qiuping Yi Institute Of Software Chinese Academy of Sciences On Mon, Mar 24, 2014 at 7:49 PM, Daniel Liew <[email protected]>wrote: > > /home/guest/installed/klee/scripts/klee-gcc -DPROGRAM='"bash"' > > -DCONF_HOSTTYPE='"x86_64"' -DCONF_OSTYPE='"linux-gnu"' > > -DCONF_MACHTYPE='"x86_64-unknown-linux-gnu"' -DCONF_VENDOR='"unknown"' > > -DLOCALEDIR='"/usr/local/share/locale"' -DPACKAGE='"bash"' -DSHELL > > -DHAVE_CONFIG_H -I. -I. -I./include -I./lib -g -o mksyntax > > ./mksyntax.c > > /tmp/cc1H53KR.o: file not recognized: File format not recognized > > collect2: ld returned 1 exit status > > make: *** [mksyntax] Error 1 > > It looks like the script is trying to invoke your system's native > linker to build a native executable. That won't work because > /tmp/cc1H53KR.o is probably an LLVM bitcode file so the linker does > not know what to do with it. > > You probably should be using the '-c' flag so you do not invoke the > linker. This approach is really only feasible with single file > programs. > > > Furthermore, it's strange that the not recognized file keeping changed > if I > > execute 'make' again and again. For example, the second time I encounter > the > > next error message: > > > > /tmp/ccaJGvTn.o: file not recognized: File format not recognized > > It's not strange at all, the compiler is creating temporary files > during the compilation process. > > > BUT I found both file /tmp/cc1H53KR.o and /tmp/ccaJGvTn.o do not exist. > > These files are deleted automatically by the compiler because they are > temporary intermediate files. > > > What's wrong? What should I do? > > I've already explained above what is wrong. > > I do not know much about bash's build system but I would expect it to > be more complex that coreutil's. klee-gcc is a bit of a hack so you > should probably either > > - Use wllvm [1]. This is also a hack but is considerably better than > klee-gcc and can link together multi file programs. > - Use LLVM gold [2] so you can link together a multi-file program to a > bitcode module. > > > [1] https://github.com/klee/whole-program-llvm > [2] http://llvm.org/docs/GoldPlugin.html > > Thanks, > Dan Liew. >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
