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

[SMTChecker] Change warning message

Browse Source
This commit is contained in:
Leonardo Alt
2020-09-09 16:14:21 +02:00
parent d089b56457
commit 00f6b303b1
334 changed files with 547 additions and 550 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/BMC.cpp
+2 -5
View File
@@ -836,11 +836,11 @@ void BMC::checkCondition(
case smtutil::CheckResult::SATISFIABLE:
{
std::ostringstream message;
message << _description << " happens here";
message << _description << " happens here.";
if (_callStack.size())
{
std::ostringstream modelMessage;
modelMessage << " for:\n";
modelMessage << "\nCounterexample:\n";
solAssert(values.size() == expressionNames.size(), "");
map<string, string> sortedModel;
for (size_t i = 0; i < values.size(); ++i)
@@ -859,10 +859,7 @@ void BMC::checkCondition(
);
}
else
{
message << ".";
m_errorReporter.warning(6084_error, _location, message.str(), secondaryLocation);
}
break;
}
case smtutil::CheckResult::UNSATISFIABLE:
libsolidity/formal/CHC.cpp
+6 -6
View File
@@ -1251,7 +1251,7 @@ void CHC::checkVerificationTargets()
if (target.type == VerificationTarget::Type::PopEmptyArray)
{
solAssert(dynamic_cast<FunctionCall const*>(scope), "");
satMsg = "Empty array \"pop\" detected here";
satMsg = "Empty array \"pop\" detected here.";
unknownMsg = "Empty array \"pop\" might happen here.";
errorReporterId = 2529_error;
}
@@ -1267,8 +1267,8 @@ void CHC::checkVerificationTargets()
if (!intType)
intType = TypeProvider::uint256();
satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ") happens here";
satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ") happens here";
satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ") happens here.";
satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ") happens here.";
if (target.type == VerificationTarget::Type::Underflow)
{
satMsg = satMsgUnderflow;
@@ -1314,7 +1314,7 @@ void CHC::checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const&
solAssert(it != m_errorIds.end(), "");
unsigned errorId = it->second;
checkAndReportTarget(assertion, _target, errorId, 6328_error, "Assertion violation happens here");
checkAndReportTarget(assertion, _target, errorId, 6328_error, "Assertion violation happens here.");
}
}
@@ -1345,13 +1345,13 @@ void CHC::checkAndReportTarget(
_errorReporterId,
_scope->location(),
_satMsg,
SecondarySourceLocation().append(" for:\n" + *cex, SourceLocation{})
SecondarySourceLocation().append("\nCounterexample:\n" + *cex, SourceLocation{})
);
else
m_outerErrorReporter.warning(
_errorReporterId,
_scope->location(),
_satMsg + "."
_satMsg
);
}
else if (!_unknownMsg.empty())