[klee-dev] Problem with compiling KLEE

Daniel Liew daniel.liew at imperial.ac.uk
Sun Dec 29 12:43:45 GMT 2013


Hi Vinay,

This is due to a change I added recently. I need to replace it with
something because the LLVM API I used is deprecated and taking the
address of main isn't supposed to be allowed in ISO C++.

Provided you only run KLEE from the build directory (i.e. you do not
try to install it and then run the installed version) then you can
checkout a slightly older copy without support for KLEE running from
an install directory which doesn't have the code which is causing you
issues.

$ cd klee-src-directory/
$ git checkout 857831d18708ada4590c511494d3ae5f94cf6a6a

Could you add this issue to our issue tracker [1]. I need to fix this
at some point.

[1] https://github.com/ccadar/klee/issues

Thanks,
Dan.



On 29 December 2013 09:53, Vinay T S (vinayts) <vinayts at cisco.com> wrote:
> Hello,
>
> My setup details :
>
>
> /root/bin/stp : compiled from STP r940 code base  .
>
> [root at vinayts-lab-lnx klee-master]# which llvm-gcc
> /usr/bin/llvm-gcc
> [root at vinayts-lab-lnx klee-master]# llvm-gcc --version
> llvm-gcc (GCC) 4.2.1 (Based on Apple Inc. build 5658) (LLVM build 2.9)
> Copyright (C) 2007 Free Software Foundation, Inc.
> This is free software; see the source for copying conditions.  There is NO
> warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
>
> Could install ucLibC from the instructions provided at :
> http://ccadar.github.io/klee/GetStarted.html
>
> [root at vinayts-lab-lnx klee-master]# uname -a
> Linux vinayts-lab-lnx 2.6.18-194.8.1.el5 #1 SMP Wed Jun 23 10:52:51 EDT 2010
> x86_64 x86_64 x86_64 GNU/Linux
>
> [root at vinayts-lab-lnx klee-master]# gcc -v
> Using built-in specs.
> Target: x86_64-unknown-linux-gnu
> Configured with: ../gcc-4.2.4/configure --prefix=/usr --libexecdir=/usr/lib
> --enable-shared --enable-threads=posix --enable-__cxa_atexit
> --enable-clocale=gnu --enable-languages=c,c++,fortran,java,objc,treelang
> Thread model: posix
> gcc version 4.2.4
>
> Am trying to build KLEE now ( picked up the latest downloadable version from
> github) .
>
> Ran into some issues :
>
>
> [root at vinayts-lab-lnx klee-master]# pwd
> /usr/local/src/klee-master
>
> make ENABLE_OPTIMIZED=1 -j10
>
> make[1]: Entering directory `/usr/local/src/klee-master/lib'
> make[2]: Entering directory `/usr/local/src/klee-master/lib/Support'
> make[2]: Nothing to be done for `all'.
> make[2]: Leaving directory `/usr/local/src/klee-master/lib/Support'
> make[2]: Entering directory `/usr/local/src/klee-master/lib/Basic'
> make[2]: Nothing to be done for `all'.
> make[2]: Leaving directory `/usr/local/src/klee-master/lib/Basic'
> make[2]: Entering directory `/usr/local/src/klee-master/lib/Solver'
> make[2]: Entering directory `/usr/local/src/klee-master/lib/Expr'
> make[2]: Nothing to be done for `all'.
> make[2]: Leaving directory `/usr/local/src/klee-master/lib/Expr'
> llvm[2]: Compiling STPBuilder.cpp for Release+Asserts build
> llvm[2]: Compiling Solver.cpp for Release+Asserts build
> make[2]: Entering directory `/usr/local/src/klee-master/lib/Module'
> make[2]: Nothing to be done for `all'.
> make[2]: Leaving directory `/usr/local/src/klee-master/lib/Module'
> make[2]: Entering directory `/usr/local/src/klee-master/lib/Core'
> make[2]: Nothing to be done for `all'.
> make[2]: Leaving directory `/usr/local/src/klee-master/lib/Core'
> In file included from STPBuilder.h:14,
>                  from Solver.cpp:14:
> /usr/local/src/klee-master/include/klee/util/ArrayExprHash.h:135:7: warning:
> no newline at end of file
> In file included from STPBuilder.h:14,
>                  from STPBuilder.cpp:10:
> /usr/local/src/klee-master/include/klee/util/ArrayExprHash.h:135:7: warning:
> no newline at end of file
> llvm[2]: Building Release+Asserts Archive Library libkleaverSolver.a
> make[2]: Leaving directory `/usr/local/src/klee-master/lib/Solver'
> make[1]: Leaving directory `/usr/local/src/klee-master/lib'
> make[1]: Entering directory `/usr/local/src/klee-master/tools'
> make[2]: Entering directory `/usr/local/src/klee-master/tools/klee-stats'
> make[2]: Nothing to be done for `all'.
> make[2]: Leaving directory `/usr/local/src/klee-master/tools/klee-stats'
> make[2]: Entering directory `/usr/local/src/klee-master/tools/ktest-tool'
> make[2]: Nothing to be done for `all'.
> make[2]: Leaving directory `/usr/local/src/klee-master/tools/ktest-tool'
> make[2]: Entering directory
> `/usr/local/src/klee-master/tools/gen-random-bout'
> make[2]: Nothing to be done for `all'.
> make[2]: Leaving directory
> `/usr/local/src/klee-master/tools/gen-random-bout'
> make[2]: Entering directory `/usr/local/src/klee-master/tools/klee-replay'
> make[2]: Nothing to be done for `all'.
> make[2]: Leaving directory `/usr/local/src/klee-master/tools/klee-replay'
> perl: warning: Setting locale failed.
> perl: warning: Please check that your locale settings:
> LANGUAGE = (unset),
> LC_ALL = (unset),
> LC_CTYPE = "UTF-8",
> LANG = "en_US.UTF-8"
>     are supported and installed on your system.
> perl: warning: Falling back to the standard locale ("C").
> perl: warning: Setting locale failed.
> perl: warning: Please check that your locale settings:
> LANGUAGE = (unset),
> LC_ALL = (unset),
> LC_CTYPE = "UTF-8",
> LANG = "en_US.UTF-8"
>     are supported and installed on your system.
> perl: warning: Falling back to the standard locale ("C").
> perl: warning: Setting locale failed.
> perl: warning: Please check that your locale settings:
> LANGUAGE = (unset),
> LC_ALL = (unset),
> LC_CTYPE = "UTF-8",
> LANG = "en_US.UTF-8"
>     are supported and installed on your system.
> perl: warning: Falling back to the standard locale ("C").
> perl: warning: Setting locale failed.
> perl: warning: Please check that your locale settings:
> LANGUAGE = (unset),
> LC_ALL = (unset),
> LC_CTYPE = "UTF-8",
> LANG = "en_US.UTF-8"
>     are supported and installed on your system.
> perl: warning: Falling back to the standard locale ("C").
> make[2]: Entering directory `/usr/local/src/klee-master/tools/kleaver'
> llvm[2]: Linking Release+Asserts executable kleaver (without symbols)
> make[2]: Entering directory `/usr/local/src/klee-master/tools/klee'
> llvm[2]: Compiling main.cpp for Release+Asserts build
> In file included from
> /usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
>                  from
> /usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
>                  from main.cpp:32:
> /usr/local/src/llvm-2.9/include/llvm/Config/config.h:641:1: warning:
> "PACKAGE_BUGREPORT" redefined
> In file included from
> /usr/local/src/klee-master/include/klee/Config/Version.h:13,
>                  from
> /usr/local/src/klee-master/include/klee/util/Bits.h:13,
>                  from /usr/local/src/klee-master/include/klee/Expr.h:13,
>                  from
> /usr/local/src/klee-master/include/klee/Constraints.h:13,
>                  from
> /usr/local/src/klee-master/include/klee/ExecutionState.h:13,
>                  from main.cpp:6:
> /usr/local/src/klee-master/include/klee/Config/config.h:59:1: warning: this
> is the location of the previous definition
> In file included from
> /usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
>                  from
> /usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
>                  from main.cpp:32:
> /usr/local/src/llvm-2.9/include/llvm/Config/config.h:644:1: warning:
> "PACKAGE_NAME" redefined
> In file included from
> /usr/local/src/klee-master/include/klee/Config/Version.h:13,
>                  from
> /usr/local/src/klee-master/include/klee/util/Bits.h:13,
>                  from /usr/local/src/klee-master/include/klee/Expr.h:13,
>                  from
> /usr/local/src/klee-master/include/klee/Constraints.h:13,
>                  from
> /usr/local/src/klee-master/include/klee/ExecutionState.h:13,
>                  from main.cpp:6:
> /usr/local/src/klee-master/include/klee/Config/config.h:62:1: warning: this
> is the location of the previous definition
> In file included from
> /usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
>                  from
> /usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
>                  from main.cpp:32:
> /usr/local/src/llvm-2.9/include/llvm/Config/config.h:647:1: warning:
> "PACKAGE_STRING" redefined
> In file included from
> /usr/local/src/klee-master/include/klee/Config/Version.h:13,
>                  from
> /usr/local/src/klee-master/include/klee/util/Bits.h:13,
>                  from /usr/local/src/klee-master/include/klee/Expr.h:13,
>                  from
> /usr/local/src/klee-master/include/klee/Constraints.h:13,
>                  from
> /usr/local/src/klee-master/include/klee/ExecutionState.h:13,
>                  from main.cpp:6:
> /usr/local/src/klee-master/include/klee/Config/config.h:65:1: warning: this
> is the location of the previous definition
> In file included from
> /usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
>                  from
> /usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
>                  from main.cpp:32:
> /usr/local/src/llvm-2.9/include/llvm/Config/config.h:650:1: warning:
> "PACKAGE_TARNAME" redefined
> In file included from
> /usr/local/src/klee-master/include/klee/Config/Version.h:13,
>                  from
> /usr/local/src/klee-master/include/klee/util/Bits.h:13,
>                  from /usr/local/src/klee-master/include/klee/Expr.h:13,
>                  from
> /usr/local/src/klee-master/include/klee/Constraints.h:13,
>                  from
> /usr/local/src/klee-master/include/klee/ExecutionState.h:13,
>                  from main.cpp:6:
> /usr/local/src/klee-master/include/klee/Config/config.h:68:1: warning: this
> is the location of the previous definition
> In file included from
> /usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
>                  from
> /usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
>                  from main.cpp:32:
> /usr/local/src/llvm-2.9/include/llvm/Config/config.h:653:1: warning:
> "PACKAGE_VERSION" redefined
> In file included from
> /usr/local/src/klee-master/include/klee/Config/Version.h:13,
>                  from
> /usr/local/src/klee-master/include/klee/util/Bits.h:13,
>                  from /usr/local/src/klee-master/include/klee/Expr.h:13,
>                  from
> /usr/local/src/klee-master/include/klee/Constraints.h:13,
>                  from
> /usr/local/src/klee-master/include/klee/ExecutionState.h:13,
>                  from main.cpp:6:
> /usr/local/src/klee-master/include/klee/Config/config.h:74:1: warning: this
> is the location of the previous definition
> llvm[2]: ======= Finished Linking Release+Asserts Executable kleaver
> (without symbols)
> make[2]: Leaving directory `/usr/local/src/klee-master/tools/kleaver'
> main.cpp: In function 'void parseArguments(int, char**)':
> main.cpp:653: warning: cast from type 'const char**' to type 'char**' casts
> away constness
> main.cpp: In function 'int main(int, char**, char**)':
> main.cpp:1263: error: ISO C++ forbids taking address of function '::main'
> main.cpp:1263: warning: ISO C++ forbids casting between pointer-to-function
> and pointer-to-object
> make[2]: *** [/usr/local/src/klee-master/tools/klee/Release+Asserts/main.o]
> Error 1
> make[2]: Leaving directory `/usr/local/src/klee-master/tools/klee'
> make[1]: *** [klee/.makeall] Error 2
> make[1]: Leaving directory `/usr/local/src/klee-master/tools'
> make: *** [all] Error 1
>
>
> On examining line 1263 :
>
> 1262    :   llvm::sys::Path LibraryDir =
> KleeHandler::getRunTimeLibraryPath(argv[0],
>  1263   :                         reinterpret_cast<void*>(main));
>  1264  : Interpreter::ModuleOptions Opts(LibraryDir.c_str(),
>
> Seems like gcc 4.2.4 does not like this ( in line 1263)  . I am not too good
> at C++, wanted to check how to get around this compilation issue .
>
> Thanks
> Vinay
>
>




More information about the klee-dev mailing list