about summary refs log tree commit diff homepage
path: root/test/Runtime
diff options
context:
space:
mode:
authorAlastair Reid <adreid@google.com>2020-11-02 16:47:51 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2020-11-03 13:15:06 +0000
commitbef9f39d033ea5c9600f39af7cfd213e01aab4c1 (patch)
tree6e9e1ac2f03045850ddf0dcebb1706d7f8872844 /test/Runtime
parent909bca0e15282a56e3345850fb23a8f16c9e39e6 (diff)
downloadklee-bef9f39d033ea5c9600f39af7cfd213e01aab4c1.tar.gz
fix: bcmp with n==0
This was executing the loop when n==0 leading to an out of bound pointer
error.

Found while verifying Rust code that compares strings.
Diffstat (limited to 'test/Runtime')
-rw-r--r--test/Runtime/klee-libc/bcmp.c21
1 files changed, 21 insertions, 0 deletions
diff --git a/test/Runtime/klee-libc/bcmp.c b/test/Runtime/klee-libc/bcmp.c
new file mode 100644
index 00000000..d0f5d7e5
--- /dev/null
+++ b/test/Runtime/klee-libc/bcmp.c
@@ -0,0 +1,21 @@
+// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=klee %t1.bc
+
+// test bcmp for sizes including zero
+
+#include <assert.h>
+#include <stdlib.h>
+#include <strings.h>
+
+int main() {
+  for (int i = 0; i < 5; ++i) {
+    void *s = malloc(i);
+    if (s) {
+      klee_make_symbolic(s, i, "s");
+      assert(0 == bcmp(s, s, i));
+      free(s);
+    }
+  }
+  return 0;
+}