[klee-dev] Problem with compiling KLEE

Vinay T S (vinayts) vinayts at cisco.com
Sun Dec 29 09:53:15 GMT 2013


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


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


More information about the klee-dev mailing list