3 files changed, 110 insertions, 0 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 3ad9db92..6c4662ac 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -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)
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 85a37f2c..54e3b22a 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -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;
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index ff93f7c7..667d666b 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -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()
 
 }