From 9a9a815fc9953d820a330fc6ca515e367f4d97aa Mon Sep 17 00:00:00 2001
From: chriseth <c@ethdev.com>
Date: Mon, 18 Jul 2016 18:16:22 +0200
Subject: Provide formal version in json output.
---
libsolidity/interface/CompilerStack.cpp | 6 ++++--
libsolidity/interface/CompilerStack.h | 3 ++-
solc/jsonCompiler.cpp | 16 ++++++++++++++++
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)
{
--
cgit v1.2.3