From aa0776d5e806be8f10ebcc21210ed25290c33598 Mon Sep 17 00:00:00 2001
From: Alex Beregszaszi <alex@rtfs.hu>
Date: Tue, 11 Apr 2017 09:43:30 +0100
Subject: Support Why3 in StandardCompiler

---
 libsolidity/interface/StandardCompiler.cpp | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

(limited to 'libsolidity/interface/StandardCompiler.cpp')

diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp
index 8fffea8e..a2909fa3 100644
--- a/libsolidity/interface/StandardCompiler.cpp
+++ b/libsolidity/interface/StandardCompiler.cpp
@@ -337,6 +337,30 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
 	}
 	output["contracts"] = contractsOutput;
 
+	{
+		ErrorList formalErrors;
+		if (m_compilerStack.prepareFormalAnalysis(&formalErrors))
+			output["why3"] = m_compilerStack.formalTranslation();
+
+		for (auto const& error: formalErrors)
+		{
+			auto err = dynamic_pointer_cast<Error const>(error);
+
+			errors.append(formatErrorWithException(
+				*error,
+				err->type() == Error::Type::Warning,
+				err->typeName(),
+				"general",
+				"",
+				scannerFromSourceName
+			));
+		}
+
+		// FIXME!!
+		if (!formalErrors.empty())
+			output["errors"] = errors;
+	}
+
 	return output;
 }
 
-- 
cgit