Merge pull request #5416 from ethereum/develop

Merge develop into release for 0.5.0

29 files changed, 386 insertions, 0 deletions

diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol
new file mode 100644
index 00000000..25a42db6
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = h(42);
+		assert(x > 0);
+	}
+}
+
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol
new file mode 100644
index 00000000..a70aaf61
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = h(0);
+		assert(x > 0);
+	}
+}
+
+// ----
+// Warning: (161-174): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol
new file mode 100644
index 00000000..aff24b03
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return k(x);
+	}
+
+	function k(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = h(2);
+		assert(x > 0);
+	}
+}
+
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol
new file mode 100644
index 00000000..9baeb935
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol
@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return k(x);
+	}
+
+	function k(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = h(0);
+		assert(x > 0);
+	}
+}
+
+// ----
+// Warning: (229-242): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol
new file mode 100644
index 00000000..3793f411
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = (h)(42);
+		assert(x > 0);
+	}
+}
+
+// ----
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol
new file mode 100644
index 00000000..e3c80594
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = (h)(0);
+		assert(x > 0);
+	}
+}
+
+// ----
+// Warning: (163-176): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol b/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol
new file mode 100644
index 00000000..d2f8ab1d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function g() public {
+		if (a > 0)
+		{
+			a = a - 1;
+			g();
+		}
+		else
+			assert(a == 0);
+	}
+}
+
+// ----
+// Warning: (111-114): Assertion checker does not support recursive function calls.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol
new file mode 100644
index 00000000..d5b83f00
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol
@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f() public {
+		if (a > 0)
+		{
+			a = a - 1;
+			g();
+		}
+		else
+			assert(a == 0);
+	}
+	function g() public {
+		if (a > 0)
+		{
+			a = a - 1;
+			f();
+		}
+		else
+			assert(a == 0);
+	}
+}
+// ----
+// Warning: (206-209): Assertion checker does not support recursive function calls.
+// Warning: (111-114): Assertion checker does not support recursive function calls.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol
new file mode 100644
index 00000000..2f7563dd
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f(uint x) public {
+		uint y;
+		a = (y = x);
+	}
+	function g() public {
+		f(1);
+		assert(a > 0);
+	}
+}
+
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol
new file mode 100644
index 00000000..ad735768
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol
@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f(uint x) public {
+		uint y;
+		a = (y = x);
+	}
+	function g() public {
+		f(0);
+		assert(a > 0);
+	}
+}
+
+// ----
+// Warning: (144-157): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol
new file mode 100644
index 00000000..2f95d8af
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f(uint x) public {
+		uint y;
+		a = (y = x);
+	}
+	function g() public {
+		f(1);
+		f(42);
+		assert(a > 1);
+	}
+}
+
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol
new file mode 100644
index 00000000..5d972f96
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f(uint x) public {
+		uint y;
+		a = (y = x);
+	}
+	function g() public {
+		f(1);
+		f(0);
+		assert(a > 0);
+	}
+}
+
+// ----
+// Warning: (152-165): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol
new file mode 100644
index 00000000..7693ad81
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { require(x); for (;x;) {} }
+}
+// ----
+// Warning: (98-99): For loop condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol
new file mode 100644
index 00000000..ed1ad73a
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { for (;x;) {} }
+	function g() public pure { f(true); }
+}
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol
new file mode 100644
index 00000000..364fe8d1
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function f(bool x) public pure { require(x); if (x) {} }
+}
+// ----
+// Warning: (95-96): Condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol
new file mode 100644
index 00000000..e76badf2
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { x = true; require(x); }
+}
+// ----
+// Warning: (98-99): Condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol
new file mode 100644
index 00000000..5cae940b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { require(x); }
+	function g() public pure { f(true); }
+}
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol
new file mode 100644
index 00000000..66396dd8
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { require(x); while (x) {} }
+}
+// ----
+// Warning: (99-100): While loop condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol
new file mode 100644
index 00000000..5000eeb6
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { while (x) {} }
+	function g() public pure { f(true); }
+}
diff --git a/test/libsolidity/smtCheckerTests/special/blockhash.sol b/test/libsolidity/smtCheckerTests/special/blockhash.sol
new file mode 100644
index 00000000..1c693914
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/blockhash.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public payable {
+		assert(blockhash(2) > 0);
+	}
+}
+// ----
+// Warning: (79-103): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/special/difficulty.sol b/test/libsolidity/smtCheckerTests/special/difficulty.sol
new file mode 100644
index 00000000..4469d4e5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/difficulty.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint difficulty) public view {
+		assert(block.difficulty == difficulty);
+	}
+}
+// ----
+// Warning: (91-129): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/special/gasleft.sol b/test/libsolidity/smtCheckerTests/special/gasleft.sol
new file mode 100644
index 00000000..857230fe
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/gasleft.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public view {
+		assert(gasleft() > 0);
+		uint g = gasleft();
+		assert(g < gasleft());
+		assert(g >= gasleft());
+	}
+}
+// ----
+// Warning: (76-97): Assertion violation happens here
+// Warning: (123-144): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/special/many.sol b/test/libsolidity/smtCheckerTests/special/many.sol
new file mode 100644
index 00000000..40e5d987
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/many.sol
@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public payable {
+		assert(msg.sender == block.coinbase);
+		assert(block.difficulty == block.gaslimit);
+		assert(block.number == block.timestamp);
+		assert(tx.gasprice == msg.value);
+		assert(tx.origin == msg.sender);
+		uint x = block.number;
+		assert(x + 2 > block.number);
+		assert(now > 10);
+		assert(gasleft() > 100);
+	}
+}
+// ----
+// Warning: (79-115): Assertion violation happens here
+// Warning: (119-161): Assertion violation happens here
+// Warning: (165-204): Assertion violation happens here
+// Warning: (208-240): Assertion violation happens here
+// Warning: (244-275): Assertion violation happens here
+// Warning: (311-316): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here
+// Warning: (336-352): Assertion violation happens here
+// Warning: (356-379): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/special/msg_data.sol b/test/libsolidity/smtCheckerTests/special/msg_data.sol
new file mode 100644
index 00000000..7e748f09
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/msg_data.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public payable {
+		assert(msg.data.length > 0);
+	}
+}
+// ----
+// Warning: (86-101): Assertion checker does not yet support this expression.
+// Warning: (86-94): Assertion checker does not yet support this special variable.
+// Warning: (86-94): Assertion checker does not yet implement this type.
+// Warning: (86-101): Internal error: Expression undefined for SMT solver.
+// Warning: (79-106): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_1.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_1.sol
new file mode 100644
index 00000000..dd2366e2
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/msg_sender_1.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public view {
+		address a = msg.sender;
+		address b = msg.sender;
+		assert(a == b);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol
new file mode 100644
index 00000000..ad45d076
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public view {
+		require(msg.sender != address(0));
+		address a = msg.sender;
+		address b = msg.sender;
+		assert(a == b);
+	}
+}
+// ----
+// Warning: (98-108): Assertion checker does not yet implement this expression.
+// Warning: (98-108): Internal error: Expression undefined for SMT solver.
diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol
new file mode 100644
index 00000000..9a4eefd5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(address c) public view {
+		address a = msg.sender;
+		address b = msg.sender;
+		assert(a == b);
+		assert(c == msg.sender);
+	}
+}
+// ----
+// Warning: (155-178): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/special/msg_sig.sol b/test/libsolidity/smtCheckerTests/special/msg_sig.sol
new file mode 100644
index 00000000..109470a8
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/msg_sig.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public payable {
+		assert(msg.sig == 0x00000000);
+	}
+}
+// ----
+// Warning: (79-108): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_1.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_1.sol
new file mode 100644
index 00000000..541fff54
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_1.sol
@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	bytes32 x;
+	function f(bytes8 y) public view {
+		assert(x != y);
+		assert(x != g());
+	}
+	function g() public view returns (bytes32) {
+		return x;
+	}
+}
+// ----
+// Warning: (96-110): Assertion violation happens here
+// Warning: (114-130): Assertion violation happens here