[klee-dev] klee .bca files missing

[Alexandru Ionut Diaconescu]

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
-------------- next part --------------
HTML attachment scrubbed and removed