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.

2 files changed, 27 insertions, 11 deletions

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;
     }
   }
 }
diff --git a/test/Replay/libkleeruntest/replay_posix_runtime.c b/test/Replay/libkleeruntest/replay_posix_runtime.c
index 57f97dd0..70d8a1d9 100644
--- a/test/Replay/libkleeruntest/replay_posix_runtime.c
+++ b/test/Replay/libkleeruntest/replay_posix_runtime.c
@@ -1,6 +1,5 @@
 // REQUIRES: posix-runtime
 // FIXME: We need to fix a bug in libkleeRuntest
-// XFAIL: *
 // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --posix-runtime --search=dfs %t.bc