From 9a9a815fc9953d820a330fc6ca515e367f4d97aa Mon Sep 17 00:00:00 2001
From: chriseth <c@ethdev.com>
Date: Mon, 18 Jul 2016 18:16:22 +0200
Subject: Provide formal version in json output.
---
solc/jsonCompiler.cpp | 16 ++++++++++++++++
1 file changed, 16 insertions(+)
(limited to 'solc/jsonCompiler.cpp')
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)
{
--
cgit v1.2.3