From 0ca2dc8176a08a0d4fcaa90807e770a5809d95cf Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Tue, 21 Mar 2023 20:32:09 +0000 Subject: Remove model_version from the POSIX runtime, as we have never used it. --- tools/klee-replay/file-creator.c | 2 +- tools/klee-replay/klee-replay.c | 25 ++++++------------------- 2 files changed, 7 insertions(+), 20 deletions(-) (limited to 'tools/klee-replay') 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++; } } } -- cgit 1.4.1