diff options
author | chriseth <chris@ethereum.org> | 2017-10-13 23:57:58 +0800 |
---|---|---|
committer | Leonardo Alt <leo@ethereum.org> | 2018-11-23 16:43:49 +0800 |
commit | 54bed454f6e7a53f51ec7e9bda7805900a2c8472 (patch) | |
tree | 87be069348deaac4cc526f227466adadec1d94de | |
parent | bb10be789c269927e593b41d37aa0637db68bbe1 (diff) | |
download | dexon-solidity-54bed454f6e7a53f51ec7e9bda7805900a2c8472.tar dexon-solidity-54bed454f6e7a53f51ec7e9bda7805900a2c8472.tar.gz dexon-solidity-54bed454f6e7a53f51ec7e9bda7805900a2c8472.tar.bz2 dexon-solidity-54bed454f6e7a53f51ec7e9bda7805900a2c8472.tar.lz dexon-solidity-54bed454f6e7a53f51ec7e9bda7805900a2c8472.tar.xz dexon-solidity-54bed454f6e7a53f51ec7e9bda7805900a2c8472.tar.zst dexon-solidity-54bed454f6e7a53f51ec7e9bda7805900a2c8472.zip |
Rename function and warn if responses are supplied for Z3.
-rw-r--r-- | libsolidity/formal/SMTPortfolio.cpp | 8 | ||||
-rw-r--r-- | libsolidity/interface/CompilerStack.h | 8 | ||||
-rw-r--r-- | libsolidity/interface/StandardCompiler.cpp | 4 |
3 files changed, 13 insertions, 7 deletions
diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp index 4c591380..515d6f32 100644 --- a/libsolidity/formal/SMTPortfolio.cpp +++ b/libsolidity/formal/SMTPortfolio.cpp @@ -41,7 +41,13 @@ SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses) m_solvers.emplace_back(make_shared<smt::CVC4Interface>()); #endif #if !defined (HAVE_Z3) && !defined (HAVE_CVC4) - m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses)), + m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses)); +#else + if (!_smtlib2Responses.empty()) + m_errorReporter.warning( + "Query responses for smtlib2 were given in the auxiliary input, " + "but this Solidity binary uses an SMT solver directly." + ); #endif (void)_smtlib2Responses; } diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h index 3fceed24..2c7add3b 100644 --- a/libsolidity/interface/CompilerStack.h +++ b/libsolidity/interface/CompilerStack.h @@ -156,10 +156,6 @@ public: /// Adds a response to an SMTLib2 query (identified by the hash of the query input). void addSMTLib2Response(h256 const& _hash, std::string const& _response) { m_smtlib2Responses[_hash] = _response; } - /// @returns a list of unhandled queries to the SMT solver (has to be supplied in a second run - /// by calling @a addSMTLib2Response. - std::vector<std::string> const& unhandledSMTQueries() const { return m_unhandledSMTLib2Queries; } - /// Parses all source units that were added /// @returns false on error. bool parse(); @@ -195,6 +191,10 @@ public: /// start line, start column, end line, end column std::tuple<int, int, int, int> positionFromSourceLocation(langutil::SourceLocation const& _sourceLocation) const; + /// @returns a list of unhandled queries to the SMT solver (has to be supplied in a second run + /// by calling @a addSMTLib2Response). + std::vector<std::string> const& unhandledSMTLib2Queries() const { return m_unhandledSMTLib2Queries; } + /// @returns a list of the contract names in the sources. std::vector<std::string> contractNames() const; diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index 59c28cd9..a3cb90b1 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -539,8 +539,8 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input) if (errors.size() > 0) output["errors"] = errors; - if (!m_compilerStack.unhandledSMTQueries().empty()) - for (string const& query: m_compilerStack.unhandledSMTQueries()) + if (!m_compilerStack.unhandledSMTLib2Queries().empty()) + for (string const& query: m_compilerStack.unhandledSMTLib2Queries()) output["auxiliaryInputRequested"]["smtlib2"]["0x" + keccak256(query).hex()] = query; output["sources"] = Json::objectValue; |