diff options
Diffstat (limited to 'runtime/POSIX')
-rw-r--r-- | runtime/POSIX/fd.h | 1 | ||||
-rw-r--r-- | runtime/POSIX/fd_init.c | 9 |
2 files changed, 0 insertions, 10 deletions
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); } |