Merge pull request #26 from delcypher/fix_divide_by_zero

Fixed bug where divide by zero bugs would only be detected once in a program

1 files changed, 8 insertions, 2 deletions

diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 5dbc8fb0..0e576415 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -158,7 +158,12 @@ namespace {
   CheckDivZero("check-div-zero", 
                cl::desc("Inject checks for division-by-zero"),
                cl::init(true));
-    
+
+  cl::opt<bool>
+  CheckOvershift("check-overshift",
+               cl::desc("Inject checks for overshift"),
+               cl::init(true));
+
   cl::opt<std::string>
   OutputDir("output-dir", 
             cl::desc("Directory to write results in (defaults to klee-out-N)"),
@@ -1251,7 +1256,8 @@ int main(int argc, char **argv, char **envp) {
 #endif
   Interpreter::ModuleOptions Opts(LibraryDir.c_str(),
                                   /*Optimize=*/OptimizeModule, 
-                                  /*CheckDivZero=*/CheckDivZero);
+                                  /*CheckDivZero=*/CheckDivZero,
+                                  /*CheckOvershift=*/CheckOvershift);
   
   switch (Libc) {
   case NoLibc: /* silence compiler warning */