Arithmetic compound assignment operators tests

test/libsolidity/SMTChecker.cpp

@@ -188,6 +188,48 @@ BOOST_AUTO_TEST_CASE(division_truncates_correctly)
 	CHECK_SUCCESS_NO_WARNINGS(text);
 }
 
+BOOST_AUTO_TEST_CASE(compound_assignment_division)
+{
+	string text = R"(
+		contract C {
+			function f(uint x) public pure {
+				require(x == 2);
+				uint y = 10;
+				y /= y / x;
+				assert(y == x);
+				assert(y == 0);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation");
+	text = R"(
+		contract C {
+			uint[] array;
+			function f(uint x, uint p) public {
+				require(x == 2);
+				require(array[p] == 10);
+				array[p] /= array[p] / x;
+				assert(array[p] == x);
+				assert(array[p] == 0);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation");
+	text = R"(
+		contract C {
+			mapping (uint => uint) map;
+			function f(uint x, uint p) public {
+				require(x == 2);
+				require(map[p] == 10);
+				map[p] /= map[p] / x;
+				assert(map[p] == x);
+				assert(map[p] == 0);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation");
+}
+
 BOOST_AUTO_TEST_SUITE_END()
 
 }

test/libsolidity/smtCheckerTests/operators/compound_add.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 100);
+		uint y = 100;
+		y += y + x;
+		assert(y < 300);
+		assert(y < 110);
+	}
+}
+// ----
+// Warning: (151-166): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] array;
+	function f(uint x, uint p) public {
+		require(x < 100);
+		require(array[p] == 100);
+		array[p] += array[p] + x;
+		assert(array[p] < 300);
+		assert(array[p] < 110);
+	}
+}
+// ----
+// Warning: (202-224): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_add_chain.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		uint a = 1;
+		uint b = 3;
+		uint c = 7;
+		a += b += c;
+		assert(b ==  10 && a == 11);
+		a += (b += c);
+		assert(b ==  17 && a == 28);
+		a += a += a;
+		assert(a == 112);
+	}
+}

test/libsolidity/smtCheckerTests/operators/compound_add_mapping.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) map;
+	function f(uint x, uint p) public {
+		require(x < 100);
+		require(map[p] == 100);
+		map[p] += map[p] + x;
+		assert(map[p] < 300);
+		assert(map[p] < 110);
+	}
+}
+// ----
+// Warning: (208-228): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_mul.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 10);
+		uint y = 10;
+		y *= y + x;
+		assert(y <= 190);
+		assert(y < 50);
+	}
+}
+// ----
+// Warning: (150-164): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_mul_array_index.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] array;
+	function f(uint x, uint p) public {
+		require(x < 10);
+		require(array[p] == 10);
+		array[p] *= array[p] + x;
+		assert(array[p] <= 190);
+		assert(array[p] < 50);
+	}
+}
+// ----
+// Warning: (201-222): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) map;
+	function f(uint x, uint p) public {
+		require(x < 10);
+		require(map[p] == 10);
+		map[p] *= map[p] + x;
+		assert(map[p] <= 190);
+		assert(map[p] < 50);
+	}
+}
+// ----
+// Warning: (207-226): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_sub.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		require(x < 100);
+		uint y = 200;
+		y -= y - x;
+		assert(y >= 0);
+		assert(y < 90);
+	}
+}
+// ----
+// Warning: (150-164): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_sub_array_index.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] array;
+	function f(uint x, uint p) public {
+		require(x < 100);
+		require(array[p] == 200);
+		array[p] -= array[p] - x;
+		assert(array[p] >= 0);
+		assert(array[p] < 90);
+	}
+}
+// ----
+// Warning: (201-222): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_sub_mapping.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) map;
+	function f(uint x, uint p) public {
+		require(x < 100);
+		require(map[p] == 200);
+		map[p] -= map[p] - x;
+		assert(map[p] >= 0);
+		assert(map[p] < 90);
+	}
+}
+// ----
+// Warning: (207-226): Assertion violation happens here