From 19e067465a058ca9f40238cb3a928a1113531c9d Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Thu, 5 Oct 2017 15:23:25 +0200
Subject: Unary operators and division.

---
 test/libsolidity/SMTChecker.cpp | 85 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 85 insertions(+)

(limited to 'test')

diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index 667d666b..7aa555e9 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -458,6 +458,91 @@ BOOST_AUTO_TEST_CASE(for_loop)
 	CHECK_WARNING(text, "Assertion violation");
 }
 
+BOOST_AUTO_TEST_CASE(division)
+{
+	string text = R"(
+		contract C {
+			function f(uint x, uint y) public pure returns (uint) {
+				return x / y;
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Division by zero");
+	text = R"(
+		contract C {
+			function f(uint x, uint y) public pure returns (uint) {
+				require(y != 0);
+				return x / y;
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C {
+			function f(int x, int y) public pure returns (int) {
+				require(y != 0);
+				return x / y;
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Overflow");
+	text = R"(
+		contract C {
+			function f(int x, int y) public pure returns (int) {
+				require(y != 0);
+				require(y != -1);
+				return x / y;
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
+BOOST_AUTO_TEST_CASE(division_truncates_correctly)
+{
+	string text = R"(
+		contract C {
+			function f(uint x, uint y) public pure {
+				x = 7;
+				y = 2;
+				assert(x / y == 3);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C {
+			function f(int x, int y) public pure {
+				x = 7;
+				y = 2;
+				assert(x / y == 3);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C {
+			function f(int x, int y) public pure {
+				x = -7;
+				y = 2;
+				assert(x / y == -3);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C {
+			function f(int x, int y) public pure {
+				x = -7;
+				y = -2;
+				int r = x / y;
+				assert(r == 3);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
 BOOST_AUTO_TEST_SUITE_END()
 
 }
-- 
cgit 


From 00e252a39faf99802ab46f32b41950c6f825063a Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Thu, 5 Oct 2017 19:31:28 +0200
Subject: Another test for division.

---
 test/libsolidity/SMTChecker.cpp | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'test')

diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index 7aa555e9..eac78835 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -530,6 +530,16 @@ BOOST_AUTO_TEST_CASE(division_truncates_correctly)
 		}
 	)";
 	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C {
+			function f(int x, int y) public pure {
+				x = 7;
+				y = -2;
+				assert(x / y == -3);
+			}
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
 	text = R"(
 		contract C {
 			function f(int x, int y) public pure {
-- 
cgit 


From 6d609557b6b2f13d7d8f8b13c2ceb1472266860a Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Thu, 5 Oct 2017 19:40:28 +0200
Subject: Fix test.

---
 test/libsolidity/SMTChecker.cpp | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'test')

diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index eac78835..38d02601 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -351,9 +351,9 @@ BOOST_AUTO_TEST_CASE(while_loop_simple)
 	// Check that side-effects of condition are taken into account
 	text = R"(
 		contract C {
-			function f(uint x) public pure {
+			function f(uint x, uint y) public pure {
 				x = 7;
-				while ((x = 5) > 0) {
+				while ((x = y) > 0) {
 				}
 				assert(x == 7);
 			}
@@ -545,8 +545,7 @@ BOOST_AUTO_TEST_CASE(division_truncates_correctly)
 			function f(int x, int y) public pure {
 				x = -7;
 				y = -2;
-				int r = x / y;
-				assert(r == 3);
+				assert(x / y == 3);
 			}
 		}
 	)";
-- 
cgit