aboutsummaryrefslogtreecommitdiffhomepage
path: root/runtime/POSIX
diff options
context:
space:
mode:
Diffstat (limited to 'runtime/POSIX')
-rw-r--r--runtime/POSIX/fd.h1
-rw-r--r--runtime/POSIX/fd_init.c9
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);
}