about summary refs log tree commit diff homepage
path: root/test/Feature
diff options
context:
space:
mode:
authorMartin Nowack <martin.nowack@gmail.com>2015-08-09 12:14:39 +0200
committerMartin Nowack <martin@se.inf.tu-dresden.de>2015-09-22 22:37:55 +0200
commita801ac5dfef0533c3fc00a7dbfb630eccb0b8f30 (patch)
treec591187a2af65ec9182d7d1bbf678daaccc37143 /test/Feature
parente8fded10ccdaea3d9d72d178506d6aebb799394e (diff)
downloadklee-a801ac5dfef0533c3fc00a7dbfb630eccb0b8f30.tar.gz
[STPBuilder] Generate SRrem expressions correctly
The '%' operater in C is not Gauss Modulo
but remainder operations.

Using a negative number as right operand
can result in a negative number.

Fix appropriate SRem building

Note: MetaSMTlib implementation doesn't have that bug.
Diffstat (limited to 'test/Feature')
-rw-r--r--test/Feature/srem.c33
1 files changed, 33 insertions, 0 deletions
diff --git a/test/Feature/srem.c b/test/Feature/srem.c
new file mode 100644
index 00000000..f4fa8aa5
--- /dev/null
+++ b/test/Feature/srem.c
@@ -0,0 +1,33 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out -use-cex-cache=1 %t.bc
+// RUN: grep "KLEE: done: explored paths = 5" %t.klee-out/info
+// RUN: grep "KLEE: done: generated tests = 4" %t.klee-out/info
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv)
+{
+    int y;
+
+    klee_make_symbolic(&y, sizeof(y), "y");
+
+    // Test cases divisor is positive or negative
+    if (y >= 0) {
+      if (y < 2) {
+        // Two test cases generated taking this path, one for y == 0 and y ==1
+        assert(1 % y == 0);
+      } else {
+        assert(1 % y == 1);
+      }
+    } else {
+      if (y > -2) {
+        assert(1 % y == 0);
+      } else {
+        assert(1 % y == 1);
+      }
+    }
+
+    assert(0 % y == 0);
+    assert(-1 % y == -1);
+}