diff options
| author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-03-21 20:32:09 +0000 |
|---|---|---|
| committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2023-03-23 20:30:11 +0000 |
| commit | 0ca2dc8176a08a0d4fcaa90807e770a5809d95cf (patch) | |
| tree | 8d1d7972153c406f4c898571efa5865f60712bbb /runtime | |
| parent | 58d454647ff1465128423fa02896f84e5d3b989a (diff) | |
| download | klee-0ca2dc8176a08a0d4fcaa90807e770a5809d95cf.tar.gz | |
Remove model_version from the POSIX runtime, as we have never used it.
Diffstat (limited to 'runtime')
| -rw-r--r-- | runtime/POSIX/fd.h | 1 | ||||
| -rw-r--r-- | runtime/POSIX/fd_init.c | 9 | ||||
| -rw-r--r-- | runtime/Runtest/intrinsics.c | 7 |
3 files changed, 0 insertions, 17 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); } 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\"", |