Merge pull request #10017 from ethereum/develop

Merge develop into breaking.

test/libsolidity/smtCheckerTests/types/array_literal_1.sol

@@ -4,8 +4,9 @@ contract C
 {
 	function f() public pure {
 		uint[3] memory array = [uint(1), 2, 3];
+		assert(array[0] == 1);
+		assert(array[1] == 2);
+		assert(array[2] == 3);
 	}
 }
 // ----
-// Warning 2072: (76-96): Unused local variable.
-// Warning 2177: (99-114): Assertion checker does not yet implement inline arrays.

test/libsolidity/smtCheckerTests/types/array_literal_2.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		uint[3] memory a = [uint(1), 2, 3];
+		uint[3] memory b = [uint(1), 2, 4];
+		assert(a[0] == b[0]);
+		assert(a[1] == b[1]);
+		assert(a[2] == b[2]); // fails
+	}
+}
+// ----
+// Warning 6328: (200-220): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/array_literal_3.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		(uint[3] memory a, uint[3] memory b) = ([uint(1), 2, 3], [uint(1), 2, 4]);
+		assert(a[0] == b[0]);
+		assert(a[1] == b[1]);
+		assert(a[2] == b[2]); // fails
+	}
+}
+// ----
+// Warning 6328: (201-221): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/array_literal_4.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool c) public pure {
+		uint[3] memory a = c ? [uint(1), 2, 3] : [uint(1), 2, 4];
+		uint[3] memory b = [uint(1), 2, c ? 3 : 4];
+		assert(a[0] == b[0]);
+		assert(a[1] == b[1]);
+		assert(a[2] == b[2]);
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/types/array_literal_5.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] s;
+	function f() public {
+		uint[3] memory a = [uint(1), 2, 3];
+		s = a;
+		assert(s.length == a.length);
+		assert(s[0] == a[0]);
+		assert(s[1] == a[1]);
+		assert(s[2] != a[2]); // fails
+	}
+}
+// ----
+// Warning 6328: (209-229): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/array_literal_6.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		uint[3] memory a = [uint(1), 2, 3];
+		uint[4] memory b = [uint(1), 2, 4, 3];
+		uint[4] memory c = b;
+		assert(a.length == c.length); // fails
+		assert(a[0] == c[0]);
+		assert(a[1] == c[1]);
+		assert(a[2] == c[2]); // fails
+		assert(a[2] == c[3]);
+	}
+}
+// ----
+// Warning 6328: (179-207): CHC: Assertion violation happens here.
+// Warning 6328: (268-288): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/array_literal_7.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] s;
+	function f() public {
+		uint[3] memory a = [uint(1), 2, 3];
+		uint[4] memory b = [uint(1), 2, 4, 3];
+		uint[4] memory c = b;
+		assert(c.length == b.length);
+		s = a;
+		assert(s.length == a.length);
+
+		assert(s.length == c.length); // fails
+		assert(s[0] == c[0]);
+		assert(s[1] == c[1]);
+		assert(s[2] == c[2]); // fails
+		assert(s[2] == c[3]);
+	}
+}
+// ----
+// Warning 6328: (259-287): CHC: Assertion violation happens here.
+// Warning 6328: (348-368): CHC: Assertion violation happens here.