Hi *Philip Guo, *
Recently I have been trying to apply KLEE to busybox and I got the error "inline assembly is unsupported". I saw your method that pretend like the inline assembly was an external call and simply return a fresh symbolic value and modified code in lib/Executor.cpp as you suggested. But when I build the klee, there is no declaration fo the function "Expr::getWidthForLLVMType" in the Expr.h. I used the the function"getWidthForLLVMType" in the Executor.h to replace it and build klee with some warning: make[1]: Entering directory `/home/wang/work/klee/lib' make[2]: Entering directory `/home/wang/work/klee/lib/Basic' make[2]: Nothing to be done for `all'. make[2]: Leaving directory `/home/wang/work/klee/lib/Basic' make[2]: Entering directory `/home/wang/work/klee/lib/Support' make[2]: Nothing to be done for `all'. make[2]: Leaving directory `/home/wang/work/klee/lib/Support' make[2]: Entering directory `/home/wang/work/klee/lib/Expr' make[2]: Nothing to be done for `all'. make[2]: Leaving directory `/home/wang/work/klee/lib/Expr' make[2]: Entering directory `/home/wang/work/klee/lib/Solver' make[2]: Nothing to be done for `all'. make[2]: Leaving directory `/home/wang/work/klee/lib/Solver' make[2]: Entering directory `/home/wang/work/klee/lib/Module' make[2]: Nothing to be done for `all'. make[2]: Leaving directory `/home/wang/work/klee/lib/Module' make[2]: Entering directory `/home/wang/work/klee/lib/Core' llvm[2]: Compiling Executor.cpp for Release+Asserts build llvm[2]: Compiling ExecutorTimers.cpp for Release+Asserts build llvm[2]: Compiling ExecutorUtil.cpp for Release+Asserts build llvm[2]: Compiling ImpliedValue.cpp for Release+Asserts build llvm[2]: Compiling Memory.cpp for Release+Asserts build llvm[2]: Compiling MemoryManager.cpp for Release+Asserts build llvm[2]: Compiling PTree.cpp for Release+Asserts build llvm[2]: Compiling Searcher.cpp for Release+Asserts build llvm[2]: Compiling SeedInfo.cpp for Release+Asserts build llvm[2]: Compiling SpecialFunctionHandler.cpp for Release+Asserts build llvm[2]: Compiling StatsTracker.cpp for Release+Asserts build StatsTracker.cpp: In constructor 'klee::StatsTracker::StatsTracker(klee::Executor&, std::string, bool)': StatsTracker.cpp:180: warning: 'bool llvm::sys::Path::isAbsolute() const' is deprecated (declared at /home/wang/work/llvm-2.9/include/llvm/Support/PathV1.h:315) StatsTracker.cpp:183: warning: 'bool llvm::sys::Path::exists() const' is deprecated (declared at /home/wang/work/llvm-2.9/include/llvm/Support/PathV1.h:383) llvm[2]: Compiling TimingSolver.cpp for Release+Asserts build llvm[2]: Compiling UserSearcher.cpp for Release+Asserts build llvm[2]: Building Release+Asserts Archive Library libkleeCore.a make[2]: Leaving directory `/home/wang/work/klee/lib/Core' make[1]: Leaving directory `/home/wang/work/klee/lib' make[1]: Entering directory `/home/wang/work/klee/tools' make[2]: Entering directory `/home/wang/work/klee/tools/klee' llvm[2]: Compiling Debug.cpp for Release+Asserts build llvm[2]: Compiling main.cpp for Release+Asserts build main.cpp: In constructor 'KleeHandler::KleeHandler(int, char**)': main.cpp:306: warning: 'bool llvm::sys::Path::isAbsolute() const' is deprecated (declared at /home/wang/work/llvm-2.9/include/llvm/Support/PathV1.h:315) main.cpp: In function 'void parseArguments(int, char**)': main.cpp:603: warning: cast from type 'const char**' to type 'char**' casts away constness llvm[2]: Linking Release+Asserts executable klee (without symbols) /home/wang/work/llvm-2.9/Release+Asserts/lib/libLLVMipa.a(CallGraphSCCPass.o): In function `(anonymous namespace)::CGPassManager::runOnModule(llvm::Module&)': CallGraphSCCPass.cpp:(.text+0x1e61): warning: memset used with constant zero length parameter; this could be due to transposed parameters llvm[2]: ======= Finished Linking Release+Asserts Executable klee (without symbols) make[2]: Leaving directory `/home/wang/work/klee/tools/klee' make[2]: Entering directory `/home/wang/work/klee/tools/kleaver' llvm[2]: Compiling main.cpp for Release+Asserts build llvm[2]: Linking Release+Asserts executable kleaver (without symbols) llvm[2]: ======= Finished Linking Release+Asserts Executable kleaver (without symbols) make[2]: Leaving directory `/home/wang/work/klee/tools/kleaver' make[2]: Entering directory `/home/wang/work/klee/tools/ktest-tool' make[2]: Nothing to be done for `all'. make[2]: Leaving directory `/home/wang/work/klee/tools/ktest-tool' make[2]: Entering directory `/home/wang/work/klee/tools/gen-random-bout' llvm[2]: Linking Release+Asserts executable gen-random-bout (without symbols) llvm[2]: ======= Finished Linking Release+Asserts Executable gen-random-bout (without symbols) make[2]: Leaving directory `/home/wang/work/klee/tools/gen-random-bout' make[2]: Entering directory `/home/wang/work/klee/tools/klee-stats' make[2]: Nothing to be done for `all'. make[2]: Leaving directory `/home/wang/work/klee/tools/klee-stats' make[2]: Entering directory `/home/wang/work/klee/tools/klee-replay' llvm[2]: Linking Release+Asserts executable klee-replay (without symbols) llvm[2]: ======= Finished Linking Release+Asserts Executable klee-replay (without symbols) make[2]: Leaving directory `/home/wang/work/klee/tools/klee-replay' make[1]: Leaving directory `/home/wang/work/klee/tools' make[1]: Entering directory `/home/wang/work/klee/runtime' make[2]: Entering directory `/home/wang/work/klee/runtime/Intrinsic' make[2]: Nothing to be done for `all'. make[2]: Leaving directory `/home/wang/work/klee/runtime/Intrinsic' make[2]: Entering directory `/home/wang/work/klee/runtime/klee-libc' make[2]: Nothing to be done for `all'. make[2]: Leaving directory `/home/wang/work/klee/runtime/klee-libc' make[2]: Entering directory `/home/wang/work/klee/runtime/Runtest' llvm[2]: Linking Release+Asserts Shared Library libkleeRuntest.so make[2]: Leaving directory `/home/wang/work/klee/runtime/Runtest' make[2]: Entering directory `/home/wang/work/klee/runtime/POSIX' make[2]: Nothing to be done for `all'. make[2]: Leaving directory `/home/wang/work/klee/runtime/POSIX' make[1]: Leaving directory `/home/wang/work/klee/runtime' Am I right? If not, could you tell me the difference of these two functions?
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
