diff options
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) { |