diff options
| author | Pavel <operasfantom@gmail.com> | 2022-07-04 15:43:52 +0400 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2022-09-14 20:40:10 +0100 |
| commit | 1ac45951a90c2eed70d5232d7cd794060c47162a (patch) | |
| tree | b3c8a6506ca60aea7cab1ed7bc987ae75369cb2c /lib/Core | |
| parent | d14b7dc335f1dc31a53602cee48f05e415edbfe5 (diff) | |
| download | klee-1ac45951a90c2eed70d5232d7cd794060c47162a.tar.gz | |
Eliminate .undefined_behavior.err category and simplify tests
Diffstat (limited to 'lib/Core')
| -rw-r--r-- | lib/Core/Executor.cpp | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 157c1cc8..1187654d 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -290,12 +290,24 @@ cl::list<StateTerminationType> ExitOnErrorType( "Write to read-only memory"), clEnumValN(StateTerminationType::ReportError, "ReportError", "klee_report_error called"), + clEnumValN(StateTerminationType::InvalidBuiltin, "InvalidBuiltin", + "Passing invalid value to compiler builtin"), + clEnumValN(StateTerminationType::ImplicitTruncation, "ImplicitTruncation", + "Implicit conversion from integer of larger bit width to " + "smaller bit width that results in data loss"), clEnumValN(StateTerminationType::ImplicitConversion, "ImplicitConversion", - "Undefined implicit conversion detected"), + "Implicit conversion between integer types that changes the " + "sign of the value"), + clEnumValN(StateTerminationType::UnreachableCall, "UnreachableCall", + "Control flow reached an unreachable program point"), + clEnumValN(StateTerminationType::MissingReturn, "MissingReturn", + "Reaching the end of a value-returning function without " + "returning a value"), + clEnumValN(StateTerminationType::InvalidLoad, "InvalidLoad", + "Load of a value which is not in the range of representable " + "values for that type"), 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, |