diff options
| author | Frank Busse <bb0xfb@gmail.com> | 2021-12-15 14:35:31 +0000 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2021-12-23 17:43:13 +0000 |
| commit | 799ab806509407f72249e6ef49fc44b185a3e81d (patch) | |
| tree | c95a60e940e687371f379c03447f6d5323218c18 /include | |
| parent | a38ee31b70101955f7360f1e077261daf43c3378 (diff) | |
| download | klee-799ab806509407f72249e6ef49fc44b185a3e81d.tar.gz | |
Introduce termination categories
Track all path terminations: esp. for debugging or visualising a persistent process tree (with or without full MoKlee integration) it is helpful to know the exact reason (StateTerminationType) why a path terminated.
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 |