Merge pull request #274 from MartinNowack/fix_sdiv_1

Fix signed division by constant 1/ -1

1 files changed, 19 insertions, 0 deletions

diff --git a/test/regression/2015-08-30-sdiv-1.c b/test/regression/2015-08-30-sdiv-1.c
new file mode 100644
index 00000000..a90df308
--- /dev/null
+++ b/test/regression/2015-08-30-sdiv-1.c
@@ -0,0 +1,19 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out -exit-on-error -solver-optimize-divides=true %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out -exit-on-error -solver-optimize-divides=false %t.bc
+
+/* Division by constant can be optimized.using mul/shift
+ * For signed division, div by 1 or -1 cannot be optimized like that.
+ */
+#include <stdint.h>
+int main() {
+  int32_t dividend;
+  klee_make_symbolic(&dividend, sizeof dividend, "Dividend");
+  if ((3 ^ (dividend & 2)) / 1)
+    return 1;
+  if ((3 ^ (dividend & 2)) / -1)
+    return 1;
+  return 0;
+}