about summary refs log tree commit diff homepage
path: root/lib/Core
diff options
context:
space:
mode:
authorPavel <operasfantom@gmail.com>2022-01-18 17:47:50 +0530
committerCristian Cadar <c.cadar@imperial.ac.uk>2022-09-14 20:40:10 +0100
commit712745687c080e2607a7c7657af33b3791d90f41 (patch)
tree0b5fb2e05b1eb991151b93bed97910f3c7019e84 /lib/Core
parent4ccb533158d40e15db9e9f2ade9bb28c3f83f38e (diff)
downloadklee-712745687c080e2607a7c7657af33b3791d90f41.tar.gz
Introduce separate categories for different kinds of undefined behavior
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/Executor.cpp6
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,