> /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
