diff options
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/Core/TerminationTypes.h | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h new file mode 100644 index 00000000..592cd3cb --- /dev/null +++ b/include/klee/Core/TerminationTypes.h @@ -0,0 +1,55 @@ +//===-- TerminationTypes.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_TERMINATIONTYPES_H +#define KLEE_TERMINATIONTYPES_H + +#include <cstdint> + +#define TERMINATION_TYPES \ + TTYPE(RUNNING, 0U, "") \ + TTYPE(Exit, 1U, "") \ + MARK(NORMAL, 1U) \ + TTYPE(Interrupted, 2U, "early") \ + TTYPE(MaxDepth, 3U, "early") \ + TTYPE(OutOfMemory, 4U, "early") \ + TTYPE(OutOfStackMemory, 5U, "early") \ + MARK(EARLY, 5U) \ + TTYPE(Solver, 8U, "solver.err") \ + MARK(SOLVERERR, 8U) \ + TTYPE(Abort, 10U, "abort.err") \ + TTYPE(Assert, 11U, "assert.err") \ + TTYPE(BadVectorAccess, 12U, "bad_vector_access.err") \ + TTYPE(Free, 13U, "free.err") \ + TTYPE(Model, 14U, "model.err") \ + TTYPE(Overflow, 15U, "overflow.err") \ + TTYPE(Ptr, 16U, "ptr.err") \ + TTYPE(ReadOnly, 17U, "read_only.err") \ + TTYPE(ReportError, 18U, "report_error.err") \ + MARK(PROGERR, 18U) \ + TTYPE(User, 23U, "user.err") \ + MARK(USERERR, 23U) \ + TTYPE(Execution, 25U, "exec.err") \ + TTYPE(External, 26U, "external.err") \ + MARK(EXECERR, 26U) \ + TTYPE(Replay, 27U, "") \ + TTYPE(Merge, 28U, "") \ + TTYPE(SilentExit, 29U, "") \ + MARK(END, 29U) + +///@brief Reason an ExecutionState got terminated. +enum class StateTerminationType : std::uint8_t { +#define TTYPE(N,I,S) N = (I), +#define MARK(N,I) N = (I), + TERMINATION_TYPES +#undef TTYPE +#undef MARK +}; + +#endif |