[klee-dev] Problems compiling KLEE/STP

[Urmas Repinski]

Hi Luis.

According to installation manual, http://ccadar.github.io/klee/GetStarted.html
In order to install LLVM-29, first, necessary to install llvm-gcc first.
It
        is important to do this first so that llvm-gcc is
        found in subsequent configure
        steps. llvm-gcc will be used later to compile
        programs that KLEE can execute.
      

So possibly llvm-gcc were installed with error or wrong version of llvm-gcc were downloaded.
Try to download fresh copy - GCC of LLVM Version 2.9. There is different GCC-s are available to download so possibly you choosed 32-bit version instead of 64-bit, or vise versa. 

Try to reinstall then LLVM with new GCC version, if problem is with LLVM-GCC installation, then problem is there.

I used 
LLVM-GCC 4.2 Front End Binaries for FreeBSD8/x86 (23M) (.sig)
for my installation, and it worked fine.

Urmas Repinski.
Date: Mon, 2 Dec 2013 09:41:33 -0700
Subject: Re: [klee-dev] Problems compiling KLEE/STP
From: lumi.martinez at gmail.com
To: urrimus at hotmail.com; klee-dev at imperial.ac.uk

Urmas,
Thanks for your help. I was able to build STP.

However, I'm still having trouble with building Klee and re-building LLVM. 

Let me start with a question: Should llvm-2.9 be built with the normal GCC or with llvm-gcc? What about klee? 


When I tried compiling KLEE, I get the emit-llvm error. Here's the output:
/bin/sh: 0: Illegal option --
make: --emit-llvm: Command not found
make: --emit-llvm: Command not found
./extra/scripts/conf-header.sh .config > include/bits/uClibc_config.h

/bin/sh: 0: Illegal option --
make[1]: --emit-llvm: Command not found
make[1]: --emit-llvm: Command not found
extra/scripts/gen_bits_syscall_h.sh: 30: extra/scripts/gen_bits_syscall_h.sh: --emit-llvm: not found

extra/scripts/gen_bits_syscall_h.sh: 26: extra/scripts/gen_bits_syscall_h.sh: --emit-llvm: not found
  CC libcrypt/crypt.os
/bin/sh: 1: --emit-llvm: not found
make: *** [libcrypt/crypt.os] Error 127


I googled it and found that the problem is related to the fact that I am not compiling with llvm-gcc. For sure, llvm-gcc is in the path:

/home/lumi/Development/llvm-gcc4.2-2.9-x86_64-linux/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games


Any ideas how to solve this?

Help is really appreciated.

Luis



On Tue, Nov 26, 2013 at 4:46 AM, Urmas Repinski <urrimus at hotmail.com> wrote:




Hi Luis.

I had reached several errors during my klee installation, and, fortunately, i have script, that allows to install klee on 64-bit Linux Mint 13 OS with no errors, attaching script to the letter.


During step 3 i had made following modifications:

STP="stp"
# change revision number to  1180 on 64 bit system, 940 on 32 bit system
# --with-fpic configure option is required on 64 bit machines


echo " Package $STP"
svn co -r 1180 https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp $INSTALLDIR/$STP

(cd $INSTALLDIR/$STP; ./scripts/configure    --with-fpic  ; make OPTIMIZE=-O2 CFLAGS_M32= install ; ulimit -s unlimited  )

I used revision 1190 of STP instead of 940 for 64 bit machine, used CFLAGS_M32=install flag for make, used flag  --with-fpic for configure.


Hope this helps.

Urmas.


Date: Mon, 25 Nov 2013 15:52:37 -0700
From: lumi.martinez at gmail.com
To: klee-dev at keeda.stanford.edu

Subject: [klee-dev] Problems compiling KLEE/STP

Hi guys,
I'm having trouble compiling STP as instructed by http://ccadar.github.io/klee/GetStarted.html


(step 3)

I am running in a Ubuntu 12.04 LTS Linux 64-bit machine.

After failing to build with my default toolchain GCC 4.6.3, I installed version 3.4.6 of gcc, gcc-base, g++, cpp, libstdc++6 via:
$ wget http://old-releases.ubuntu.com/ubuntu/pool/universe/g/gcc-3.4/*.deb (I put each separately)


$ sudo dpkg -i *.deb

I didn't update binutils nor make.

I ran...
$ ./scripts/configure --with-prefix=/home/(myname)/stp --with-cryptominisat2, and...
$ make CC=gcc-3.4 CXX=g++-3.4 OPTIMIZE=-O2 CFLAGS_M32=



But still I get lots of warnings and an error that I print below:

In file included from Gaussian.h:32,
                 from Logger.cpp:36:
PackedMatrix.h: In member function `MINISAT::PackedRow MINISAT::PackedMatrix::iterator::operator*()':


PackedRow.h:224: error: `MINISAT::PackedRow::PackedRow(uint32_t, uint64_t*)' is private
PackedMatrix.h:141: error: within this context
Logger.cpp: In member function `void MINISAT::Logger::end(MINISAT::Logger::finish_type)':


Logger.cpp:375: warning: cast to pointer from integer of different size
make[2]: *** [Logger.o] Error 1
make[2]: Leaving directory `/home/(myname)/llvm-2.9/stp/src/sat/cryptominisat2'
make[1]: *** [cryptominisat2] Error 2


make[1]: Leaving directory `/home/(myname)/llvm-2.9/stp/src/sat'
make: *** [all] Error 2

Any ideas of what this error is and how to resolve it? 

Help is truly appreciated.



Thanks,
Luis



_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev 		 	   		  


 		 	   		  
-------------- next part --------------
HTML attachment scrubbed and removed