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, 31 insertions, 0 deletions

diff --git a/runtime/Intrinsic/klee_overshift_check.c b/runtime/Intrinsic/klee_overshift_check.c
new file mode 100644
index 00000000..c0cb6102
--- /dev/null
+++ b/runtime/Intrinsic/klee_overshift_check.c
@@ -0,0 +1,31 @@
+//===-- klee_overshift_check.c ---------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <klee/klee.h>
+
+/* This instrumentation call is used to check for overshifting.
+ * If we do try to do x << y or x >> y
+ * where
+ *   bitWidth = sizeof(x)*8
+ *   shift = y
+ *
+ * then we can detect overshifting (which has undefined behaviour).
+ */
+void klee_overshift_check(unsigned long long bitWidth, unsigned long long shift) {
+  if (shift >= bitWidth) {
+    /* Maybe we shouldn't throw an error because
+     * overshifting can be non-fatal? Perhaps
+     * we should generate a test case but carry
+     * on executing the state with a warning?
+     */
+    klee_report_error("IGNORED", 0 /*Ignored */, "overshift error", "overshift.err");
+  }
+}
+
+