Merge remote-tracking branch 'origin/develop' into breaking

test/libsolidity/smtCheckerTests/external_calls/external.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+	uint x;
+	D d;
+	function f() public {
+		if (x < 10)
+			++x;
+	}
+	function g() public {
+		d.d();
+		assert(x < 10);
+	}
+}
+// ----
+// Warning 4661: (200-214): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+abstract contract Crypto {
+	function hash(bytes32) external pure virtual returns (bytes32);
+}
+
+contract C {
+	address owner;
+	bytes32 sig_1;
+	bytes32 sig_2;
+	Crypto d;
+
+	constructor() public {
+		owner = msg.sender;
+	}
+
+	function f1(bytes32 _msg) public {
+		address prevOwner = owner;
+		sig_1 = d.hash(_msg);
+		sig_2 = d.hash(_msg);
+		assert(prevOwner == owner);
+	}
+
+	function inv() public view {
+		assert(sig_1 == sig_2);
+	}
+}
+// ----
+// Warning 4661: (430-452): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol

@@ -0,0 +1,31 @@
+pragma experimental SMTChecker;
+
+contract Crypto {
+	function hash(bytes32) external pure returns (bytes32) {
+		return bytes32(0);
+	}
+}
+
+contract C {
+	address owner;
+	bytes32 sig_1;
+	bytes32 sig_2;
+	Crypto d;
+
+	constructor() public {
+		owner = msg.sender;
+	}
+
+	function f1(bytes32 _msg) public {
+		address prevOwner = owner;
+		sig_1 = d.hash(_msg);
+		sig_2 = d.hash(_msg);
+		assert(prevOwner == owner);
+	}
+
+	function inv() public view {
+		assert(sig_1 == sig_2);
+	}
+}
+// ----
+// Warning 4661: (438-460): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol

@@ -0,0 +1,38 @@
+pragma experimental SMTChecker;
+
+contract State {
+	uint x;
+	function f() public returns (uint) {
+		if (x == 0) x = 1;
+		else if (x == 1) x = 2;
+		else if (x == 2) x = 0;
+		return x;
+	}
+}
+
+contract C {
+	address owner;
+	uint y;
+	uint z;
+	State s;
+
+	constructor() public {
+		owner = msg.sender;
+	}
+
+	function f() public {
+		address prevOwner = owner;
+		y = s.f();
+		z = s.f();
+		assert(prevOwner == owner);
+	}
+
+	function inv() public view {
+		// This is safe but external calls do not yet support the state
+		// of the called contract.
+		assert(owner == address(0) || y != z);
+	}
+}
+// ----
+// Warning 5084: (551-561): Type conversion is not yet fully supported and might yield false positives.
+// Warning 4661: (535-572): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol

@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+
+contract State {
+	uint x;
+	C c;
+	function f() public view returns (uint) {
+		return c.g();
+	}
+}
+
+contract C {
+	address owner;
+	uint y;
+	State s;
+
+	constructor() public {
+		owner = msg.sender;
+	}
+
+	function f() public view {
+		address prevOwner = owner;
+		uint z = s.f();
+		assert(z == y);
+		assert(prevOwner == owner);
+	}
+
+	function g() public view returns (uint) {
+		return y;
+	}
+}
+// ----
+// Warning 4661: (306-320): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol

@@ -0,0 +1,47 @@
+pragma experimental SMTChecker;
+
+contract Other {
+	C c;
+	function h() public {
+		c.setOwner(address(0));
+	}
+}
+
+contract State {
+	uint x;
+	Other o;
+	C c;
+	function f() public returns (uint) {
+		o.h();
+		return c.g();
+	}
+}
+
+contract C {
+	address owner;
+	uint y;
+	State s;
+
+	constructor() public {
+		owner = msg.sender;
+	}
+
+	function setOwner(address _owner) public {
+		owner = _owner;
+	}
+
+	function f() public {
+		address prevOwner = owner;
+		uint z = s.f();
+		assert(z == y);
+		assert(prevOwner == owner);
+	}
+
+	function g() public view returns (uint) {
+		return y;
+	}
+}
+// ----
+// Warning 5084: (92-102): Type conversion is not yet fully supported and might yield false positives.
+// Warning 4661: (459-473): Assertion violation happens here
+// Warning 4661: (477-503): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol

