[klee-dev] klee .bca files missing

[Paul Thomson]

Try the following:
 - Look at Makefile.config in the "llvm source/build directory" and
ensure that LLVMGCC is set correctly (with full path to the binary).
 - Now, re-configure klee and make sure the "llvm source/build
directory" is specified (not the binary directory).
 - For me, in the klee directory, I have:
 -- in Makefile.config: LLVM_OBJ_ROOT is set to the "llvm source/build
directory" from previous steps.
 -- in Makefile.common I have: include
$(LLVM_OBJ_ROOT)/Makefile.config, which should ensure that the LLVMGCC
variable is set correctly.

Thanks,
Paul


On 1 February 2013 14:33, Alexandru Ionut Diaconescu
<alexandruionutdiaconescu at gmail.com> wrote:
> Hi Daniel,
>
> Thank you for your response.
>
> 1. uname -m gave me i686, so I am on 32b
> 2. yes, I have this:
>
>
> configure:13234: checking for llvm-gcc
> configure:13252: found /home/alex/llvmklee/llvm-gcc-
> 4.2-2.9-i686-linux/bin/llvm-gcc
> configure:13264: result:
> /home/alex/llvmklee/llvm-gcc-4.2-2.9-i686-linux/bin/llvm-gcc
>
> configure:13274: checking for llvm-g++
> configure:13292: found
> /home/alex/llvmklee/llvm-gcc-4.2-2.9-i686-linux/bin/llvm-g++
> configure:13304: result:
> /home/alex/llvmklee/llvm-gcc-4.2-2.9-i686-linux/bin/llvm-g++
>
> configure:13340: checking LLVM capable compiler
> configure:13358: result: llvm-gcc
>
> What do you think I can do?
>
>
> On Fri, Feb 1, 2013 at 11:34 AM, Daniel Liew <daniel.liew at imperial.ac.uk>
> wrote:
>>
>> 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
>> >
>
>
>
>
> --
> Best regards,
> Alexandru Ionut Diaconescu
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>