aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex Beregszaszi <alex@rtfs.hu>2017-04-11 16:43:30 +0800
committerAlex Beregszaszi <alex@rtfs.hu>2017-04-21 02:38:00 +0800
commitaa0776d5e806be8f10ebcc21210ed25290c33598 (patch)
tree0157bffb607843d5952cc57ca30fffbbc46d26c0
parentb513db74a0bd8d5f3730cb3fec9f5385f5f194f8 (diff)
downloaddexon-solidity-aa0776d5e806be8f10ebcc21210ed25290c33598.tar.gz
dexon-solidity-aa0776d5e806be8f10ebcc21210ed25290c33598.tar.zst
dexon-solidity-aa0776d5e806be8f10ebcc21210ed25290c33598.zip
Support Why3 in StandardCompiler
-rw-r--r--libsolidity/interface/StandardCompiler.cpp24
1 files changed, 24 insertions, 0 deletions
diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp
index 8fffea8e..a2909fa3 100644
--- a/libsolidity/interface/StandardCompiler.cpp
+++ b/libsolidity/interface/StandardCompiler.cpp
@@ -337,6 +337,30 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
}
output["contracts"] = contractsOutput;
+ {
+ ErrorList formalErrors;
+ if (m_compilerStack.prepareFormalAnalysis(&formalErrors))
+ output["why3"] = m_compilerStack.formalTranslation();
+
+ for (auto const& error: formalErrors)
+ {
+ auto err = dynamic_pointer_cast<Error const>(error);
+
+ errors.append(formatErrorWithException(
+ *error,
+ err->type() == Error::Type::Warning,
+ err->typeName(),
+ "general",
+ "",
+ scannerFromSourceName
+ ));
+ }
+
+ // FIXME!!
+ if (!formalErrors.empty())
+ output["errors"] = errors;
+ }
+
return output;
}