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

4 files changed, 7 insertions, 23 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++;
     }
   }
 }
diff --git a/tools/ktest-gen/ktest-gen.cpp b/tools/ktest-gen/ktest-gen.cpp
index 331ff7b1..d127c0e5 100644
--- a/tools/ktest-gen/ktest-gen.cpp
+++ b/tools/ktest-gen/ktest-gen.cpp
@@ -303,8 +303,6 @@ int main(int argc, char *argv[]) {
   b.numArgs = argv_copy_idx;
   b.args = argv_copy;
 
-  push_range(&b, "model_version", 1);
-
   if (!kTest_toFile(&b, bout_file ? bout_file : "file.bout"))
     assert(0);
 
diff --git a/tools/ktest-randgen/ktest-randgen.cpp b/tools/ktest-randgen/ktest-randgen.cpp
index 9b7260eb..6146d35d 100644
--- a/tools/ktest-randgen/ktest-randgen.cpp
+++ b/tools/ktest-randgen/ktest-randgen.cpp
@@ -281,7 +281,6 @@ int main(int argc, char *argv[]) {
     push_random_obj(&b, "stdout", 1024, 1024);
     push_obj(&b, "stdout-stat", sizeof(struct stat), (unsigned char *)&s);
   }
-  push_range(&b, "model_version", 1);
 
   if (!kTest_toFile(&b, bout_file ? bout_file : "random.bout")) {
     error_exit("Error in storing data into random.bout\n");