diff options
Diffstat (limited to 'tools')
-rw-r--r-- | tools/klee/main.cpp | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index cc9d0943..f55a9614 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -156,6 +156,11 @@ namespace { cl::desc("Optimize the code before execution (default=false)."), cl::init(false), cl::cat(StartCat)); + + cl::opt<bool> + WarnAllExternals("warn-all-external-symbols", + cl::desc("Issue a warning on startup for all external symbols (default=false)."), + cl::cat(StartCat)); /*** Linking options ***/ @@ -211,9 +216,7 @@ namespace { cl::init(true), cl::cat(ChecksCat)); - cl::opt<bool> - WarnAllExternals("warn-all-externals", - cl::desc("Give initial warning for all externals (default=false).")); + cl::opt<bool> OptExitOnError("exit-on-error", @@ -794,6 +797,7 @@ static const char *modelledExternals[] = { "__ubsan_handle_mul_overflow", "__ubsan_handle_divrem_overflow", }; + // Symbols we aren't going to warn about static const char *dontCareExternals[] = { #if 0 @@ -842,17 +846,19 @@ static const char *dontCareExternals[] = { "__isnan", "__signbit", }; + // Extra symbols we aren't going to warn about with klee-libc static const char *dontCareKlee[] = { "__ctype_b_loc", "__ctype_get_mb_cur_max", - // io system calls + // I/O system calls "open", "write", "read", "close", }; + // Extra symbols we aren't going to warn about with uclibc static const char *dontCareUclibc[] = { "__dso_handle", @@ -862,6 +868,7 @@ static const char *dontCareUclibc[] = { "printf", "vprintf" }; + // Symbols we consider unsafe static const char *unsafeExternals[] = { "fork", // oh lord @@ -870,6 +877,7 @@ static const char *unsafeExternals[] = { "raise", // yeah "kill", // mmmhmmm }; + #define NELEMS(array) (sizeof(array)/sizeof(array[0])) void externalsAndGlobalsCheck(const llvm::Module *m) { std::map<std::string, bool> externals; @@ -913,6 +921,7 @@ void externalsAndGlobalsCheck(const llvm::Module *m) { } } } + for (Module::const_global_iterator it = m->global_begin(), ie = m->global_end(); it != ie; ++it) |