Merge pull request #9106 from ethereum/develop

Merge develop into breaking.

test/libsolidity/smtCheckerTests/array_members/push_struct_member_1.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+contract C {
+	struct S {
+		int[] b;
+	}
+	S s;
+	struct T {
+		S s;
+	}
+	T t;
+	function f() public {
+		s.b.push();
+		t.s.b.push();
+	}
+}
+
+// ----
+// Warning: (72-75): Assertion checker does not yet support the type of this variable.
+// Warning: (100-103): Assertion checker does not yet support the type of this variable.
+// Warning: (130-133): Assertion checker does not yet support this expression.
+// Warning: (130-131): Assertion checker does not yet implement type struct C.S storage ref
+// Warning: (130-133): Assertion checker does not yet implement this expression.
+// Warning: (144-149): Assertion checker does not yet support this expression.
+// Warning: (144-147): Assertion checker does not yet implement type struct C.S storage ref
+// Warning: (144-147): Assertion checker does not yet support this expression.
+// Warning: (144-145): Assertion checker does not yet implement type struct C.T storage ref
+// Warning: (144-149): Assertion checker does not yet implement this expression.

test/libsolidity/smtCheckerTests/array_members/push_struct_member_2.sol

@@ -0,0 +1,33 @@
+pragma experimental SMTChecker;
+contract C {
+	struct S {
+		int[] b;
+	}
+	S s;
+	struct T {
+		S[] s;
+	}
+	T t;
+	function f() public {
+		s.b.push();
+		t.s.push();
+		t.s[0].b.push();
+	}
+}
+
+// ----
+// Warning: (72-75): Assertion checker does not yet support the type of this variable.
+// Warning: (102-105): Assertion checker does not yet support the type of this variable.
+// Warning: (132-135): Assertion checker does not yet support this expression.
+// Warning: (132-133): Assertion checker does not yet implement type struct C.S storage ref
+// Warning: (132-135): Assertion checker does not yet implement this expression.
+// Warning: (146-149): Assertion checker does not yet support this expression.
+// Warning: (146-147): Assertion checker does not yet implement type struct C.T storage ref
+// Warning: (146-156): Assertion checker does not yet implement type struct C.S storage ref
+// Warning: (146-149): Assertion checker does not yet implement this expression.
+// Warning: (160-168): Assertion checker does not yet support this expression.
+// Warning: (160-163): Assertion checker does not yet support this expression.
+// Warning: (160-161): Assertion checker does not yet implement type struct C.T storage ref
+// Warning: (160-166): Assertion checker does not yet implement type struct C.S storage ref
+// Warning: (160-166): Assertion checker does not yet implement this expression.
+// Warning: (160-168): Assertion checker does not yet implement this expression.

test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+contract C {
+	function g() public returns (uint) {
+		try this.g() returns (uint x) { x; }
+		catch Error(string memory s) { s; }
+	}
+}
+// ====
+// EVMVersion: >=byzantium
+// ----
+// Warning: (98-121): Assertion checker does not support try/catch clauses.
+// Warning: (124-159): Assertion checker does not support try/catch clauses.

test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+	function f() public {
+		try this.f() {}
+		catch (bytes memory x) {
+			x;
+		}
+	}
+}
+// ====
+// EVMVersion: >=byzantium
+// ----
+// Warning: (83-85): Assertion checker does not support try/catch clauses.
+// Warning: (88-122): Assertion checker does not support try/catch clauses.

test/libsolidity/smtCheckerTests/functions/internal_call_state_var_init.sol

@@ -0,0 +1,5 @@
+pragma experimental SMTChecker;
+contract c {
+	bool b = (f() == 0) && (f() == 0);
+	function f() internal returns (uint) {}
+}

test/libsolidity/smtCheckerTests/functions/internal_call_state_var_init_2.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+contract c {
+	uint x;
+	function f() internal returns (uint) {
+		x = x + 1;
+	}
+	bool b = (f() > 0) || (f() > 0);
+}
+// ----
+// Warning: (100-105): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning: (100-105): Underflow (resulting value less than 0) happens here
+// Warning: (100-105): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/operators/bitwise_and_int.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		int8 x = 1;
+		int8 y = 0;
+		assert(x & y != 0);
+		x = -1; y = 3;
+		assert(x & y == 3);
+		y = -1;
+		int8 z = x & y;
+		assert(z == -1);
+		y = 127;
+		assert(x & y == 127);
+	}
+}
+// ----
+// Warning: (104-122): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/bitwise_and_rational.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		assert(1 & 0 != 0);
+		assert(-1 & 3 == 3);
+		assert(-1 & -1 == -1);
+		assert(-1 & 127 == 127);
+	}
+}
+// ----
+// Warning: (76-94): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/bitwise_and_uint.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		uint8 x = 1;
+		uint16 y = 0;
+		assert(x & y != 0);
+		x = 0xff;
+		y = 0xffff;
+		assert(x & y == 0xff);
+		assert(x & y == 0xffff);
+		assert(x & y == 0x0000);
+	}
+}
+// ----
+// Warning: (107-125): Assertion violation happens here
+// Warning: (180-203): Assertion violation happens here
+// Warning: (207-230): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/delete_multid_array.sol

@@ -0,0 +1,42 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	uint[][] b;
+	function f(uint x, uint y, uint v) public {
+		a[x] = v;
+		delete a;
+		assert(a[y] == 0);
+	}
+ 	function g(uint x, uint y, uint v) public {
+		b[x][y] = v;
+		delete b;
+		assert(b[y][x] == 0);
+	}
+ 	function h(uint x, uint y, uint v) public {
+		b[x][y] = v;
+		delete b[x];
+		// Not necessarily the case.
+		assert(b[y][x] == 0);
+	}
+ 	function i(uint x, uint y, uint v) public {
+		b[x][y] = v;
+		delete b[y];
+		assert(b[y][x] == 0);
+	}
+ 	function j(uint x, uint y, uint z, uint v) public {
+		b[x][y] = v;
+		delete b[z];
+		// Not necessarily the case.
+		assert(b[y][x] == 0);
+	}
+	function setA(uint x, uint y) public {
+		a[x] = y;
+	}
+	function setB(uint x, uint y, uint z) public {
+		b[x][y] = z;
+	}
+}
+// ----
+// Warning: (372-392): Assertion violation happens here
+// Warning: (617-637): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/mapping_struct_assignment.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+contract C
+{
+	struct S {
+		uint x;
+	}
+	mapping (uint => S) smap;
+	function f(uint y, uint v) public {
+		if (0==1)
+			smap[y] = S(v);
+	}
+}
+// ----
+// Warning: (140-144): Condition is always false.
+// Warning: (149-156): Assertion checker does not yet implement type struct C.S storage ref
+// Warning: (159-160): Assertion checker does not yet implement type type(struct C.S storage pointer)
+// Warning: (159-163): Assertion checker does not yet implement type struct C.S memory
+// Warning: (159-163): Assertion checker does not yet implement this expression.
+// Warning: (149-163): Assertion checker does not yet implement type struct C.S storage ref