Hello!
I am a Chinese student and I am intereted in KLEE. But I run into several
problems when I build and use KlEE.
The first problem, I am sure I follow the instructions in the Getting
Started page http://klee.llvm.org/GetStarted.html. All is OK until I run make
check. Below is the detail information.
ct at ct-ubuntu:~/klee/klee_sources$ make check
llvm[0]: Running test suite
make[1]: Entering directory `/home/ct/klee/klee_sources/test'
Making a new site.exp file...
*** dejagnu not found. Make sure runtest is in your PATH, then reconfigure
llvm.
make[1]: Leaving directory `/home/ct/klee/klee_sources/test'
But make unittests seems to be OK.
ct at ct-ubuntu:~/klee/klee_sources$ make unittests
llvm[0]: Running unittests test suite
make[1]: Entering directory `/home/ct/klee/klee_sources/unittests'
make[2]: Entering directory `/home/ct/klee/klee_sources/unittests/Expr'
llvm[2]: Compiling ExprTest.cpp for Release build
llvm[2]: Linking Release unit test Expr (without symbols)
llvm[2]: ======= Finished Linking Release Unit test Expr (without symbols)
Release/ExprTests
[==========] Running 3 tests from 1 test case.
[----------] Global test environment set-up.
[----------] 3 tests from ExprTest
[ RUN ] ExprTest.BasicConstruction
[ OK ] ExprTest.BasicConstruction
[ RUN ] ExprTest.ConcatExtract
[ OK ] ExprTest.ConcatExtract
[ RUN ] ExprTest.ExtractConcat
[ OK ] ExprTest.ExtractConcat
[----------] Global test environment tear-down
[==========] 3 tests from 1 test case ran.
[ PASSED ] 3 tests.
make[2]: Leaving directory `/home/ct/klee/klee_sources/unittests/Expr'
make[2]: Entering directory `/home/ct/klee/klee_sources/unittests/Solver'
llvm[2]: Compiling SolverTest.cpp for Release build
llvm[2]: Linking Release unit test Solver (without symbols)
llvm[2]: ======= Finished Linking Release Unit test Solver (without symbols)
Release/SolverTests
[==========] Running 1 test from 1 test case.
[----------] Global test environment set-up.
[----------] 1 test from SolverTest
[ RUN ] SolverTest.Evaluation
[ OK ] SolverTest.Evaluation
[----------] Global test environment tear-down
[==========] 1 test from 1 test case ran.
[ PASSED ] 1 test.
make[2]: Leaving directory `/home/ct/klee/klee_sources/unittests/Solver'
make[1]: Leaving directory `/home/ct/klee/klee_sources/unittests'
Then I follow the instructions of Tutorial One: Testing a Small Function in
the page http://klee.llvm.org/Tutorial-1.html, I find KLEE works well. So could
you answer me why make check fail?
The next step, I want to feed KLEE with a test case which contains a extern
function. Here is the source code of the test case.
#include </home/ct/klee/klee_sources/include/klee/klee.h>
#include "math.h"
int my_islower(double x) {
if(pow(x,2) == 16)
return 1;
else return 0;
}
int main(int argc, char** argv) {
char c1;
klee_make_symbolic(&c1, sizeof(c1), "input1");
return my_islower(c1);
}
In which, pow is a extern function. I follow the instructions in in the
Getting Started page http://klee.llvm.org/GetStarted.html and rebuild KLEE.
Make seems to work fine.
ct at ct-ubuntu:~/klee/klee_sources$ ./configure
--with-llvm=/home/ct/klee/llvm-2.7 --with-uclibc=/home/ct/klee/klee-uclibc
--enable-posix-runtime
checking build system type... i686-pc-linux-gnu
checking host system type... i686-pc-linux-gnu
checking target system type... i686-pc-linux-gnu
checking type of operating system we're going to host on...
checking llvm source dir... /home/ct/klee/llvm-2.7
checking llvm obj dir... /home/ct/klee/llvm-2.7
checking llvm package version... 2.7
checking llvm version major... 2
checking llvm version minor... 7
checking llvm is release version... 1
checking uclibc... /home/ct/klee/klee-uclibc
checking POSIX runtime... yes
checking runtime configuration... Release
checking for gcc... gcc
checking for C compiler default output file name... a.out
checking whether the C compiler works... yes
checking whether we are cross compiling... no
checking for suffix of executables...
checking for suffix of object files... o
checking whether we are using the GNU C compiler... yes
checking whether gcc accepts -g... yes
checking for gcc option to accept ISO C89... none needed
checking how to run the C preprocessor... gcc -E
checking for grep that handles long lines and -e... /bin/grep
checking for egrep... /bin/grep -E
checking for ANSI C header files... yes
checking for sys/types.h... yes
checking for sys/stat.h... yes
checking for stdlib.h... yes
checking for string.h... yes
checking for memory.h... yes
checking for strings.h... yes
checking for inttypes.h... yes
checking for stdint.h... yes
checking for unistd.h... yes
checking sys/acl.h usability... no
checking sys/acl.h presence... no
checking for sys/acl.h... no
checking for g++... g++
checking whether we are using the GNU C++ compiler... yes
checking whether g++ accepts -g... yes
checking how to run the C++ preprocessor... g++ -E
checking selinux/selinux.h usability... no
checking selinux/selinux.h presence... no
checking for selinux/selinux.h... no
configure: creating ./config.status
config.status: creating Makefile.config
config.status: creating include/klee/Config/config.h
config.status: include/klee/Config/config.h is unchanged
config.status: executing setup commands
config.status: executing Makefile commands
config.status: executing Makefile.common commands
config.status: executing lib/Makefile commands
config.status: executing runtime/Makefile commands
config.status: executing stp/Makefile commands
config.status: executing test/Makefile commands
config.status: executing test/Makefile.tests commands
config.status: executing tools/Makefile commands
config.status: executing unittests/Makefile commands
ct at ct-ubuntu:~/klee/klee_sources$ make clean
make[1]: Entering directory `/home/ct/klee/klee_sources/lib'
make[2]: Entering directory `/home/ct/klee/klee_sources/lib/Basic'
make[2]: Leaving directory `/home/ct/klee/klee_sources/lib/Basic'
make[2]: Entering directory `/home/ct/klee/klee_sources/lib/Support'
make[2]: Leaving directory `/home/ct/klee/klee_sources/lib/Support'
make[2]: Entering directory `/home/ct/klee/klee_sources/lib/Expr'
make[2]: Leaving directory `/home/ct/klee/klee_sources/lib/Expr'
make[2]: Entering directory `/home/ct/klee/klee_sources/lib/Solver'
make[2]: Leaving directory `/home/ct/klee/klee_sources/lib/Solver'
make[2]: Entering directory `/home/ct/klee/klee_sources/lib/Module'
make[2]: Leaving directory `/home/ct/klee/klee_sources/lib/Module'
make[2]: Entering directory `/home/ct/klee/klee_sources/lib/Core'
make[2]: Leaving directory `/home/ct/klee/klee_sources/lib/Core'
make[1]: Leaving directory `/home/ct/klee/klee_sources/lib'
make[1]: Entering directory `/home/ct/klee/klee_sources/stp'
make[2]: Entering directory `/home/ct/klee/klee_sources/stp/AST'
make[2]: Leaving directory `/home/ct/klee/klee_sources/stp/AST'
make[2]: Entering directory `/home/ct/klee/klee_sources/stp/bitvec'
make[2]: Leaving directory `/home/ct/klee/klee_sources/stp/bitvec'
make[2]: Entering directory `/home/ct/klee/klee_sources/stp/c_interface'
make[2]: Leaving directory `/home/ct/klee/klee_sources/stp/c_interface'
make[2]: Entering directory `/home/ct/klee/klee_sources/stp/constantbv'
make[2]: Leaving directory `/home/ct/klee/klee_sources/stp/constantbv'
make[2]: Entering directory `/home/ct/klee/klee_sources/stp/sat'
make[2]: Leaving directory `/home/ct/klee/klee_sources/stp/sat'
make[2]: Entering directory `/home/ct/klee/klee_sources/stp/simplifier'
make[2]: Leaving directory `/home/ct/klee/klee_sources/stp/simplifier'
make[1]: Leaving directory `/home/ct/klee/klee_sources/stp'
make[1]: Entering directory `/home/ct/klee/klee_sources/tools'
make[2]: Entering directory `/home/ct/klee/klee_sources/tools/klee'
make[2]: Leaving directory `/home/ct/klee/klee_sources/tools/klee'
make[2]: Entering directory `/home/ct/klee/klee_sources/tools/kleaver'
make[2]: Leaving directory `/home/ct/klee/klee_sources/tools/kleaver'
make[2]: Entering directory `/home/ct/klee/klee_sources/tools/ktest-tool'
make[2]: Leaving directory `/home/ct/klee/klee_sources/tools/ktest-tool'
make[2]: Entering directory `/home/ct/klee/klee_sources/tools/gen-random-bout'
make[2]: Leaving directory `/home/ct/klee/klee_sources/tools/gen-random-bout'
make[2]: Entering directory `/home/ct/klee/klee_sources/tools/klee-stats'
make[2]: Leaving directory `/home/ct/klee/klee_sources/tools/klee-stats'
make[2]: Entering directory `/home/ct/klee/klee_sources/tools/klee-replay'
make[2]: Leaving directory `/home/ct/klee/klee_sources/tools/klee-replay'
make[1]: Leaving directory `/home/ct/klee/klee_sources/tools'
make[1]: Entering directory `/home/ct/klee/klee_sources/runtime'
make[2]: Entering directory `/home/ct/klee/klee_sources/runtime/Intrinsic'
make[2]: Leaving directory `/home/ct/klee/klee_sources/runtime/Intrinsic'
make[2]: Entering directory `/home/ct/klee/klee_sources/runtime/klee-libc'
make[2]: Leaving directory `/home/ct/klee/klee_sources/runtime/klee-libc'
make[2]: Entering directory `/home/ct/klee/klee_sources/runtime/Runtest'
make[2]: Leaving directory `/home/ct/klee/klee_sources/runtime/Runtest'
make[2]: Entering directory `/home/ct/klee/klee_sources/runtime/POSIX'
make[2]: Leaving directory `/home/ct/klee/klee_sources/runtime/POSIX'
make[1]: Leaving directory `/home/ct/klee/klee_sources/runtime'
make -C test clean
make[1]: Entering directory `/home/ct/klee/klee_sources/test'
/bin/rm -f a.out core
/bin/rm -rf Output/
/bin/rm -rf `find /home/ct/klee/klee_sources/test -name Output -type d -print`
/bin/rm -rf `find /home/ct/klee/klee_sources/test -name 'ft-out*' -type d
-print`
/bin/rm -rf `find /home/ct/klee/klee_sources/test -name 'ft-last' -print`
/bin/rm -rf `find /home/ct/klee/klee_sources/test -name 'klee-last'`
/bin/rm -rf `find /home/ct/klee/klee_sources/test -name 'klee-out*'`
/bin/rm -rf `find /home/ct/klee/klee_sources/test -name '*~'`
/bin/rm -rf `find /home/ct/klee/klee_sources/test -name test.log`
rm -f site.exp
make[1]: Leaving directory `/home/ct/klee/klee_sources/test'
make -C unittests clean
make[1]: Entering directory `/home/ct/klee/klee_sources/unittests'
make[2]: Entering directory `/home/ct/klee/klee_sources/unittests/Expr'
make[2]: Leaving directory `/home/ct/klee/klee_sources/unittests/Expr'
make[2]: Entering directory `/home/ct/klee/klee_sources/unittests/Solver'
make[2]: Leaving directory `/home/ct/klee/klee_sources/unittests/Solver'
make[1]: Leaving directory `/home/ct/klee/klee_sources/unittests'
rm -rf docs/doxygen
ct at ct-ubuntu:~/klee/klee_sources$ make ENABLE_OPTIMIZED=1
make[1]: Entering directory `/home/ct/klee/klee_sources/lib'
make[2]: Entering directory `/home/ct/klee/klee_sources/lib/Basic'
llvm[2]: Compiling KTest.cpp for Release build
llvm[2]: Compiling Statistics.cpp for Release build
llvm[2]: Building Release Archive Library libkleeBasic.a
make[2]: Leaving directory `/home/ct/klee/klee_sources/lib/Basic'
make[2]: Entering directory `/home/ct/klee/klee_sources/lib/Support'
llvm[2]: Compiling RNG.cpp for Release build
llvm[2]: Compiling Time.cpp for Release build
llvm[2]: Compiling Timer.cpp for Release build
llvm[2]: Compiling TreeStream.cpp for Release build
llvm[2]: Building Release Archive Library libkleeSupport.a
make[2]: Leaving directory `/home/ct/klee/klee_sources/lib/Support'
make[2]: Entering directory `/home/ct/klee/klee_sources/lib/Expr'
llvm[2]: Compiling Constraints.cpp for Release build
llvm[2]: Compiling Expr.cpp for Release build
llvm[2]: Compiling ExprBuilder.cpp for Release build
llvm[2]: Compiling ExprEvaluator.cpp for Release build
llvm[2]: Compiling ExprPPrinter.cpp for Release build
llvm[2]: Compiling ExprUtil.cpp for Release build
llvm[2]: Compiling ExprVisitor.cpp for Release build
llvm[2]: Compiling Lexer.cpp for Release build
llvm[2]: Compiling Parser.cpp for Release build
llvm[2]: Compiling Updates.cpp for Release build
llvm[2]: Building Release Archive Library libkleaverExpr.a
make[2]: Leaving directory `/home/ct/klee/klee_sources/lib/Expr'
make[2]: Entering directory `/home/ct/klee/klee_sources/lib/Solver'
llvm[2]: Compiling CachingSolver.cpp for Release build
llvm[2]: Compiling CexCachingSolver.cpp for Release build
llvm[2]: Compiling ConstantDivision.cpp for Release build
llvm[2]: Compiling FastCexSolver.cpp for Release build
llvm[2]: Compiling IncompleteSolver.cpp for Release build
llvm[2]: Compiling IndependentSolver.cpp for Release build
llvm[2]: Compiling PCLoggingSolver.cpp for Release build
llvm[2]: Compiling STPBuilder.cpp for Release build
llvm[2]: Compiling Solver.cpp for Release build
llvm[2]: Compiling SolverStats.cpp for Release build
llvm[2]: Building Release Archive Library libkleaverSolver.a
make[2]: Leaving directory `/home/ct/klee/klee_sources/lib/Solver'
make[2]: Entering directory `/home/ct/klee/klee_sources/lib/Module'
llvm[2]: Compiling Checks.cpp for Release build
llvm[2]: Compiling InstructionInfoTable.cpp for Release build
llvm[2]: Compiling IntrinsicCleaner.cpp for Release build
llvm[2]: Compiling KInstruction.cpp for Release build
llvm[2]: Compiling KModule.cpp for Release build
llvm[2]: Compiling LowerSwitch.cpp for Release build
llvm[2]: Compiling ModuleUtil.cpp for Release build
llvm[2]: Compiling Optimize.cpp for Release build
llvm[2]: Compiling PhiCleaner.cpp for Release build
llvm[2]: Compiling RaiseAsm.cpp for Release build
llvm[2]: Building Release Archive Library libkleeModule.a
make[2]: Leaving directory `/home/ct/klee/klee_sources/lib/Module'
make[2]: Entering directory `/home/ct/klee/klee_sources/lib/Core'
llvm[2]: Compiling AddressSpace.cpp for Release build
llvm[2]: Compiling CallPathManager.cpp for Release build
llvm[2]: Compiling Common.cpp for Release build
llvm[2]: Compiling Context.cpp for Release build
llvm[2]: Compiling CoreStats.cpp for Release build
llvm[2]: Compiling ExecutionState.cpp for Release build
llvm[2]: Compiling Executor.cpp for Release build
llvm[2]: Compiling ExecutorTimers.cpp for Release build
llvm[2]: Compiling ExecutorUtil.cpp for Release build
llvm[2]: Compiling ExternalDispatcher.cpp for Release build
llvm[2]: Compiling ImpliedValue.cpp for Release build
llvm[2]: Compiling Memory.cpp for Release build
llvm[2]: Compiling MemoryManager.cpp for Release build
llvm[2]: Compiling PTree.cpp for Release build
llvm[2]: Compiling Searcher.cpp for Release build
llvm[2]: Compiling SeedInfo.cpp for Release build
llvm[2]: Compiling SpecialFunctionHandler.cpp for Release build
llvm[2]: Compiling StatsTracker.cpp for Release build
llvm[2]: Compiling TimingSolver.cpp for Release build
llvm[2]: Compiling UserSearcher.cpp for Release build
llvm[2]: Building Release Archive Library libkleeCore.a
make[2]: Leaving directory `/home/ct/klee/klee_sources/lib/Core'
make[1]: Leaving directory `/home/ct/klee/klee_sources/lib'
make[1]: Entering directory `/home/ct/klee/klee_sources/stp'
make[2]: Entering directory `/home/ct/klee/klee_sources/stp/AST'
llvm[2]: Compiling AST.cpp for Release build
llvm[2]: Compiling ASTKind.cpp for Release build
llvm[2]: Compiling ASTUtil.cpp for Release build
llvm[2]: Compiling BitBlast.cpp for Release build
llvm[2]: Compiling SimpBool.cpp for Release build
llvm[2]: Compiling ToCNF.cpp for Release build
llvm[2]: Compiling ToSAT.cpp for Release build
llvm[2]: Compiling Transform.cpp for Release build
llvm[2]: Building Release Archive Library libstp_AST.a
make[2]: Leaving directory `/home/ct/klee/klee_sources/stp/AST'
make[2]: Entering directory `/home/ct/klee/klee_sources/stp/bitvec'
llvm[2]: Compiling consteval.cpp for Release build
llvm[2]: Building Release Archive Library libstp_bitvec.a
make[2]: Leaving directory `/home/ct/klee/klee_sources/stp/bitvec'
make[2]: Entering directory `/home/ct/klee/klee_sources/stp/c_interface'
llvm[2]: Compiling c_interface.cpp for Release build
llvm[2]: Building Release Archive Library libstp_c_interface.a
make[2]: Leaving directory `/home/ct/klee/klee_sources/stp/c_interface'
make[2]: Entering directory `/home/ct/klee/klee_sources/stp/constantbv'
llvm[2]: Compiling constantbv.cpp for Release build
llvm[2]: Building Release Archive Library libstp_constantbv.a
make[2]: Leaving directory `/home/ct/klee/klee_sources/stp/constantbv'
make[2]: Entering directory `/home/ct/klee/klee_sources/stp/sat'
llvm[2]: Compiling Simplifier.cpp for Release build
llvm[2]: Compiling Solver.cpp for Release build
llvm[2]: Building Release Archive Library libstp_sat.a
make[2]: Leaving directory `/home/ct/klee/klee_sources/stp/sat'
make[2]: Entering directory `/home/ct/klee/klee_sources/stp/simplifier'
llvm[2]: Compiling bvsolver.cpp for Release build
llvm[2]: Compiling simplifier.cpp for Release build
llvm[2]: Building Release Archive Library libstp_simplifier.a
make[2]: Leaving directory `/home/ct/klee/klee_sources/stp/simplifier'
make[1]: Leaving directory `/home/ct/klee/klee_sources/stp'
make[1]: Entering directory `/home/ct/klee/klee_sources/tools'
make[2]: Entering directory `/home/ct/klee/klee_sources/tools/klee'
llvm[2]: Compiling Debug.cpp for Release build
llvm[2]: Compiling main.cpp for Release build
llvm[2]: Linking Release executable klee (without symbols)
llvm[2]: ======= Finished Linking Release Executable klee (without symbols)
make[2]: Leaving directory `/home/ct/klee/klee_sources/tools/klee'
make[2]: Entering directory `/home/ct/klee/klee_sources/tools/kleaver'
llvm[2]: Compiling main.cpp for Release build
llvm[2]: Linking Release executable kleaver (without symbols)
llvm[2]: ======= Finished Linking Release Executable kleaver (without symbols)
make[2]: Leaving directory `/home/ct/klee/klee_sources/tools/kleaver'
make[2]: Entering directory `/home/ct/klee/klee_sources/tools/ktest-tool'
llvm[2]: Copying Release script ktest-tool
make[2]: Leaving directory `/home/ct/klee/klee_sources/tools/ktest-tool'
make[2]: Entering directory `/home/ct/klee/klee_sources/tools/gen-random-bout'
llvm[2]: Compiling gen-random-bout.cpp for Release build
llvm[2]: Linking Release executable gen-random-bout (without symbols)
llvm[2]: ======= Finished Linking Release Executable gen-random-bout (without
symbols)
make[2]: Leaving directory `/home/ct/klee/klee_sources/tools/gen-random-bout'
make[2]: Entering directory `/home/ct/klee/klee_sources/tools/klee-stats'
llvm[2]: Copying Release script klee-stats
make[2]: Leaving directory `/home/ct/klee/klee_sources/tools/klee-stats'
make[2]: Entering directory `/home/ct/klee/klee_sources/tools/klee-replay'
llvm[2]: Compiling fd_init.c for Release build
llvm[2]: Compiling file-creator.c for Release build
llvm[2]: Compiling klee-replay.c for Release build
llvm[2]: Compiling klee_init_env.c for Release build
llvm[2]: Linking Release executable klee-replay (without symbols)
llvm[2]: ======= Finished Linking Release Executable klee-replay (without
symbols)
make[2]: Leaving directory `/home/ct/klee/klee_sources/tools/klee-replay'
make[1]: Leaving directory `/home/ct/klee/klee_sources/tools'
make[1]: Entering directory `/home/ct/klee/klee_sources/runtime'
make[2]: Entering directory `/home/ct/klee/klee_sources/runtime/Intrinsic'
llvm[2]: Compiling klee_div_zero_check.c for Release build (bytecode)
llvm[2]: Compiling klee_div_zero_check.ll to klee_div_zero_check.bc for Release
build (bytecode)
llvm[2]: Compiling klee_int.c for Release build (bytecode)
llvm[2]: Compiling klee_int.ll to klee_int.bc for Release build (bytecode)
llvm[2]: Compiling klee_range.c for Release build (bytecode)
llvm[2]: Compiling klee_range.ll to klee_range.bc for Release build (bytecode)
llvm[2]: Compiling memcpy.c for Release build (bytecode)
llvm[2]: Compiling memcpy.ll to memcpy.bc for Release build (bytecode)
llvm[2]: Compiling memmove.c for Release build (bytecode)
llvm[2]: Compiling memmove.ll to memmove.bc for Release build (bytecode)
llvm[2]: Compiling mempcpy.c for Release build (bytecode)
llvm[2]: Compiling mempcpy.ll to mempcpy.bc for Release build (bytecode)
llvm[2]: Compiling memset.c for Release build (bytecode)
llvm[2]: Compiling memset.ll to memset.bc for Release build (bytecode)
llvm[2]: Building Release Bytecode Archive libkleeRuntimeIntrinsic.bca
llvm[2]: Compiling klee_div_zero_check.c for Release build
llvm[2]: Compiling klee_int.c for Release build
llvm[2]: Compiling klee_range.c for Release build
llvm[2]: Compiling memcpy.c for Release build
llvm[2]: Compiling memmove.c for Release build
llvm[2]: Compiling mempcpy.c for Release build
llvm[2]: Compiling memset.c for Release build
llvm[2]: Building Release Archive Library libkleeRuntimeIntrinsic.a
make[2]: Leaving directory `/home/ct/klee/klee_sources/runtime/Intrinsic'
make[2]: Entering directory `/home/ct/klee/klee_sources/runtime/klee-libc'
llvm[2]: Compiling __cxa_atexit.c for Release build (bytecode)
llvm[2]: Compiling __cxa_atexit.ll to __cxa_atexit.bc for Release build
(bytecode)
llvm[2]: Compiling abort.c for Release build (bytecode)
llvm[2]: Compiling abort.ll to abort.bc for Release build (bytecode)
llvm[2]: Compiling atexit.c for Release build (bytecode)
llvm[2]: Compiling atexit.ll to atexit.bc for Release build (bytecode)
llvm[2]: Compiling atoi.c for Release build (bytecode)
llvm[2]: Compiling atoi.ll to atoi.bc for Release build (bytecode)
llvm[2]: Compiling calloc.c for Release build (bytecode)
llvm[2]: Compiling calloc.ll to calloc.bc for Release build (bytecode)
llvm[2]: Compiling htonl.c for Release build (bytecode)
llvm[2]: Compiling htonl.ll to htonl.bc for Release build (bytecode)
llvm[2]: Compiling klee-choose.c for Release build (bytecode)
llvm[2]: Compiling klee-choose.ll to klee-choose.bc for Release build (bytecode)
llvm[2]: Compiling memchr.c for Release build (bytecode)
llvm[2]: Compiling memchr.ll to memchr.bc for Release build (bytecode)
llvm[2]: Compiling memcmp.c for Release build (bytecode)
llvm[2]: Compiling memcmp.ll to memcmp.bc for Release build (bytecode)
llvm[2]: Compiling memcpy.c for Release build (bytecode)
llvm[2]: Compiling memcpy.ll to memcpy.bc for Release build (bytecode)
llvm[2]: Compiling memmove.c for Release build (bytecode)
llvm[2]: Compiling memmove.ll to memmove.bc for Release build (bytecode)
llvm[2]: Compiling mempcpy.c for Release build (bytecode)
llvm[2]: Compiling mempcpy.ll to mempcpy.bc for Release build (bytecode)
llvm[2]: Compiling memset.c for Release build (bytecode)
llvm[2]: Compiling memset.ll to memset.bc for Release build (bytecode)
llvm[2]: Compiling putchar.c for Release build (bytecode)
llvm[2]: Compiling putchar.ll to putchar.bc for Release build (bytecode)
llvm[2]: Compiling stpcpy.c for Release build (bytecode)
llvm[2]: Compiling stpcpy.ll to stpcpy.bc for Release build (bytecode)
llvm[2]: Compiling strcat.c for Release build (bytecode)
llvm[2]: Compiling strcat.ll to strcat.bc for Release build (bytecode)
llvm[2]: Compiling strchr.c for Release build (bytecode)
llvm[2]: Compiling strchr.ll to strchr.bc for Release build (bytecode)
llvm[2]: Compiling strcmp.c for Release build (bytecode)
llvm[2]: Compiling strcmp.ll to strcmp.bc for Release build (bytecode)
llvm[2]: Compiling strcoll.c for Release build (bytecode)
llvm[2]: Compiling strcoll.ll to strcoll.bc for Release build (bytecode)
llvm[2]: Compiling strcpy.c for Release build (bytecode)
llvm[2]: Compiling strcpy.ll to strcpy.bc for Release build (bytecode)
llvm[2]: Compiling strlen.c for Release build (bytecode)
llvm[2]: Compiling strlen.ll to strlen.bc for Release build (bytecode)
llvm[2]: Compiling strncmp.c for Release build (bytecode)
llvm[2]: Compiling strncmp.ll to strncmp.bc for Release build (bytecode)
llvm[2]: Compiling strncpy.c for Release build (bytecode)
llvm[2]: Compiling strncpy.ll to strncpy.bc for Release build (bytecode)
llvm[2]: Compiling strrchr.c for Release build (bytecode)
llvm[2]: Compiling strrchr.ll to strrchr.bc for Release build (bytecode)
llvm[2]: Compiling strtol.c for Release build (bytecode)
llvm[2]: Compiling strtol.ll to strtol.bc for Release build (bytecode)
llvm[2]: Compiling strtoul.c for Release build (bytecode)
llvm[2]: Compiling strtoul.ll to strtoul.bc for Release build (bytecode)
llvm[2]: Compiling tolower.c for Release build (bytecode)
llvm[2]: Compiling tolower.ll to tolower.bc for Release build (bytecode)
llvm[2]: Compiling toupper.c for Release build (bytecode)
llvm[2]: Compiling toupper.ll to toupper.bc for Release build (bytecode)
llvm[2]: Building Release Bytecode Archive libklee-libc.bca
llvm[2]: Compiling __cxa_atexit.c for Release build
llvm[2]: Compiling abort.c for Release build
llvm[2]: Compiling atexit.c for Release build
llvm[2]: Compiling atoi.c for Release build
llvm[2]: Compiling calloc.c for Release build
llvm[2]: Compiling htonl.c for Release build
llvm[2]: Compiling klee-choose.c for Release build
llvm[2]: Compiling memchr.c for Release build
llvm[2]: Compiling memcmp.c for Release build
llvm[2]: Compiling memcpy.c for Release build
llvm[2]: Compiling memmove.c for Release build
llvm[2]: Compiling mempcpy.c for Release build
llvm[2]: Compiling memset.c for Release build
llvm[2]: Compiling putchar.c for Release build
llvm[2]: Compiling stpcpy.c for Release build
llvm[2]: Compiling strcat.c for Release build
llvm[2]: Compiling strchr.c for Release build
llvm[2]: Compiling strcmp.c for Release build
llvm[2]: Compiling strcoll.c for Release build
llvm[2]: Compiling strcpy.c for Release build
llvm[2]: Compiling strlen.c for Release build
llvm[2]: Compiling strncmp.c for Release build
llvm[2]: Compiling strncpy.c for Release build
llvm[2]: Compiling strrchr.c for Release build
llvm[2]: Compiling strtol.c for Release build
llvm[2]: Compiling strtoul.c for Release build
llvm[2]: Compiling tolower.c for Release build
llvm[2]: Compiling toupper.c for Release build
llvm[2]: Building Release Archive Library libklee-libc.a
make[2]: Leaving directory `/home/ct/klee/klee_sources/runtime/klee-libc'
make[2]: Entering directory `/home/ct/klee/klee_sources/runtime/Runtest'
llvm[2]: Compiling intrinsics.c for Release build (PIC)
intrinsics.c: In function ?klee_choose?:
intrinsics.c:105: warning: format ?%ld? expects type ?long int?, but argument 3
has type ?uintptr_t?
intrinsics.c:105: warning: format ?%ld? expects type ?long int?, but argument 4
has type ?uintptr_t?
llvm[2]: Linking Release Shared Library kleeRuntest.so
llvm[2]: Building Release Archive Library libkleeRuntest.a
make[2]: Leaving directory `/home/ct/klee/klee_sources/runtime/Runtest'
make[2]: Entering directory `/home/ct/klee/klee_sources/runtime/POSIX'
llvm[2]: Compiling fd.c for Release build (bytecode)
llvm[2]: Compiling fd.ll to fd.bc for Release build (bytecode)
llvm[2]: Compiling fd_32.c for Release build (bytecode)
llvm[2]: Compiling fd_32.ll to fd_32.bc for Release build (bytecode)
llvm[2]: Compiling fd_64.c for Release build (bytecode)
llvm[2]: Compiling fd_64.ll to fd_64.bc for Release build (bytecode)
llvm[2]: Compiling fd_init.c for Release build (bytecode)
llvm[2]: Compiling fd_init.ll to fd_init.bc for Release build (bytecode)
llvm[2]: Compiling illegal.c for Release build (bytecode)
llvm[2]: Compiling illegal.ll to illegal.bc for Release build (bytecode)
llvm[2]: Compiling klee_init_env.c for Release build (bytecode)
llvm[2]: Compiling klee_init_env.ll to klee_init_env.bc for Release build
(bytecode)
llvm[2]: Compiling misc.c for Release build (bytecode)
llvm[2]: Compiling misc.ll to misc.bc for Release build (bytecode)
llvm[2]: Compiling selinux.c for Release build (bytecode)
llvm[2]: Compiling selinux.ll to selinux.bc for Release build (bytecode)
llvm[2]: Compiling stubs.c for Release build (bytecode)
llvm[2]: Compiling stubs.ll to stubs.bc for Release build (bytecode)
llvm[2]: Building Release Bytecode Archive libkleeRuntimePOSIX.bca
llvm[2]: Compiling fd.c for Release build
llvm[2]: Compiling fd_32.c for Release build
llvm[2]: Compiling fd_64.c for Release build
llvm[2]: Compiling fd_init.c for Release build
llvm[2]: Compiling illegal.c for Release build
llvm[2]: Compiling klee_init_env.c for Release build
llvm[2]: Compiling misc.c for Release build
llvm[2]: Compiling selinux.c for Release build
llvm[2]: Compiling stubs.c for Release build
llvm[2]: Building Release Archive Library libkleeRuntimePOSIX.a
make[2]: Leaving directory `/home/ct/klee/klee_sources/runtime/POSIX'
make[1]: Leaving directory `/home/ct/klee/klee_sources/runtime'
But make check fails again.
ct at ct-ubuntu:~/klee/klee_sources$ make check
llvm[0]: Running test suite
make[1]: Entering directory `/home/ct/klee/klee_sources/test'
Making a new site.exp file...
*** dejagnu not found. Make sure runtest is in your PATH, then reconfigure
llvm.
make[1]: Leaving directory `/home/ct/klee/klee_sources/test'
Then I run the simple code with KLEE, result shows that KLEE can not recognize
the function pow. So I think uclibc and posix do not work. Could you give some
advices to figure out this problem?
ct at ct-ubuntu:~/klee/klee_sources/examples/islower$ llvm-gcc --emit-llvm -c
-g demo1.c
ct at ct-ubuntu:~/klee/klee_sources/examples/islower$ klee demo1.o
KLEE: output directory = "klee-out-16"
KLEE: WARNING: undefined reference to function: pow
KLEE: WARNING: silently concretizing (reason: floating point) expression (Read
w8 0 arr1) to value 0 (/home/ct/klee/klee_sources/examples/islower/demo1.c:17)
KLEE: WARNING: calling external: pow(0, 4611686018427387904)
KLEE: done: total instructions = 32
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
Thank you very much!
Ting
Chen
University of Electronic Science and Technology of
China
2010-12-18
chenting19870201
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20101219/9fde51a6/attachment-0001.html
