Tests.

2 files changed, 240 insertions, 5 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 428afa9f..1cf5dc95 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -106,11 +106,6 @@ bool SMTChecker::visit(WhileStatement const& _node)
 {
 	// TODO Check if condition is always true
 
-	// TODO Weird side effects like
-	// uint x = 1;
-	// while (x ++ > 0) { assert(x == 2); }
-	// solution: clear variables first, then execute and assert condition, then executed body.
-
 	auto touchedVariables = m_variableUsage->touchedVariables(_node);
 	resetVariables(touchedVariables);
 	if (_node.isDoWhile())
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index 8d712a80..400f696c 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -105,6 +105,246 @@ BOOST_AUTO_TEST_CASE(warn_on_struct)
 	CHECK_WARNING_ALLOW_MULTI(text, "");
 }
 
+BOOST_AUTO_TEST_CASE(simple_assert)
+{
+	string text = R"(
+		contract C {
+			function f(uint a) public pure { assert(a == 2); }
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here for");
+}
+
+BOOST_AUTO_TEST_CASE(simple_assert_with_require)
+{
+	string text = R"(
+		contract C {
+			function f(uint a) public pure { require(a < 10); assert(a < 20); }
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
+BOOST_AUTO_TEST_CASE(assignment_in_declaration)
+{
+	string text = R"(
+		contract C {
+			function f() public pure { uint a = 2; assert(a == 2); }
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
+BOOST_AUTO_TEST_CASE(use_before_declaration)
+{
+	string text = R"(
+		contract C {
+			function f() public pure { a = 3; uint a = 2; assert(a == 2); }
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C {
+			function f() public pure { assert(a == 0); uint a = 2; assert(a == 2); }
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
+BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars)
+{
+	string text = R"(
+		contract C {
+			function f() public {
+				uint a = 3;
+				this.f();
+				assert(a == 3);
+				f();
+				assert(a == 3);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
+BOOST_AUTO_TEST_CASE(branches_clear_variables)
+{
+	// Only clears accessed variables
+	string text = R"(
+		contract C {
+			function f(uint x) public pure {
+				uint a = 3;
+				if (x > 10) {
+				}
+				assert(a == 3);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	// It is just a plain clear and will not combine branches.
+	text = R"(
+	contract C {
+			function f(uint x) public pure {
+				uint a = 3;
+				if (x > 10) {
+					a = 3;
+				}
+				assert(a == 3);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+	// Clear also works on the else branch
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				uint a = 3;
+				if (x > 10) {
+				} else {
+					a = 3;
+				}
+				assert(a == 3);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+	// Variable is not cleared, if it is only read.
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				uint a = 3;
+				if (x > 10) {
+					assert(a == 3);
+				} else {
+					assert(a == 3);
+				}
+				assert(a == 3);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
+BOOST_AUTO_TEST_CASE(branches_assert_condition)
+{
+	string text = R"(
+		contract C {
+			function f(uint x) public pure {
+				if (x > 10) {
+					assert(x > 9);
+				}
+				else
+				{
+					assert(x < 11);
+				}
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
+BOOST_AUTO_TEST_CASE(ways_to_clear_variables)
+{
+	string text = R"(
+		contract C {
+			function f(uint x) public pure {
+				uint a = 3;
+				if (x > 10) {
+					a++;
+				}
+				assert(a == 3);
+			}
+		}
+	)";
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				uint a = 3;
+				if (x > 10) {
+					++a;
+				}
+				assert(a == 3);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				uint a = 3;
+				if (x > 10) {
+					a = 5;
+				}
+				assert(a == 3);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+}
+
+BOOST_AUTO_TEST_CASE(while_loop_simple)
+{
+	// Check that variables are cleared
+	string text = R"(
+		contract C {
+			function f(uint x) public pure {
+				x = 2;
+				while (x > 1) {
+					x = 2;
+				}
+				assert(x == 2);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+	// Check that condition is assumed.
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				while (x == 2) {
+					assert(x == 2);
+				}
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	// Check that condition is not assumed after the body anymore
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				while (x == 2) {
+				}
+				assert(x == 2);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+	// Check that negation of condition is not assumed after the body anymore
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				while (x == 2) {
+				}
+				assert(x != 2);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+	// Check that side-effects of condition are taken into account
+	text = R"(
+		contract C {
+			function f(uint x) public pure {
+				x = 7;
+				while ((x = 5) > 0) {
+				}
+				assert(x == 7);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+}
+
+
 BOOST_AUTO_TEST_SUITE_END()
 
 }