[klee-dev] Strange error when compiling 'bash-4.0' using klee-gcc

[Daniel Liew]

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