From 4b477f8108a2a92012ff138725f6c6f26ccb23e5 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 29 Aug 2013 17:30:33 +0100
Subject: 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.
---
 tools/klee/main.cpp | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'tools')

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 */
-- 
cgit 1.4.1