diff options
author | Pavel <operasfantom@gmail.com> | 2022-01-18 17:47:50 +0530 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2022-09-14 20:40:10 +0100 |
commit | 712745687c080e2607a7c7657af33b3791d90f41 (patch) | |
tree | 0b5fb2e05b1eb991151b93bed97910f3c7019e84 /lib/Core/Executor.cpp | |
parent | 4ccb533158d40e15db9e9f2ade9bb28c3f83f38e (diff) | |
download | klee-712745687c080e2607a7c7657af33b3791d90f41.tar.gz |
Introduce separate categories for different kinds of undefined behavior
Diffstat (limited to 'lib/Core/Executor.cpp')
-rw-r--r-- | lib/Core/Executor.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 6fad8830..157c1cc8 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -290,6 +290,12 @@ cl::list<StateTerminationType> ExitOnErrorType( "Write to read-only memory"), clEnumValN(StateTerminationType::ReportError, "ReportError", "klee_report_error called"), + clEnumValN(StateTerminationType::ImplicitConversion, "ImplicitConversion", + "Undefined implicit conversion detected"), + clEnumValN(StateTerminationType::NullableAttribute, "NullableAttribute", + "Violation of nullable attribute detected"), + clEnumValN(StateTerminationType::UndefinedBehavior, "UndefinedBehavior", + "Undefined behavior detected"), clEnumValN(StateTerminationType::User, "User", "Wrong klee_* functions invocation")), cl::ZeroOrMore, |