diff options
| author | Frank Busse <bb0xfb@gmail.com> | 2022-01-11 09:09:44 +0000 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-03-23 17:41:08 +0000 |
| commit | 3a1965c62540ef3fa3ec857f2b7d055cbbb68939 (patch) | |
| tree | 09dc3af2c442bbae80331b9a968d9d8f83558384 /include | |
| parent | a6f0612026cac27a1c997517420bfe5c9d254944 (diff) | |
| download | klee-3a1965c62540ef3fa3ec857f2b7d055cbbb68939.tar.gz | |
stats: add termination class stats
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/Core/TerminationTypes.h | 110 |
1 files changed, 72 insertions, 38 deletions
diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h index 4fe5583a..25e5ef4a 100644 --- a/include/klee/Core/TerminationTypes.h +++ b/include/klee/Core/TerminationTypes.h @@ -12,51 +12,85 @@ #include <cstdint> + +#define TERMINATION_CLASSES \ + TCLASS(Exit, 1U) \ + TCLASS(Early, 2U) \ + TCLASS(SolverError, 3U) \ + TCLASS(ProgramError, 4U) \ + TCLASS(UserError, 5U) \ + TCLASS(ExecutionError, 6U) \ + TCLASS(EarlyAlgorithm, 7U) \ + TCLASS(EarlyUser, 8U) + +///@brief Termination classes categorize termination types +enum class StateTerminationClass : std::uint8_t { + /// \cond DO_NOT_DOCUMENT + #define TCLASS(N,I) N = (I), + TERMINATION_CLASSES + /// \endcond +}; + + +// (Name, ID, file suffix) #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") \ - TTYPE(InvalidBuiltin, 19U, "invalid_builtin_use.err") \ - TTYPE(ImplicitTruncation, 20U, "implicit_truncation.err") \ - TTYPE(ImplicitConversion, 21U, "implicit_conversion.err") \ - TTYPE(UnreachableCall, 22U, "unreachable_call.err") \ - TTYPE(MissingReturn, 23U, "missing_return.err") \ - TTYPE(InvalidLoad, 24U, "invalid_load.err") \ - TTYPE(NullableAttribute, 25U, "nullable_attribute.err") \ - MARK(PROGERR, 25U) \ - TTYPE(User, 33U, "user.err") \ - MARK(USERERR, 33U) \ - TTYPE(Execution, 35U, "exec.err") \ - TTYPE(External, 36U, "external.err") \ - MARK(EXECERR, 36U) \ - TTYPE(Replay, 37U, "") \ - TTYPE(Merge, 38U, "") \ - TTYPE(SilentExit, 39U, "") \ - MARK(END, 39U) + TTMARK(EXIT, 1U) \ + TTYPE(Interrupted, 10U, "early") \ + TTYPE(MaxDepth, 11U, "early") \ + TTYPE(OutOfMemory, 12U, "early") \ + TTYPE(OutOfStackMemory, 13U, "early") \ + TTMARK(EARLY, 13U) \ + TTYPE(Solver, 20U, "solver.err") \ + TTMARK(SOLVERERR, 20U) \ + TTYPE(Abort, 30U, "abort.err") \ + TTYPE(Assert, 31U, "assert.err") \ + TTYPE(BadVectorAccess, 32U, "bad_vector_access.err") \ + TTYPE(Free, 33U, "free.err") \ + TTYPE(Model, 34U, "model.err") \ + TTYPE(Overflow, 35U, "overflow.err") \ + TTYPE(Ptr, 36U, "ptr.err") \ + TTYPE(ReadOnly, 37U, "read_only.err") \ + TTYPE(ReportError, 38U, "report_error.err") \ + TTYPE(InvalidBuiltin, 39U, "invalid_builtin_use.err") \ + TTYPE(ImplicitTruncation, 40U, "implicit_truncation.err") \ + TTYPE(ImplicitConversion, 41U, "implicit_conversion.err") \ + TTYPE(UnreachableCall, 42U, "unreachable_call.err") \ + TTYPE(MissingReturn, 43U, "missing_return.err") \ + TTYPE(InvalidLoad, 44U, "invalid_load.err") \ + TTYPE(NullableAttribute, 45U, "nullable_attribute.err") \ + TTMARK(PROGERR, 45U) \ + TTYPE(User, 50U, "user.err") \ + TTMARK(USERERR, 50U) \ + TTYPE(Execution, 60U, "exec.err") \ + TTYPE(External, 61U, "external.err") \ + TTMARK(EXECERR, 61U) \ + TTYPE(Replay, 70U, "") \ + TTYPE(Merge, 71U, "") \ + TTMARK(EARLYALGORITHM, 71U) \ + TTYPE(SilentExit, 80U, "") \ + TTMARK(EARLYUSER, 80U) \ + TTMARK(END, 80U) + ///@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), + /// \cond DO_NOT_DOCUMENT + #define TTYPE(N,I,S) N = (I), + #define TTMARK(N,I) N = (I), TERMINATION_TYPES -#undef TTYPE -#undef MARK + /// \endcond }; + +// reset definitions + +#undef TCLASS +#undef TTYPE +#undef TTMARK +#define TCLASS(N,I) +#define TTYPE(N,I,S) +#define TTMARK(N,I) + #endif |