[klee-dev] Running Multifile Applications using Klee

[Daniel Liew]

On 20 September 2013 17:15, Saikat Dutta <saikatdutta.pro2011 at gmail.com> wrote:
> Hi,
> Everything goes fine with wllvm according to the way you described in the
> previous mail. No errors till make step.

If you don't tell us what the errors are we will **not** be able to
help you. If you see an error tell us what it is.

> But instead of "gzip.bc" or
> "gzip.o.bc" , ".gzip.o.bc" is being formed.

.gzip.o.bc is a LLVM bitcode file that corresponds to the gzip.o
object file (this mostly likely corresponds with gzip.c) . It is
**not** the finally linked executable. You are only supposed to run
extract-bc on the the finally linked executable (or on static
libraries) **not** on object files.

I just tried this and it works fine. You should run extract-bc on the
"gzip" executable.

# I assume you have llvm-gcc in your path and it was the pre-built
binary llvm-gcc 4.2

$ export LLVM_COMPILER=llvm-gcc
$ export WLLVM_OUTPUT=WARNING
$ export LLVM_COMPILER_PATH=/your/path/to/the/llvm2.9/build/Release+Asserts/bin
$ wget http://ftp.gnu.org/gnu/gzip/gzip-1.6.tar.xz
$ tar -xvf gzip-1.6.tar.xz
$ cd gzip-1.6
$ CC=wllvm ./configure
$ make -j4
$ extract-bc gzip

# gzip.bc will now be in the current directory

> When I use extract bc on it,
> error is generated. Please help.
> -Saikat

Again... If there is an error message tell us what it is.

Hope that helps.

Dan.