aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/interface/StandardCompiler.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/interface/StandardCompiler.cpp')
-rw-r--r--libsolidity/interface/StandardCompiler.cpp25
1 files changed, 25 insertions, 0 deletions
diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp
index 291a1071..bf33b789 100644
--- a/libsolidity/interface/StandardCompiler.cpp
+++ b/libsolidity/interface/StandardCompiler.cpp
@@ -319,6 +319,27 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
return formatFatalError("JSONError", "Invalid input source specified.");
}
+ Json::Value const& auxInputs = _input["auxiliaryInput"];
+ if (!!auxInputs)
+ {
+ Json::Value const& smtlib2Responses = auxInputs["smtlib2responses"];
+ if (!!smtlib2Responses)
+ for (auto const& hashString: smtlib2Responses.getMemberNames())
+ {
+ h256 hash;
+ try
+ {
+ hash = h256(hashString);
+ }
+ catch (dev::BadHexCharacter const&)
+ {
+ return formatFatalError("JSONError", "Invalid hex encoding of SMTLib2 auxiliary input.");
+ }
+
+ m_compilerStack.addSMTLib2Response(hash, smtlib2Responses[hashString].asString());
+ }
+ }
+
Json::Value const& settings = _input.get("settings", Json::Value());
if (settings.isMember("evmVersion"))
@@ -518,6 +539,10 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
if (errors.size() > 0)
output["errors"] = errors;
+ if (!m_compilerStack.unhandledSMTLib2Queries().empty())
+ for (string const& query: m_compilerStack.unhandledSMTLib2Queries())
+ output["auxiliaryInputRequested"]["smtlib2queries"]["0x" + keccak256(query).hex()] = query;
+
output["sources"] = Json::objectValue;
unsigned sourceIndex = 0;
for (string const& sourceName: analysisSuccess ? m_compilerStack.sourceNames() : vector<string>())