Support Why3 in StandardCompiler

1 files changed, 24 insertions, 0 deletions

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;
 }