5 files changed, 31 insertions, 4 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index e3186bbf..325e28ab 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -288,10 +288,12 @@ cl::list<Executor::TerminateReason> ExitOnErrorType(
         clEnumValN(Executor::ReportError, "ReportError",
                    "klee_report_error called"),
         clEnumValN(Executor::User, "User", "Wrong klee_* functions invocation"),
+#ifdef SUPPORT_KLEE_EH_CXX
         clEnumValN(Executor::UncaughtException, "UncaughtException",
                    "Exception was not caught"),
         clEnumValN(Executor::UnexpectedException, "UnexpectedException",
                    "An unexpected exception was thrown"),
+#endif
         clEnumValN(Executor::Unhandled, "Unhandled",
                    "Unhandled instruction hit") KLEE_LLVM_CL_VAL_END),
     cl::ZeroOrMore,
@@ -441,8 +443,10 @@ const char *Executor::TerminateReasonNames[] = {
   [ ReadOnly ] = "readonly",
   [ ReportError ] = "reporterror",
   [ User ] = "user",
+#ifdef SUPPORT_KLEE_EH_CXX
   [ UncaughtException ] = "uncaught_exception",
   [ UnexpectedException ] = "unexpected_exception",
+#endif
   [ Unhandled ] = "xxx",
 };
 
@@ -1743,10 +1747,12 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
       break;
     }
 
+#ifdef SUPPORT_KLEE_EH_CXX
     case Intrinsic::eh_typeid_for: {
       bindLocal(ki, state, getEhTypeidFor(arguments.at(0)));
       break;
     }
+#endif
 
     case Intrinsic::vaend:
       // va_end is a noop for the interpreter.
@@ -2026,6 +2032,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         ++state.pc;
       }
 
+#ifdef SUPPORT_KLEE_EH_CXX
       if (ri->getFunction()->getName() == "_klee_eh_cxx_personality") {
         assert(dyn_cast<ConstantExpr>(result) &&
                "result from personality fn must be a concrete value");
@@ -2059,6 +2066,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         // never return normally from the personality fn
         break;
       }
+#endif // SUPPORT_KLEE_EH_CXX
 
       if (!isVoidReturn) {
         Type *t = caller->getType();
@@ -3152,6 +3160,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     terminateStateOnExecError(state, "Unexpected ShuffleVector instruction");
     break;
 
+#ifdef SUPPORT_KLEE_EH_CXX
   case Instruction::Resume: {
     auto *cui = dyn_cast_or_null<CleanupPhaseUnwindingInformation>(
         state.unwindingInformation.get());
@@ -3230,6 +3239,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
 
     break;
   }
+#endif // SUPPORT_KLEE_EH_CXX
 
   case Instruction::AtomicRMW:
     terminateStateOnExecError(state, "Unexpected Atomic instruction, should be "
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 1614a0f9..eb3417ae 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -110,8 +110,10 @@ public:
     ReadOnly,
     ReportError,
     User,
+#ifdef SUPPORT_KLEE_EH_CXX
     UncaughtException,
     UnexpectedException,
+#endif
     Unhandled,
   };
 
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index f101a085..27ca385c 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -18,6 +18,7 @@
 #include "StatsTracker.h"
 #include "TimingSolver.h"
 
+#include "klee/Config/config.h"
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/KModule.h"
 #include "klee/Solver/SolverCmdLine.h"
@@ -115,7 +116,11 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
   add("malloc", handleMalloc, true),
   add("memalign", handleMemalign, true),
   add("realloc", handleRealloc, true),
+
+#ifdef SUPPORT_KLEE_EH_CXX
   add("_klee_eh_Unwind_RaiseException_impl", handleEhUnwindRaiseExceptionImpl, false),
+  add("klee_eh_typeid_for", handleEhTypeid, true),
+#endif
 
   // operator delete[](void*)
   add("_ZdaPv", handleDeleteArray, false),
@@ -140,7 +145,6 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
   add("__ubsan_handle_sub_overflow", handleSubOverflow, false),
   add("__ubsan_handle_mul_overflow", handleMulOverflow, false),
   add("__ubsan_handle_divrem_overflow", handleDivRemOverflow, false),
-  add("klee_eh_typeid_for", handleEhTypeid, true),
 
 #undef addDNR
 #undef add
@@ -458,6 +462,7 @@ void SpecialFunctionHandler::handleMemalign(ExecutionState &state,
                         alignment);
 }
 
+#ifdef SUPPORT_KLEE_EH_CXX
 void SpecialFunctionHandler::handleEhUnwindRaiseExceptionImpl(
     ExecutionState &state, KInstruction *target,
     std::vector<ref<Expr>> &arguments) {
@@ -495,6 +500,7 @@ void SpecialFunctionHandler::handleEhTypeid(ExecutionState &state,
 
   executor.bindLocal(target, state, executor.getEhTypeidFor(arguments[0]));
 }
+#endif // SUPPORT_KLEE_EH_CXX
 
 void SpecialFunctionHandler::handleAssume(ExecutionState &state,
                             KInstruction *target,
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index 3db650d7..a9f7100d 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -10,6 +10,8 @@
 #ifndef KLEE_SPECIALFUNCTIONHANDLER_H
 #define KLEE_SPECIALFUNCTIONHANDLER_H
 
+#include "klee/Config/config.h"
+
 #include <iterator>
 #include <map>
 #include <vector>
@@ -109,8 +111,12 @@ namespace klee {
     HANDLER(handleDefineFixedObject);
     HANDLER(handleDelete);    
     HANDLER(handleDeleteArray);
-    HANDLER(handleExit);
+#ifdef SUPPORT_KLEE_EH_CXX
+    HANDLER(handleEhUnwindRaiseExceptionImpl);
+    HANDLER(handleEhTypeid);
+#endif
     HANDLER(handleErrnoLocation);
+    HANDLER(handleExit);
     HANDLER(handleFree);
     HANDLER(handleGetErrno);
     HANDLER(handleGetObjSize);
@@ -119,8 +125,6 @@ namespace klee {
     HANDLER(handleMakeSymbolic);
     HANDLER(handleMalloc);
     HANDLER(handleMemalign);
-    HANDLER(handleEhUnwindRaiseExceptionImpl);
-    HANDLER(handleEhTypeid);
     HANDLER(handleMarkGlobal);
     HANDLER(handleOpenMerge);
     HANDLER(handleCloseMerge);
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index cd93b3ec..eaec7722 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -364,6 +364,9 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) {
 #if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0)
       case Intrinsic::dbg_label:
 #endif
+#ifndef SUPPORT_KLEE_EH_CXX
+      case Intrinsic::eh_typeid_for:
+#endif
       case Intrinsic::exp2:
       case Intrinsic::exp:
       case Intrinsic::expect:
@@ -399,10 +402,12 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) {
         dirty = true;
         break;
 
+#ifdef SUPPORT_KLEE_EH_CXX
       case Intrinsic::eh_typeid_for: {
         // Don't lower this, we need it for exception handling
         break;
       }
+#endif
 
         // Warn about any unrecognized intrinsics.
       default: {