diff options
| -rw-r--r-- | runtime/POSIX/fd_init.c | 28 | ||||
| -rw-r--r-- | test/Runtime/POSIX/Replay.c | 45 | ||||
| -rw-r--r-- | test/lit.cfg | 7 |
3 files changed, 64 insertions, 16 deletions
diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c index 0cfa5788..327ddb53 100644 --- a/runtime/POSIX/fd_init.c +++ b/runtime/POSIX/fd_init.c @@ -74,20 +74,20 @@ static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size, reasonable. */ klee_assume((s->st_blksize & ~0xFFFF) == 0); - klee_posix_prefer_cex(s, !(s->st_mode & ~(S_IFMT | 0777))); - klee_posix_prefer_cex(s, s->st_dev == defaults->st_dev); - klee_posix_prefer_cex(s, s->st_rdev == defaults->st_rdev); - klee_posix_prefer_cex(s, (s->st_mode&0700) == 0600); - klee_posix_prefer_cex(s, (s->st_mode&0070) == 0040); - klee_posix_prefer_cex(s, (s->st_mode&0007) == 0004); - klee_posix_prefer_cex(s, (s->st_mode&S_IFMT) == S_IFREG); - klee_posix_prefer_cex(s, s->st_nlink == 1); - klee_posix_prefer_cex(s, s->st_uid == defaults->st_uid); - klee_posix_prefer_cex(s, s->st_gid == defaults->st_gid); - klee_posix_prefer_cex(s, s->st_blksize == 4096); - klee_posix_prefer_cex(s, s->st_atime == defaults->st_atime); - klee_posix_prefer_cex(s, s->st_mtime == defaults->st_mtime); - klee_posix_prefer_cex(s, s->st_ctime == defaults->st_ctime); + klee_prefer_cex(s, !(s->st_mode & ~(S_IFMT | 0777))); + klee_prefer_cex(s, s->st_dev == defaults->st_dev); + klee_prefer_cex(s, s->st_rdev == defaults->st_rdev); + klee_prefer_cex(s, (s->st_mode&0700) == 0600); + klee_prefer_cex(s, (s->st_mode&0070) == 0040); + klee_prefer_cex(s, (s->st_mode&0007) == 0004); + klee_prefer_cex(s, (s->st_mode&S_IFMT) == S_IFREG); + klee_prefer_cex(s, s->st_nlink == 1); + klee_prefer_cex(s, s->st_uid == defaults->st_uid); + klee_prefer_cex(s, s->st_gid == defaults->st_gid); + klee_prefer_cex(s, s->st_blksize == 4096); + klee_prefer_cex(s, s->st_atime == defaults->st_atime); + klee_prefer_cex(s, s->st_mtime == defaults->st_mtime); + klee_prefer_cex(s, s->st_ctime == defaults->st_ctime); s->st_size = dfile->size; s->st_blocks = 8; diff --git a/test/Runtime/POSIX/Replay.c b/test/Runtime/POSIX/Replay.c new file mode 100644 index 00000000..ba11f05f --- /dev/null +++ b/test/Runtime/POSIX/Replay.c @@ -0,0 +1,45 @@ +// RUN: %llvmgcc -DKLEE_EXECUTION %s -emit-llvm -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --posix-runtime %t.bc --sym-files 1 3 +// RUN: %klee-replay --create-files-only %t.klee-out/test000001.ktest + +// RUN: FileCheck --input-file=A --check-prefix=CREATE_FILES_ONLY %s +// CREATE_FILES_ONLY: abc + +// RUN: %cc %s -O0 -o %t2 +// RUN: %klee-replay %t2 %t.klee-out/test000001.ktest | FileCheck --check-prefix=REPLAY %s +// REPLAY: Yes + +#ifdef KLEE_EXECUTION +#define EXIT klee_silent_exit +#else +#define EXIT exit +#endif + +#include <sys/types.h> +#include <sys/stat.h> +#include <fcntl.h> +#include <unistd.h> +#include <assert.h> +#include <stdio.h> + +int main(int argc, char** argv) { + int fd, n; + char buf[1024]; + + fd = open("A", O_RDONLY); + assert(fd != -1); + n = read(fd, buf, 3); + assert(n == 3); + + /* Generate a single test, with the first three chars + in the file 'abc' */ + if (buf[0] == 'a' && buf[1] == 'b' && buf[2] == 'c') + printf("Yes\n"); + else + EXIT(0); + + return 0; +} + + diff --git a/test/lit.cfg b/test/lit.cfg index 6cb85712..00b429b6 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -133,9 +133,12 @@ if len(kleaver_extra_params) != 0: ) # Set absolute paths and extra cmdline args for KLEE's tools +# If a tool's name is a prefix of another, the longer name has +# to come first, e.g., klee-replay should come before klee subs = [ ('%kleaver', 'kleaver', kleaver_extra_params), - ('%klee','klee', klee_extra_params), - ('%ktest-tool', 'ktest-tool', '') + ('%klee-replay', 'klee-replay', ''), + ('%klee','klee', klee_extra_params), + ('%ktest-tool', 'ktest-tool', '') ] for s,basename,extra_args in subs: config.substitutions.append( |