diff options
| author | chriseth <c@ethdev.com> | 2016-07-19 00:16:22 +0800 |
|---|---|---|
| committer | chriseth <c@ethdev.com> | 2016-07-19 00:26:56 +0800 |
| commit | 9a9a815fc9953d820a330fc6ca515e367f4d97aa (patch) | |
| tree | e745b7c4a331d8f297284f2905bdca348e1eff89 /solc/jsonCompiler.cpp | |
| parent | 417fde3eab0f862f7265e6881d4dc4404b37497e (diff) | |
| download | dexon-solidity-9a9a815fc9953d820a330fc6ca515e367f4d97aa.tar.gz dexon-solidity-9a9a815fc9953d820a330fc6ca515e367f4d97aa.tar.zst dexon-solidity-9a9a815fc9953d820a330fc6ca515e367f4d97aa.zip | |
Provide formal version in json output.
Diffstat (limited to 'solc/jsonCompiler.cpp')
| -rw-r--r-- | solc/jsonCompiler.cpp | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/solc/jsonCompiler.cpp b/solc/jsonCompiler.cpp index e8f674a0..bc1305c5 100644 --- a/solc/jsonCompiler.cpp +++ b/solc/jsonCompiler.cpp @@ -219,6 +219,22 @@ string compile(StringMap const& _sources, bool _optimize, CStyleReadFileCallback output["contracts"][contractName] = contractData; } + // Do not taint the internal error list + ErrorList formalErrors; + if (compiler.prepareFormalAnalysis(&formalErrors)) + output["formal"]["why3"] = compiler.formalTranslation(); + if (!formalErrors.empty()) + { + Json::Value errors(Json::arrayValue); + for (auto const& error: formalErrors) + errors.append(formatError( + *error, + (error->type() == Error::Type::Warning) ? "Warning" : "Error", + scannerFromSourceName + )); + output["formal"]["errors"] = errors; + } + output["sources"] = Json::Value(Json::objectValue); for (auto const& source: _sources) { |