diff options
author | Omer Anson <oaanson@gmail.com> | 2016-02-22 23:13:34 +0200 |
---|---|---|
committer | Omer Anson <oaanson@gmail.com> | 2016-02-25 20:52:39 +0200 |
commit | 66f53aac10962db150aec07b96f3b0a756eef28b (patch) | |
tree | bd9c2a0a225ebdd3a475158c4004b8a51f78f030 /tools | |
parent | f76b6c5fe0ce8920ee6edb13802f857dae49e785 (diff) | |
download | klee-66f53aac10962db150aec07b96f3b0a756eef28b.tar.gz |
Added support to load libraries from command line
This allows a user to invoke klee with specific libraries to load from command line. This is an attempt to allow klee to run on applications linked to external libraries. The libraries still have to be compiled specially for klee, in a manner similar to klee-uclibc, i.e. archives (build with llvm-ar) of llvm IR files.
Diffstat (limited to 'tools')
-rw-r--r-- | tools/klee/main.cpp | 13 |
1 files changed, 13 insertions, 0 deletions
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); |