From 0ca2dc8176a08a0d4fcaa90807e770a5809d95cf Mon Sep 17 00:00:00 2001
From: Cristian Cadar <c.cadar@imperial.ac.uk>
Date: Tue, 21 Mar 2023 20:32:09 +0000
Subject: Remove model_version from the POSIX runtime, as we have never used
 it.

---
 runtime/POSIX/fd.h           | 1 -
 runtime/POSIX/fd_init.c      | 9 ---------
 runtime/Runtest/intrinsics.c | 7 -------
 3 files changed, 17 deletions(-)

(limited to 'runtime')

diff --git a/runtime/POSIX/fd.h b/runtime/POSIX/fd.h
index 5fa42874..87d967ee 100644
--- a/runtime/POSIX/fd.h
+++ b/runtime/POSIX/fd.h
@@ -93,7 +93,6 @@ typedef struct {
 typedef struct {
   exe_file_t fds[MAX_FDS];
   mode_t umask; /* process umask */
-  unsigned version;
   /* If set, writes execute as expected.  Otherwise, writes extending
      the file size only change the contents up to the initial
      size. The file offset is always incremented correctly. */
diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c
index a8d557e7..a064e42b 100644
--- a/runtime/POSIX/fd_init.c
+++ b/runtime/POSIX/fd_init.c
@@ -36,7 +36,6 @@ exe_sym_env_t __exe_env = {
    { 1, eOpen | eWriteable, 0, 0}, 
    { 2, eOpen | eWriteable, 0, 0}},
   022,
-  0,
   0
 };
 
@@ -96,12 +95,6 @@ static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size,
   dfile->stat = s;
 }
 
-static unsigned __sym_uint32(const char *name) {
-  unsigned x;
-  klee_make_symbolic(&x, sizeof x, name);
-  return x;
-}
-
 /* n_files: number of symbolic input files, excluding stdin
    file_length: size in bytes of each symbolic file, including stdin
    sym_stdout_flag: 1 if stdout should be symbolic, 0 otherwise
@@ -168,6 +161,4 @@ void klee_init_fds(unsigned n_files, unsigned file_length,
   else __exe_fs.sym_stdout = NULL;
   
   __exe_env.save_all_writes = save_all_writes_flag;
-  __exe_env.version = __sym_uint32("model_version");
-  klee_assume(__exe_env.version == 1);
 }
diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c
index 2442db0c..18eb3cff 100644
--- a/runtime/Runtest/intrinsics.c
+++ b/runtime/Runtest/intrinsics.c
@@ -109,13 +109,6 @@ void klee_make_symbolic(void *array, size_t nbytes, const char *name) {
       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) {
         report_internal_error(
             "object name mismatch. Requesting \"%s\" but returning \"%s\"",
-- 
cgit 1.4.1