cerc-io/solidity
10
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

Add errorCode list to invariants report

Browse Source
This commit is contained in:
Leo Alt 2021-10-13 16:21:12 +02:00
parent 49e7627bd3
commit d419c30ca6
3 changed files with 27 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
libsolidity/formal/CHC.cpp
View File

@ -31,6 +31,7 @@
#include <libsolidity/ast/TypeProvider.h> #include <libsolidity/ast/TypeProvider.h>
#include <libsmtutil/CHCSmtLib2Interface.h> #include <libsmtutil/CHCSmtLib2Interface.h>
#include <liblangutil/CharStreamProvider.h>
#include <libsolutil/Algorithms.h> #include <libsolutil/Algorithms.h>
#ifdef HAVE_Z3_DLOPEN #ifdef HAVE_Z3_DLOPEN
@ -1745,6 +1746,19 @@ void CHC::checkVerificationTargets()
for (auto const& inv: m_invariants.at(pred)) for (auto const& inv: m_invariants.at(pred))
msg += inv + "\n"; msg += inv + "\n";
} }
if (msg.find("<errorCode>") != string::npos)
{
set<unsigned> seenErrors;
msg += "<errorCode> = 0 -> no errors\n";
for (auto const& target: verificationTargets)
if (!seenErrors.count(target.errorId))
{
seenErrors.insert(target.errorId);
string loc = string(m_charStreamProvider.charStream(*target.errorNode->location().sourceName).text(target.errorNode->location()));
msg += "<errorCode> = " + to_string(target.errorId) + " -> " + ModelCheckerTargets::targetTypeToString.at(target.type) + " at " + loc + "\n";
}
}
if (!msg.empty()) if (!msg.empty())
m_errorReporter.info(1180_error, msg); m_errorReporter.info(1180_error, msg);
} }

11
libsolidity/formal/ModelCheckerSettings.cpp
View File

@ -71,6 +71,17 @@ map<string, TargetType> const ModelCheckerTargets::targetStrings{
{"outOfBounds", TargetType::OutOfBounds} {"outOfBounds", TargetType::OutOfBounds}
}; };
map<TargetType, string> const ModelCheckerTargets::targetTypeToString{
{TargetType::ConstantCondition, "Constant condition"},
{TargetType::Underflow, "Underflow"},
{TargetType::Overflow, "Overflow"},
{TargetType::DivByZero, "Division by zero"},
{TargetType::Balance, "Insufficient balance"},
{TargetType::Assert, "Assertion failed"},
{TargetType::PopEmptyArray, "Empty array pop"},
{TargetType::OutOfBounds, "Out of bounds access"}
};
std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const& _targets) std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const& _targets)
{ {
set<TargetType> chosenTargets; set<TargetType> chosenTargets;

2
libsolidity/formal/ModelCheckerSettings.h
View File

@ -131,6 +131,8 @@ struct ModelCheckerTargets
static std::map<std::string, VerificationTargetType> const targetStrings; static std::map<std::string, VerificationTargetType> const targetStrings;
static std::map<VerificationTargetType, std::string> const targetTypeToString;
bool operator!=(ModelCheckerTargets const& _other) const noexcept { return !(*this == _other); } bool operator!=(ModelCheckerTargets const& _other) const noexcept { return !(*this == _other); }
bool operator==(ModelCheckerTargets const& _other) const noexcept { return targets == _other.targets; } bool operator==(ModelCheckerTargets const& _other) const noexcept { return targets == _other.targets; }