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

Merge pull request #4646 from ethereum/smt_model_secondary_location

Browse Source 
SMT model is sorted and printed as secondary location
This commit is contained in:
Alex Beregszaszi 2018-08-01 23:20:28 +01:00 committed by GitHub
commit 9ec3fd1632
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 15 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
libsolidity/formal/SMTChecker.cpp
View File

@ -252,14 +252,14 @@ void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _
_value < SymbolicIntVariable::minValue(_type), _value < SymbolicIntVariable::minValue(_type),
_location, _location,
"Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")", "Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")",
"value", "<result>",
&_value &_value
); );
checkCondition( checkCondition(
_value > SymbolicIntVariable::maxValue(_type), _value > SymbolicIntVariable::maxValue(_type),
_location, _location,
"Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")", "Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")",
"value", "<result>",
&_value &_value
); );
} }
@ -437,7 +437,7 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
if (_op.getOperator() == Token::Div) if (_op.getOperator() == Token::Div)
{ {
checkCondition(right == 0, _op.location(), "Division by zero", "value", &right); checkCondition(right == 0, _op.location(), "Division by zero", "<result>", &right);
m_interface->addAssertion(right != 0); m_interface->addAssertion(right != 0);
} }
@ -601,15 +601,23 @@ void SMTChecker::checkCondition(
message << _description << " happens here"; message << _description << " happens here";
if (m_currentFunction) if (m_currentFunction)
{ {
message << " for:\n"; std::ostringstream modelMessage;
modelMessage << " for:\n";
solAssert(values.size() == expressionNames.size(), ""); solAssert(values.size() == expressionNames.size(), "");
map<string, string> sortedModel;
for (size_t i = 0; i < values.size(); ++i) for (size_t i = 0; i < values.size(); ++i)
if (expressionsToEvaluate.at(i).name != values.at(i)) if (expressionsToEvaluate.at(i).name != values.at(i))
message << " " << expressionNames.at(i) << " = " << values.at(i) << "\n"; sortedModel[expressionNames.at(i)] = values.at(i);
for (auto const& eval: sortedModel)
modelMessage << " " << eval.first << " = " << eval.second << "\n";
m_errorReporter.warning(_location, message.str() + loopComment, SecondarySourceLocation().append(modelMessage.str(), SourceLocation()));
} }
else else
{
message << "."; message << ".";
m_errorReporter.warning(_location, message.str() + loopComment); m_errorReporter.warning(_location, message.str() + loopComment);
}
break; break;
} }
case smt::CheckResult::UNSATISFIABLE: case smt::CheckResult::UNSATISFIABLE:

2
test/libsolidity/SMTChecker.cpp
View File

@ -110,7 +110,7 @@ BOOST_AUTO_TEST_CASE(simple_assert)
function f(uint a) public pure { assert(a == 2); } function f(uint a) public pure { assert(a == 2); }
} }
)"; )";
CHECK_WARNING(text, "Assertion violation happens here for"); CHECK_WARNING(text, "Assertion violation happens here");
} }
BOOST_AUTO_TEST_CASE(simple_assert_with_require) BOOST_AUTO_TEST_CASE(simple_assert_with_require)