diff options
| -rw-r--r-- | test/Feature/LinkLLVMLib.c | 24 | ||||
| -rw-r--r-- | tools/klee/main.cpp | 13 |
2 files changed, 37 insertions, 0 deletions
diff --git a/test/Feature/LinkLLVMLib.c b/test/Feature/LinkLLVMLib.c new file mode 100644 index 00000000..7639bfef --- /dev/null +++ b/test/Feature/LinkLLVMLib.c @@ -0,0 +1,24 @@ +// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc -DLINK_LLVM_LIB_TEST_LIB +// RUN: llvm-ar r %t1.a %t1.bc +// +// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t2.bc -DLINK_LLVM_LIB_TEST_EXEC +// RUN: rm -rf %t.klee-out +// RUN: %klee --link-llvm-lib %t1.a --output-dir=%t.klee-out --emit-all-errors %t2.bc 2>&1 | FileCheck %s + +#ifdef LINK_LLVM_LIB_TEST_EXEC +extern void printint(int d); + +int main(int argc, char * argv[]) { + printint(5); + // CHECK: KLEE: WARNING ONCE: calling external: printf + return 0; +} +#endif + +#ifdef LINK_LLVM_LIB_TEST_LIB +#include <stdio.h> + +void printint(int d) { + printf("%d\n", d); +} +#endif diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 665cc842..0dfa4399 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -190,6 +190,11 @@ namespace { cl::list<std::string> SeedOutDir("seed-out-dir"); + cl::list<std::string> + LinkLibraries("link-llvm-lib", + cl::desc("Link the given libraries before execution"), + cl::value_desc("library file")); + cl::opt<unsigned> MakeConcreteSymbolic("make-concrete-symbolic", cl::desc("Probabilistic rate at which to make concrete reads symbolic, " @@ -1303,6 +1308,14 @@ int main(int argc, char **argv, char **envp) { assert(mainModule && "unable to link with simple model"); } + std::vector<std::string>::iterator libs_it; + std::vector<std::string>::iterator libs_ie; + for (libs_it = LinkLibraries.begin(), libs_ie = LinkLibraries.end(); + libs_it != libs_ie; ++libs_it) { + const char * libFilename = libs_it->c_str(); + klee_message("Linking in library: %s.\n", libFilename); + mainModule = klee::linkWithLibrary(mainModule, libFilename); + } // Get the desired main function. klee_main initializes uClibc // locale and other data and then calls main. Function *mainFn = mainModule->getFunction(EntryPoint); |