about summary refs log tree commit diff homepage
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
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.
-rw-r--r--runtime/klee-libc/bcmp.c2
-rw-r--r--test/Runtime/klee-libc/bcmp.c21
2 files changed, 22 insertions, 1 deletions
diff --git a/runtime/klee-libc/bcmp.c b/runtime/klee-libc/bcmp.c
index 23e1c233..306523fb 100644
--- a/runtime/klee-libc/bcmp.c
+++ b/runtime/klee-libc/bcmp.c
@@ -11,7 +11,7 @@
 
 int bcmp(const void *s1, const void *s2, size_t n) {
   const unsigned char *p1 = s1, *p2 = s2;
-  while (--n != 0) {
+  while (n-- != 0) {
     if (*p1++ != *p2++)
       return 1;
   }
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;
+}