2 files changed, 20 insertions, 26 deletions

diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp
index 77d3c217..fecab2de 100644
--- a/libsolidity/formal/Why3Translator.cpp
+++ b/libsolidity/formal/Why3Translator.cpp
@@ -32,7 +32,7 @@ bool Why3Translator::process(SourceUnit const& _source)
 	try
 	{
 		if (m_lines.size() != 1 || !m_lines.back().contents.empty())
-			fatalError(_source, "Multiple source units not yet supported");
+			fatalError(_source, string("Multiple source units not yet supported"));
 		appendPreface();
 		_source.accept(*this);
 	}
@@ -55,22 +55,6 @@ string Why3Translator::translation() const
 	return result;
 }
 
-void Why3Translator::error(ASTNode const& _node, string const& _description)
-{
-	auto err = make_shared<Error>(Error::Type::Why3TranslatorError);
-	*err <<
-		errinfo_sourceLocation(_node.location()) <<
-		errinfo_comment(_description);
-	m_errors.push_back(err);
-	m_errorOccured = true;
-}
-
-void Why3Translator::fatalError(ASTNode const& _node, string const& _description)
-{
-	error(_node, _description);
-	BOOST_THROW_EXCEPTION(FatalError());
-}
-
 string Why3Translator::toFormalType(Type const& _type) const
 {
 	if (_type.category() == Type::Category::Bool)
@@ -900,3 +884,15 @@ module Address
 end
    )", 0});
 }
+
+void Why3Translator::error(ASTNode const& _source, std::string const& _description)
+{
+	m_errorOccured = true;
+	m_errorReporter.why3TranslatorError(_source, _description);
+}
+void Why3Translator::fatalError(ASTNode const& _source, std::string const& _description)
+{
+	m_errorOccured = true;
+	m_errorReporter.fatalWhy3TranslatorError(_source, _description);
+}
+
diff --git a/libsolidity/formal/Why3Translator.h b/libsolidity/formal/Why3Translator.h
index 03f3bf9c..b48317be 100644
--- a/libsolidity/formal/Why3Translator.h
+++ b/libsolidity/formal/Why3Translator.h
@@ -23,7 +23,7 @@
 #pragma once
 
 #include <libsolidity/ast/ASTVisitor.h>
-#include <libsolidity/interface/Exceptions.h>
+#include <libsolidity/interface/ErrorReporter.h>
 #include <string>
 
 namespace dev
@@ -43,7 +43,7 @@ class SourceUnit;
 class Why3Translator: private ASTConstVisitor
 {
 public:
-	Why3Translator(ErrorList& _errors): m_lines(std::vector<Line>{{std::string(), 0}}), m_errors(_errors) {}
+	Why3Translator(ErrorReporter& _errorReporter): m_lines(std::vector<Line>{{std::string(), 0}}), m_errorReporter(_errorReporter) {}
 
 	/// Appends formalisation of the given source unit to the output.
 	/// @returns false on error.
@@ -52,11 +52,6 @@ public:
 	std::string translation() const;
 
 private:
-	/// Creates an error and adds it to errors list.
-	void error(ASTNode const& _node, std::string const& _description);
-	/// Reports a fatal error and throws.
-	void fatalError(ASTNode const& _node, std::string const& _description);
-
 	/// Appends imports and constants use throughout the formal code.
 	void appendPreface();
 
@@ -65,6 +60,9 @@ private:
 	using errinfo_noFormalTypeFrom = boost::error_info<struct tag_noFormalTypeFrom, std::string /* name of the type that cannot be translated */ >;
 	struct NoFormalType: virtual Exception {};
 
+	void error(ASTNode const& _source, std::string const& _description);
+	void fatalError(ASTNode const& _source, std::string const& _description);
+
 	void indent() { newLine(); m_lines.back().indentation++; }
 	void unindent();
 	void addLine(std::string const& _line);
@@ -98,7 +96,7 @@ private:
 
 	virtual bool visitNode(ASTNode const& _node) override
 	{
-		error(_node, "Code not supported for formal verification.");
+		m_errorReporter.why3TranslatorError(_node, "Code not supported for formal verification.");
 		return false;
 	}
 
@@ -142,7 +140,7 @@ private:
 		unsigned indentation;
 	};
 	std::vector<Line> m_lines;
-	ErrorList& m_errors;
+	ErrorReporter& m_errorReporter;
 };
 
 }