From 6137888c07ab45bee354ff7b66f6f313ea158da8 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 14 Jan 2017 18:49:18 +0000
Subject: Fix bug reported privately by @danielschemmel .

If KLEE generates ktest files with `--posix-runtime` then if replaying
using libkleeRuntest then replay would be incorrect because the
`model_version` object would be unintentionally used during replay.

For now just skip over that object and try the next one.

Also emit a warning if the object names don't match.
---
 runtime/Runtest/intrinsics.c | 37 +++++++++++++++++++++++++++----------
 1 file changed, 27 insertions(+), 10 deletions(-)

(limited to 'runtime')

diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c
index 2302e278..d67f093e 100644
--- a/runtime/Runtest/intrinsics.c
+++ b/runtime/Runtest/intrinsics.c
@@ -80,16 +80,33 @@ void klee_make_symbolic(void *array, size_t nbytes, const char *name) {
     }
   }
 
-  if (testPosition >= testData->numObjects) {
-    fprintf(stderr, "ERROR: out of inputs, using zero\n");
-    memset(array, 0, nbytes);
-  } else {
-    KTestObject *o = &testData->objects[testPosition++];
-    memcpy(array, o->bytes, nbytes<o->numBytes ? nbytes : o->numBytes);
-    if (nbytes != o->numBytes) {
-      fprintf(stderr, "ERROR: object sizes differ\n");
-      if (o->numBytes < nbytes) 
-        memset((char*) array + o->numBytes, 0, nbytes - o->numBytes);
+  for (;; ++testPosition) {
+    if (testPosition >= testData->numObjects) {
+      fprintf(stderr, "ERROR: out of inputs, using zero\n");
+      memset(array, 0, nbytes);
+      break;
+    } else {
+      KTestObject *o = &testData->objects[testPosition];
+      if (strcmp("model_version", o->name) == 0 &&
+          strcmp("model_version", name) != 0) {
+        // Skip over this KTestObject because we've hit
+        // `model_version` which is from the POSIX runtime
+        // and the caller didn't ask for it.
+        continue;
+      }
+      if (strcmp(name, o->name) != 0) {
+        fprintf(stderr, "ERROR: object name mismatch. Requesting \"%s\" but "
+                        "returning \"%s\"",
+                name, o->name);
+      }
+      memcpy(array, o->bytes, nbytes < o->numBytes ? nbytes : o->numBytes);
+      if (nbytes != o->numBytes) {
+        fprintf(stderr, "ERROR: object sizes differ\n");
+        if (o->numBytes < nbytes)
+          memset((char *)array + o->numBytes, 0, nbytes - o->numBytes);
+      }
+      ++testPosition;
+      break;
     }
   }
 }
-- 
cgit 1.4.1