From bb10be789c269927e593b41d37aa0637db68bbe1 Mon Sep 17 00:00:00 2001 From: chriseth Date: Fri, 13 Oct 2017 15:19:53 +0200 Subject: Inject SMTLIB2 queries and responses via standard-json-io. --- libsolidity/interface/CompilerStack.h | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'libsolidity/interface/CompilerStack.h') diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h index 8c50266e..3fceed24 100644 --- a/libsolidity/interface/CompilerStack.h +++ b/libsolidity/interface/CompilerStack.h @@ -153,6 +153,13 @@ public: /// @returns true if a source object by the name already existed and was replaced. bool addSource(std::string const& _name, std::string const& _content, bool _isLibrary = false); + /// 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 const& unhandledSMTQueries() const { return m_unhandledSMTLib2Queries; } + /// Parses all source units that were added /// @returns false on error. bool parse(); @@ -334,7 +341,6 @@ private: ) const; ReadCallback::Callback m_readFile; - ReadCallback::Callback m_smtQuery; bool m_optimize = false; unsigned m_optimizeRuns = 200; EVMVersion m_evmVersion; @@ -344,6 +350,8 @@ private: /// "context:prefix=target" std::vector m_remappings; std::map m_sources; + std::vector m_unhandledSMTLib2Queries; + std::map m_smtlib2Responses; std::shared_ptr m_globalContext; std::vector m_sourceOrder; /// This is updated during compilation. -- cgit v1.2.3