introduce an exception class for typechecking

This adds typecheckt::errort(), which is a class that designed to be thrown
as exception.  It offers streaming via << and a 'fluent API'-style
.with_location() method to set the source location.

Author: kroening

src/util/typecheck.cpp

@@ -44,5 +44,16 @@ bool typecheckt::typecheck_main()
     error() << e.get_reason() << messaget::eom;
   }
 
+  catch(const errort &e)
+  {
+    if(e.what().empty())
+      error();
+    else
+    {
+      error().source_location = e.source_location();
+      error() << e.what() << messaget::eom;
+    }
+  }
+
   return message_handler->get_message_count(messaget::M_ERROR)!=errors_before;
 }

src/util/typecheck.h

@@ -22,6 +22,38 @@ class typecheckt:public messaget
 
   virtual ~typecheckt() { }
 
+  class errort final
+  {
+  public:
+    std::string what() const
+    {
+      return message.str();
+    }
+
+    std::ostringstream &message_ostream()
+    {
+      return message;
+    }
+
+    errort with_location(source_locationt _location) &&
+    {
+      __location = std::move(_location);
+      return std::move(*this);
+    }
+
+    const source_locationt &source_location() const
+    {
+      return __location;
+    }
+
+  protected:
+    std::ostringstream message;
+    source_locationt __location = source_locationt::nil();
+
+    template <typename T>
+    friend errort operator<<(errort &&e, const T &);
+  };
+
 protected:
   // main function -- overload this one
   virtual void typecheck()=0;
@@ -31,4 +63,12 @@ class typecheckt:public messaget
   virtual bool typecheck_main();
 };
 
+/// add to the diagnostic information in the given typecheckt::errort exception
+template <typename T>
+typecheckt::errort operator<<(typecheckt::errort &&e, const T &message)
+{
+  e.message_ostream() << message;
+  return std::move(e);
+}
+
 #endif // CPROVER_UTIL_TYPECHECK_H