Implemented runtime check for overshift (controllable with --check-overshift

command line argument).

Overshift is where a Shl, AShr or LShr has a shift width greater
than the bit width of the first operand. This is undefined behaviour
in LLVM so we report this as an error.

1 files changed, 8 insertions, 2 deletions

diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 92e4df67..7cd61788 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -148,7 +148,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)"),
@@ -1241,7 +1246,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 */