mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
For loop.
This commit is contained in:
parent
5e2c066778
commit
19d5c42429
@ -126,6 +126,48 @@ bool SMTChecker::visit(WhileStatement const& _node)
|
||||
return false;
|
||||
}
|
||||
|
||||
bool SMTChecker::visit(ForStatement const& _node)
|
||||
{
|
||||
if (_node.initializationExpression())
|
||||
_node.initializationExpression()->accept(*this);
|
||||
|
||||
// Do not reset the init expression part.
|
||||
auto touchedVariables =
|
||||
m_variableUsage->touchedVariables(_node.body());
|
||||
if (_node.condition())
|
||||
touchedVariables += m_variableUsage->touchedVariables(*_node.condition());
|
||||
if (_node.loopExpression())
|
||||
touchedVariables += m_variableUsage->touchedVariables(*_node.loopExpression());
|
||||
// Remove duplicates
|
||||
std::sort(touchedVariables.begin(), touchedVariables.end());
|
||||
touchedVariables.erase(std::unique(touchedVariables.begin(), touchedVariables.end()), touchedVariables.end());
|
||||
|
||||
resetVariables(touchedVariables);
|
||||
|
||||
if (_node.condition())
|
||||
{
|
||||
_node.condition()->accept(*this);
|
||||
checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
|
||||
}
|
||||
|
||||
VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
|
||||
m_interface->push();
|
||||
if (_node.condition())
|
||||
m_interface->addAssertion(expr(*_node.condition()));
|
||||
_node.body().accept(*this);
|
||||
if (_node.loopExpression())
|
||||
_node.loopExpression()->accept(*this);
|
||||
|
||||
m_interface->pop();
|
||||
|
||||
m_conditionalExecutionHappened = true;
|
||||
m_currentSequenceCounter = sequenceCountersStart;
|
||||
|
||||
resetVariables(touchedVariables);
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
|
||||
{
|
||||
if (_varDecl.declarations().size() != 1)
|
||||
|
@ -52,6 +52,7 @@ private:
|
||||
virtual void endVisit(FunctionDefinition const& _node) override;
|
||||
virtual bool visit(IfStatement const& _node) override;
|
||||
virtual bool visit(WhileStatement const& _node) override;
|
||||
virtual bool visit(ForStatement const& _node) override;
|
||||
virtual void endVisit(VariableDeclarationStatement const& _node) override;
|
||||
virtual void endVisit(ExpressionStatement const& _node) override;
|
||||
virtual void endVisit(Assignment const& _node) override;
|
||||
|
@ -391,6 +391,73 @@ BOOST_AUTO_TEST_CASE(constant_condition)
|
||||
CHECK_SUCCESS_NO_WARNINGS(text);
|
||||
}
|
||||
|
||||
|
||||
BOOST_AUTO_TEST_CASE(for_loop)
|
||||
{
|
||||
string text = R"(
|
||||
contract C {
|
||||
function f(uint x) public pure {
|
||||
require(x == 2);
|
||||
for (;;) {}
|
||||
assert(x == 2);
|
||||
}
|
||||
}
|
||||
)";
|
||||
CHECK_SUCCESS_NO_WARNINGS(text);
|
||||
text = R"(
|
||||
contract C {
|
||||
function f(uint x) public pure {
|
||||
for (; x == 2; ) {
|
||||
assert(x == 2);
|
||||
}
|
||||
}
|
||||
}
|
||||
)";
|
||||
CHECK_SUCCESS_NO_WARNINGS(text);
|
||||
text = R"(
|
||||
contract C {
|
||||
function f(uint x) public pure {
|
||||
for (uint y = 2; x < 10; ) {
|
||||
assert(y == 2);
|
||||
}
|
||||
}
|
||||
}
|
||||
)";
|
||||
CHECK_SUCCESS_NO_WARNINGS(text);
|
||||
text = R"(
|
||||
contract C {
|
||||
function f(uint x) public pure {
|
||||
for (uint y = 2; x < 10; y = 3) {
|
||||
assert(y == 2);
|
||||
}
|
||||
}
|
||||
}
|
||||
)";
|
||||
CHECK_WARNING(text, "Assertion violation");
|
||||
text = R"(
|
||||
contract C {
|
||||
function f(uint x) public pure {
|
||||
for (uint y = 2; x < 10; ) {
|
||||
y = 3;
|
||||
}
|
||||
assert(y == 3);
|
||||
}
|
||||
}
|
||||
)";
|
||||
CHECK_WARNING(text, "Assertion violation");
|
||||
text = R"(
|
||||
contract C {
|
||||
function f(uint x) public pure {
|
||||
for (uint y = 2; x < 10; ) {
|
||||
y = 3;
|
||||
}
|
||||
assert(y == 2);
|
||||
}
|
||||
}
|
||||
)";
|
||||
CHECK_WARNING(text, "Assertion violation");
|
||||
}
|
||||
|
||||
BOOST_AUTO_TEST_SUITE_END()
|
||||
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user