diff options
Diffstat (limited to 'tools/klee-replay/klee-replay.h')
-rw-r--r-- | tools/klee-replay/klee-replay.h | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/tools/klee-replay/klee-replay.h b/tools/klee-replay/klee-replay.h new file mode 100644 index 00000000..668b5e3e --- /dev/null +++ b/tools/klee-replay/klee-replay.h @@ -0,0 +1,28 @@ +//===-- klee-replay.h ------------------------------------------*- C++ -*--===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef __KLEE_REPLAY_H__ +#define __KLEE_REPLAY_H__ + +#define _LARGEFILE64_SOURCE +#define _FILE_OFFSET_BITS 64 + +// FIXME: This is a hack. +#include "../../runtime/POSIX/fd.h" +#include <sys/time.h> + +void replay_create_files(exe_file_system_t *exe_fs); + +void process_status(int status, + time_t elapsed, + const char *pfx) + __attribute__((noreturn)); + +#endif + |