Add analysis_exceptiont

Author: danpoe

src/util/exception_utils.cpp

@@ -60,18 +60,28 @@ incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont(
 {
 }
 
+std::string incorrect_goto_program_exceptiont::what() const
+{
+  return message + " (at: " + source_location.as_string() + ")";
+}
+
 unsupported_operation_exceptiont::unsupported_operation_exceptiont(
   std::string message)
   : message(std::move(message))
 {
 }
 
-std::string incorrect_goto_program_exceptiont::what() const
+std::string unsupported_operation_exceptiont::what() const
 {
-  return message + " (at: " + source_location.as_string() + ")";
+  return message;
 }
 
-std::string unsupported_operation_exceptiont::what() const
+analysis_exceptiont::analysis_exceptiont(std::string reason)
+  : reason(std::move(reason))
 {
-  return message;
+}
+
+std::string analysis_exceptiont::what() const
+{
+  return reason;
 }

src/util/exception_utils.h

@@ -107,4 +107,17 @@ class unsupported_operation_exceptiont : public cprover_exception_baset
   std::string message;
 };
 
+/// Thrown when an unexpected error occurs during the analysis (e.g., when the
+/// SAT solver returns an error)
+class analysis_exceptiont : public cprover_exception_baset
+{
+public:
+  explicit analysis_exceptiont(std::string reason);
+  std::string what() const override;
+
+private:
+  /// The reason this exception was generated.
+  std::string reason;
+};
+
 #endif // CPROVER_UTIL_EXCEPTION_UTILS_H