cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #728 from chriseth/formalout

Browse Source 
Provide formal version in json output.
This commit is contained in:
chriseth 2016-07-19 17:46:33 +02:00 committed by GitHub
commit 427deb43f5
3 changed files with 22 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libsolidity/interface/CompilerStack.cpp
View File

@ -253,9 +253,11 @@ void CompilerStack::link(const std::map<string, h160>& _libraries)
} }
} }
bool CompilerStack::prepareFormalAnalysis() bool CompilerStack::prepareFormalAnalysis(ErrorList* _errors)
{ {
Why3Translator translator(m_errors); if (!_errors)
_errors = &m_errors;
Why3Translator translator(*_errors);
for (Source const* source: m_sourceOrder) for (Source const* source: m_sourceOrder)
if (!translator.process(*source->ast)) if (!translator.process(*source->ast))
return false; return false;

3
libsolidity/interface/CompilerStack.h
View File

@ -124,8 +124,9 @@ public:
void link(std::map<std::string, h160> const& _libraries); void link(std::map<std::string, h160> const& _libraries);
/// Tries to translate all source files into a language suitable for formal analysis. /// Tries to translate all source files into a language suitable for formal analysis.
/// @param _errors list to store errors - defaults to the internal error list.
/// @returns false on error. /// @returns false on error.
bool prepareFormalAnalysis(); bool prepareFormalAnalysis(ErrorList* _errors = nullptr);
std::string const& formalTranslation() const { return m_formalTranslation; } std::string const& formalTranslation() const { return m_formalTranslation; }
/// @returns the assembled object for a contract. /// @returns the assembled object for a contract.

16
solc/jsonCompiler.cpp
View File

@ -219,6 +219,22 @@ string compile(StringMap const& _sources, bool _optimize, CStyleReadFileCallback
output["contracts"][contractName] = contractData; 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); output["sources"] = Json::Value(Json::objectValue);
for (auto const& source: _sources) for (auto const& source: _sources)
{ {