diff options
| author | chriseth <c@ethdev.com> | 2016-07-19 23:46:33 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2016-07-19 23:46:33 +0800 |
| commit | 427deb43f56e1dca5df31db22e9ee9df9c7b5182 (patch) | |
| tree | 072a13d7dfba888a51b7f339a9789eecbf78b01b | |
| parent | e10297a2efc5f8b37c7898391315eb7551522d4c (diff) | |
| parent | 9a9a815fc9953d820a330fc6ca515e367f4d97aa (diff) | |
| download | dexon-solidity-427deb43f56e1dca5df31db22e9ee9df9c7b5182.tar.gz dexon-solidity-427deb43f56e1dca5df31db22e9ee9df9c7b5182.tar.zst dexon-solidity-427deb43f56e1dca5df31db22e9ee9df9c7b5182.zip | |
Merge pull request #728 from chriseth/formalout
Provide formal version in json output.
| -rw-r--r-- | libsolidity/interface/CompilerStack.cpp | 6 | ||||
| -rw-r--r-- | libsolidity/interface/CompilerStack.h | 3 | ||||
| -rw-r--r-- | 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) { |