[klee-dev] Problems compiling KLEE/STP

Tue Dec 3 10:04:42 GMT 2013

Hi Luis,

Please try the new version of klee-uclibc from [1] and make sure you use
the klee_0_9_29 branch.

Make sure llvm-gcc, llvm-dis and llvm-ar are in your path then run

$ ./configure -l
$ make

The version of klee-uclibc you are trying to use [2] has been broken for a
while. I've already seen the errors you've mentioned and have fixed them.

Please let me know how you get on.

[1] https://github.com/ccadar/klee-uclibc/tree/klee_0_9_29

[2] http://www.doc.ic.ac.uk/~cristic/klee/klee-uclibc-x64.html

Thanks,
Dan.
 On 3 Dec 2013 09:50, "Luis Miguel Martinez" <lumi.martinez at gmail.com>
wrote:

>  Just a clarification. My problem with --emit-llvm not being recognized
> occurs when I try to build klee-uclibc-0.02-x64, not KLEE itself.\
>
>  Also, I tried passing CC and CXX to the make command, but still got some
> errors.
>
> I entered:
>
> sudo make
> CC=/home/lumi/Development/llvm-gcc4.2-2.9-x86_64-linux/bin/llvm-gcc
> CXX=/home/lumi/Development/llvm-gcc4.2-2.9-x86_64-linux/bin/llvm-g++
>
>  It compiles a lot of stuff, but at the end I get something like this:
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
> */usr/include/asm/posix_types.h:14: error: redefinition of typedef
> '__kernel_ino_t' ./include/bits/kernel_types.h:20: error: previous
> declaration of '__kernel_ino_t' was here /usr/include/asm/posix_types.h:18:
> error: redefinition of typedef '__kernel_mode_t'
> ./include/bits/kernel_types.h:21: error: previous declaration of
> '__kernel_mode_t' was here /usr/include/asm/posix_types.h:22: error:
> redefinition of typedef '__kernel_nlink_t'
> ./include/bits/kernel_types.h:22: error: previous declaration of
> '__kernel_nlink_t' was here /usr/include/asm/posix_types.h:26: error:
> redefinition of typedef '__kernel_pid_t' ./include/bits/kernel_types.h:24:
> error: previous declaration of '__kernel_pid_t' was here
> /usr/include/asm/posix_types.h:30: error: redefinition of typedef
> '__kernel_ipc_pid_t' ./include/bits/kernel_types.h:25: error: previous
> declaration of '__kernel_ipc_pid_t' was here
> /usr/include/asm/posix_types.h:34: error: redefinition of typedef
> '__kernel_uid_t' ./include/bits/kernel_types.h:26: error: previous
> declaration of '__kernel_uid_t' was here /usr/include/asm/posix_types.h:35:
> error: redefinition of typedef '__kernel_gid_t'
> ./include/bits/kernel_types.h:27: error: previous declaration of
> '__kernel_gid_t' was here /usr/include/asm/posix_types.h:39: error:
> redefinition of typedef '__kernel_suseconds_t'
> ./include/bits/kernel_types.h:32: error: previous declaration of
> '__kernel_suseconds_t' was here /usr/include/asm/posix_types.h:43: error:
> redefinition of typedef '__kernel_daddr_t'
> ./include/bits/kernel_types.h:34: error: previous declaration of
> '__kernel_daddr_t' was here /usr/include/asm/posix_types.h:47: error:
> redefinition of typedef '__kernel_uid32_t'
> ./include/bits/kernel_types.h:38: error: previous declaration of
> '__kernel_uid32_t' was here /usr/include/asm/posix_types.h:48: error:
> redefinition of typedef '__kernel_gid32_t'
> ./include/bits/kernel_types.h:39: error: previous declaration of
> '__kernel_gid32_t' was here /usr/include/asm/posix_types.h:52: error:
> conflicting types for '__kernel_old_uid_t'
> ./include/bits/kernel_types.h:40: error: previous declaration of
> '__kernel_old_uid_t' was here /usr/include/asm/posix_types.h:53: error:
> conflicting types for '__kernel_old_gid_t'
> ./include/bits/kernel_types.h:41: error: previous declaration of
> '__kernel_old_gid_t' was here /usr/include/asm/posix_types.h:57: error:
> conflicting types for '__kernel_old_dev_t'
> ./include/bits/kernel_types.h:42: error: previous declaration of
> '__kernel_old_dev_t' was here /usr/include/asm/posix_types.h:66: error:
> conflicting types for '__kernel_size_t' ./include/bits/kernel_types.h:28:
> error: previous declaration of '__kernel_size_t' was here
> /usr/include/asm/posix_types.h:67: error: conflicting types for
> '__kernel_ssize_t' ./include/bits/kernel_types.h:29: error: previous
> declaration of '__kernel_ssize_t' was here
> /usr/include/asm/posix_types.h:68: error: conflicting types for
> '__kernel_ptrdiff_t' ./include/bits/kernel_types.h:30: error: previous
> declaration of '__kernel_ptrdiff_t' was here
> /usr/include/asm/posix_types.h:79: error: redefinition of typedef
> '__kernel_off_t' ./include/bits/kernel_types.h:23: error: previous
> declaration of '__kernel_off_t' was here /usr/include/asm/posix_types.h:80:
> error: redefinition of typedef '__kernel_loff_t'
> ./include/bits/kernel_types.h:43: error: previous declaration of
> '__kernel_loff_t' was here /usr/include/asm/posix_types.h:81: error:
> redefinition of typedef '__kernel_time_t' ./include/bits/kernel_types.h:31:
> error: previous declaration of '__kernel_time_t' was here
> /usr/include/asm/posix_types.h:82: error: redefinition of typedef
> '__kernel_clock_t' ./include/bits/kernel_types.h:33: error: previous
> declaration of '__kernel_clock_t' was here
> /usr/include/asm/posix_types.h:85: error: redefinition of typedef
> '__kernel_caddr_t' ./include/bits/kernel_types.h:35: error: previous
> declaration of '__kernel_caddr_t' was here
> /usr/include/asm/posix_types.h:86: error: redefinition of typedef
> '__kernel_uid16_t' ./include/bits/kernel_types.h:36: error: previous
> declaration of '__kernel_uid16_t' was here
> /usr/include/asm/posix_types.h:87: error: redefinition of typedef
> '__kernel_gid16_t' ./include/bits/kernel_types.h:37: error: previous
> declaration of '__kernel_gid16_t' was here
> /usr/include/asm/posix_types.h:91: error: conflicting types for
> '__kernel_fsid_t' ./include/bits/kernel_types.h:51: error: previous
> declaration of '__kernel_fsid_t' was here *
>  Help is appreciated.
>
> Thanks,
> Luis
>
>
> On Mon, Dec 2, 2013 at 9:41 AM, Luis Miguel Martinez <
> lumi.martinez at gmail.com> wrote:
>
>>    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