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, 4 insertions, 2 deletions

diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h
index e29db411..e93284d6 100644
--- a/include/klee/Interpreter.h
+++ b/include/klee/Interpreter.h
@@ -51,11 +51,13 @@ public:
     std::string LibraryDir;
     bool Optimize;
     bool CheckDivZero;
+    bool CheckOvershift;
 
     ModuleOptions(const std::string& _LibraryDir, 
-                  bool _Optimize, bool _CheckDivZero)
+                  bool _Optimize, bool _CheckDivZero,
+                  bool _CheckOvershift)
       : LibraryDir(_LibraryDir), Optimize(_Optimize), 
-        CheckDivZero(_CheckDivZero) {}
+        CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift) {}
   };
 
   enum LogType