cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Rename function and warn if responses are supplied for Z3.

Browse Source
This commit is contained in:
chriseth 2017-10-13 17:57:58 +02:00 committed by Leonardo Alt
parent bb10be789c
commit 54bed454f6
3 changed files with 13 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libsolidity/formal/SMTPortfolio.cpp
View File

@ -41,7 +41,13 @@ SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
m_solvers.emplace_back(make_shared<smt::CVC4Interface>()); m_solvers.emplace_back(make_shared<smt::CVC4Interface>());
#endif #endif
#if !defined (HAVE_Z3) && !defined (HAVE_CVC4) #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 #endif
(void)_smtlib2Responses; (void)_smtlib2Responses;
} }

8
libsolidity/interface/CompilerStack.h
View File

@ -156,10 +156,6 @@ public:
/// Adds a response to an SMTLib2 query (identified by the hash of the query input). /// 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; } 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 /// Parses all source units that were added
/// @returns false on error. /// @returns false on error.
bool parse(); bool parse();
@ -195,6 +191,10 @@ public:
/// start line, start column, end line, end column /// start line, start column, end line, end column
std::tuple<int, int, int, int> positionFromSourceLocation(langutil::SourceLocation const& _sourceLocation) const; 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. /// @returns a list of the contract names in the sources.
std::vector<std::string> contractNames() const; std::vector<std::string> contractNames() const;

4
libsolidity/interface/StandardCompiler.cpp
View File

@ -539,8 +539,8 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
if (errors.size() > 0) if (errors.size() > 0)
output["errors"] = errors; output["errors"] = errors;
if (!m_compilerStack.unhandledSMTQueries().empty()) if (!m_compilerStack.unhandledSMTLib2Queries().empty())
for (string const& query: m_compilerStack.unhandledSMTQueries()) for (string const& query: m_compilerStack.unhandledSMTLib2Queries())
output["auxiliaryInputRequested"]["smtlib2"]["0x" + keccak256(query).hex()] = query; output["auxiliaryInputRequested"]["smtlib2"]["0x" + keccak256(query).hex()] = query;
output["sources"] = Json::objectValue; output["sources"] = Json::objectValue;