Provide formal version in json output.

3 files changed, 22 insertions, 3 deletions

diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index c28e926b..4776a4ce 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -253,9 +253,11 @@ void CompilerStack::link(const std::map<string, h160>& _libraries)
 	}
 }
 
-bool CompilerStack::prepareFormalAnalysis()
+bool CompilerStack::prepareFormalAnalysis(ErrorList* _errors)
 {
-	Why3Translator translator(m_errors);
+	if (!_errors)
+		_errors = &m_errors;
+	Why3Translator translator(*_errors);
 	for (Source const* source: m_sourceOrder)
 		if (!translator.process(*source->ast))
 			return false;
diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h
index e111c982..9d2aace4 100644
--- a/libsolidity/interface/CompilerStack.h
+++ b/libsolidity/interface/CompilerStack.h
@@ -124,8 +124,9 @@ public:
 	void link(std::map<std::string, h160> const& _libraries);
 
 	/// Tries to translate all source files into a language suitable for formal analysis.
+	/// @param _errors list to store errors - defaults to the internal error list.
 	/// @returns false on error.
-	bool prepareFormalAnalysis();
+	bool prepareFormalAnalysis(ErrorList* _errors = nullptr);
 	std::string const& formalTranslation() const { return m_formalTranslation; }
 
 	/// @returns the assembled object for a contract.
diff --git a/solc/jsonCompiler.cpp b/solc/jsonCompiler.cpp
index e8f674a0..bc1305c5 100644
--- a/solc/jsonCompiler.cpp
+++ b/solc/jsonCompiler.cpp
@@ -219,6 +219,22 @@ string compile(StringMap const& _sources, bool _optimize, CStyleReadFileCallback
 			output["contracts"][contractName] = contractData;
 		}
 
+		// Do not taint the internal error list
+		ErrorList formalErrors;
+		if (compiler.prepareFormalAnalysis(&formalErrors))
+			output["formal"]["why3"] = compiler.formalTranslation();
+		if (!formalErrors.empty())
+		{
+			Json::Value errors(Json::arrayValue);
+			for (auto const& error: formalErrors)
+				errors.append(formatError(
+					*error,
+					(error->type() == Error::Type::Warning) ? "Warning" : "Error",
+					scannerFromSourceName
+				));
+			output["formal"]["errors"] = errors;
+		}
+
 		output["sources"] = Json::Value(Json::objectValue);
 		for (auto const& source: _sources)
 		{