@@ -0,0 +1,39 @@
+pragma experimental SMTChecker;
+
+contract State {
+	uint x;
+	C c;
+	function f() public returns (uint) {
+		c.setOwner(address(0));
+		return c.g();
+	}
+}
+
+contract C {
+	address owner;
+	uint y;
+	State s;
+
+	constructor() public {
+		owner = msg.sender;
+	}
+
+	function setOwner(address _owner) public {
+		owner = _owner;
+	}
+
+	function f() public {
+		address prevOwner = owner;
+		uint z = s.f();
+		assert(z == y);
+		assert(prevOwner == owner);
+	}
+
+	function g() public view returns (uint) {
+		return y;
+	}
+}
+// ----
+// Warning 5084: (116-126): Type conversion is not yet fully supported and might yield false positives.
+// Warning 4661: (388-402): Assertion violation happens here
+// Warning 4661: (406-432): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol

@@ -0,0 +1,43 @@
+pragma experimental SMTChecker;
+
+contract State {
+	uint x;
+	function f() public returns (uint) {
+		if (x == 0) x = 1;
+		else if (x == 1) x = 2;
+		else if (x == 2) x = 0;
+		return x;
+	}
+}
+
+contract C {
+	address owner;
+	uint y;
+	uint z;
+	State s;
+
+	constructor() public {
+		owner = msg.sender;
+	}
+
+	function setOwner(address _owner) public {
+		owner = _owner;
+	}
+
+	function f() public {
+		address prevOwner = owner;
+		y = s.f();
+		z = s.f();
+		assert(prevOwner == owner);
+	}
+
+	function inv() public view {
+		// This is safe but external calls do not yet support the state
+		// of the called contract.
+		assert(owner == address(0) || y != z);
+	}
+}
+// ----
+// Warning 4661: (442-468): Assertion violation happens here
+// Warning 5084: (617-627): Type conversion is not yet fully supported and might yield false positives.
+// Warning 4661: (601-638): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_inc.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+	uint x;
+	D d;
+
+	function inc() public {
+		++x;
+	}
+
+	function f() public {
+		d.d();
+		assert(x < 10);
+	}
+}
+// ----
+// Warning 2661: (146-149): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4661: (189-203): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_inc1_inc2.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+	uint x;
+	uint y;
+	D d;
+
+	function inc2() public {
+		if (y == 1)
+			x = 1;
+	}
+	function inc1() public {
+		if (x == 0)
+			y = 1;
+	}
+
+	function f() public {
+		uint oldX = x;
+		d.d();
+		assert(oldX == x);
+	}
+}
+// ----
+// Warning 4661: (286-303): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_safe.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+	uint x;
+	D d;
+	function f() public {
+		if (x < 10)
+			++x;
+	}
+	function g() public {
+		d.d();
+		assert(x < 11);
+	}
+}

test/libsolidity/smtCheckerTests/external_calls/external_single_inc.sol

@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+	uint x;
+	uint y;
+	D d;
+
+	function inc() public {
+		if (y == 1)
+			x = 1;
+		if (x == 0)
+			y = 1;
+	}
+
+	function f() public {
+		uint oldX = x;
+		d.d();
+		assert(oldX == x);
+	}
+}
+// ----
+// Warning 4661: (256-273): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/mutex.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+	uint x;
+	D d;
+
+	bool lock;
+	modifier mutex {
+		require(!lock);
+		lock = true;
+		_;
+		lock = false;
+	}
+
+	function set(uint _x) mutex public {
+		x = _x;
+	}
+
+	function f() mutex public {
+		uint y = x;
+		d.d();
+		assert(y == x);
+	}
+}

test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol

@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+	uint x;
+	D d;
+
+	bool lock;
+	modifier mutex {
+		require(!lock);
+		lock = true;
+		_;
+		lock = false;
+	}
+
+	function set(uint _x) mutex public {
+		x = _x;
+	}
+
+	function f() public {
+		uint y = x;
+		d.d();
+		assert(y == x);
+	}
+}
+// ----
+// Warning 4661: (307-321): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_external_1.sol

@@ -17,4 +17,3 @@ contract C
 	}
 }
 // ----
-// Warning 4661: (257-271): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_external_3.sol

@@ -18,4 +18,3 @@ contract C
 	}
 }
 // ----
-// Warning 4661: (355-379): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol

@@ -14,4 +14,6 @@ contract C
 	}
 }
 // ----
+// Warning 1218: (296-309): Error trying to invoke SMT solver.
 // Warning 2661: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4661: (296-309): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/address_staticcall.sol

@@ -20,6 +20,3 @@ contract C
 // ----
 // Warning 2072: (224-240): Unused local variable.
 // Warning 4661: (266-281): Assertion violation happens here
-// Warning 4661: (285-299): Assertion violation happens here
-// Warning 4661: (303-322): Assertion violation happens here
-// Warning 4661: (326-350): Assertion violation happens here