[klee-dev] klee .bca files missing

[Daniel Liew]

Hi Alexandru,

Can you confirm a few things for me?

1. Are you using a 32-bit version of Linux? A lot of the commands you
gave assume a 32-bit operating system. You can check by running

$ uname -m

Others have had problems when having mixed architecture builds (e.g. a
32-bit build of STP will not link with a 64-bit build of KLEE)

2. Can you check that LLVM detected your LLVM compiler (llvm-gcc) at
configure time?
To this look at the file config.log inside your LLVM build directory.
You should see a line like...
configure:13234: checking for llvm-gcc
configure:13252: found /data/dev/KLEE/llvm-gcc/bin/bin//llvm-gcc
configure:13264: result: /data/dev/KLEE/llvm-gcc/bin/bin//llvm-gcc
configure:13274: checking for llvm-g++
configure:13292: found /data/dev/KLEE/llvm-gcc/bin/bin//llvm-g++
configure:13304: result: /data/dev/KLEE/llvm-gcc/bin/bin//llvm-g++
configure:13340: checking LLVM capable compiler
configure:13358: result: llvm-gcc
configure:13363: checking tool compatibility

LLVM will still build even if llvm-gcc isn't found but KLEE will not
compile correctly if this happens.

Thanks,
Dan.

On 31 January 2013 21:07, Alexandru Ionut Diaconescu
<alexandruionutdiaconescu at gmail.com> wrote:
> Hello everyone !
>
> I followed http://klee.llvm.org/GetStarted.html when installing Klee over my
> LLVM 2.9 (as required), meaning :
>
> 1. Install dependencies DONE
>    export C_INCLUDE_PATH=/usr/include/i386-linux-gnu/ DONE
>    export CPLUS_INCLUDE_PATH/usr/include/i386-linux-gnu/ DONE
>
> 2. Build LLVM 2.9 DONE
>    Install llvm-gcc DONE
>    Add llvm-gcc to my PATH  DONE
>    export
> PATH=$PATH:/home/alex/llvm2.9/llvm/llvm-gcc-4.2-2.9-i686-linux/llvm-gcc-4.2-2.9-i686-linux/bin/
>    Download and build LLVM 2.9  DONE
>
> 3. Build STP  DONE
>    with --with-cryptominisat2 at configuration AND make OPTIMIZE=-O2
> CFLAGS_M32= install at make
>    ulimit -s unlimited DONE
>
> 4. Build uclibc with llvm-gcc DONE
>
> 5. svn klee DONE
>
> 6. Configure KLEE DONE
>    ./configure --with-llvm=/home/alex/llvm2.9/llvm/
> --with-stp=/home/alex/llvm2.9/llvm/stp/
> --with-uclibc=/home/alex/llvm2.9/llvm/klee-uclibc-0.02-i386/
> --with-llvm-build-mode=Release+Asserts --enable-posix-runtime
> 7.  Build KLEE DONE
>   with ENABLE_OPTIMIZED=1
> no errors, but I have the warning
> "/home/alex/llvm2.9/llvm/klee/Makefile.rules:1175: Bytecode libraries
> require LLVM capable compiler but none is available ****"
>
>
> However, when I am trying the tutorials, I have the segfault error :
> klee: error: Cannot find linker input
> '/home/alex/llvm2.9/llvm/klee/Release+Asserts/lib/libkleeRuntimeIntrinsic.bca'
>
>
> They were not build at all during Klee compilation. Can you tell me what can
> I do? Maybe my problem is related to this thread :
> http://thread.gmane.org/gmane.comp.compilers.llvm.klee/923 .
>
> Thank you for any help !
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>