about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
authorMartinNowack <martin.nowack@gmail.com>2015-11-08 14:31:42 +0100
committerMartinNowack <martin.nowack@gmail.com>2015-11-08 14:31:42 +0100
commitb614e759ac24ceebfbdeabf32dd166dcc27dbc95 (patch)
treece65cecd4a953dac22626d5d623430792adcd987 /test
parent25a21e6b91be8524f3c4be7ae352acfe862cc4a4 (diff)
parenta801ac5dfef0533c3fc00a7dbfb630eccb0b8f30 (diff)
downloadklee-b614e759ac24ceebfbdeabf32dd166dcc27dbc95.tar.gz
Merge pull request #269 from MartinNowack/fix_srem
[STPBuilder] Generate SRrem expressions correctly
Diffstat (limited to 'test')
-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);
+}