From 712745687c080e2607a7c7657af33b3791d90f41 Mon Sep 17 00:00:00 2001 From: Pavel Date: Tue, 18 Jan 2022 17:47:50 +0530 Subject: Introduce separate categories for different kinds of undefined behavior --- lib/Core/Executor.cpp | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'lib/Core') 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 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, -- cgit 1.4.1