Remove model_version from the POSIX runtime, as we have never used it.

2 files changed, 7 insertions, 20 deletions

diff --git a/tools/klee-replay/file-creator.c b/tools/klee-replay/file-creator.c
index a1685a02..5e848964 100644
--- a/tools/klee-replay/file-creator.c
+++ b/tools/klee-replay/file-creator.c
@@ -301,7 +301,7 @@ static int create_reg_file(const char *fname, exe_disk_file_t *dfile,
   fprintf(stderr, "KLEE-REPLAY: NOTE: Creating file %s of length %d\n", fname, flen);
 
   // Open in RDWR just in case we have to end up using this fd.
-  if (__exe_env.version == 0 && mode == 0)
+  if (mode == 0)
     mode = 0644;
 
   int fd = open(fname, O_CREAT | O_RDWR, mode);
diff --git a/tools/klee-replay/klee-replay.c b/tools/klee-replay/klee-replay.c
index 72eeb17e..82c638c2 100644
--- a/tools/klee-replay/klee-replay.c
+++ b/tools/klee-replay/klee-replay.c
@@ -466,30 +466,17 @@ void klee_posix_prefer_cex(void *buffer, uintptr_t condition) {
 }
 
 void klee_make_symbolic(void *addr, size_t nbytes, const char *name) {
-  /* XXX remove model version code once new tests gen'd */
   if (obj_index >= input->numObjects) {
-    if (strcmp("model_version", name) == 0) {
-      assert(nbytes == 4);
-      *((int*) addr) = 0;
-    } else {
       __emit_error("ran out of appropriate inputs");
-    }
   } else {
     KTestObject *boo = &input->objects[obj_index];
-
-    if (strcmp("model_version", name) == 0 &&
-        strcmp("model_version", boo->name) != 0) {
-      assert(nbytes == 4);
-      *((int*) addr) = 0;
+    if (boo->numBytes != nbytes) {
+      fprintf(stderr, "KLEE-REPLAY: ERROR: make_symbolic mismatch, different sizes: "
+              "%d in input file, %lu in code\n", boo->numBytes, (unsigned long)nbytes);
+      exit(1);
     } else {
-      if (boo->numBytes != nbytes) {
-        fprintf(stderr, "KLEE-REPLAY: ERROR: make_symbolic mismatch, different sizes: "
-           "%d in input file, %lu in code\n", boo->numBytes, (unsigned long)nbytes);
-        exit(1);
-      } else {
-        memcpy(addr, boo->bytes, nbytes);
-        obj_index++;
-      }
+      memcpy(addr, boo->bytes, nbytes);
+      obj_index++;
     }
   }
 }