diff options
| author | Alex Beregszaszi <alex@rtfs.hu> | 2017-04-11 16:43:30 +0800 |
|---|---|---|
| committer | Alex Beregszaszi <alex@rtfs.hu> | 2017-04-21 02:38:00 +0800 |
| commit | aa0776d5e806be8f10ebcc21210ed25290c33598 (patch) | |
| tree | 0157bffb607843d5952cc57ca30fffbbc46d26c0 | |
| parent | b513db74a0bd8d5f3730cb3fec9f5385f5f194f8 (diff) | |
| download | dexon-solidity-aa0776d5e806be8f10ebcc21210ed25290c33598.tar.gz dexon-solidity-aa0776d5e806be8f10ebcc21210ed25290c33598.tar.zst dexon-solidity-aa0776d5e806be8f10ebcc21210ed25290c33598.zip | |
Support Why3 in StandardCompiler
| -rw-r--r-- | libsolidity/interface/StandardCompiler.cpp | 24 |
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; } |