New tests

Author: Leo Alt

test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero.sol

@@ -0,0 +1,11 @@
+contract C {
+	constructor() payable {
+		assert(address(this).balance == 0); // should fail
+		assert(address(this).balance > 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (40-74): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (93-126): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()

test/libsolidity/smtCheckerTests/blockchain_state/balance_non_zero_2.sol

@@ -0,0 +1,13 @@
+contract C {
+	constructor() payable {
+		require(msg.value > 100);
+	}
+	function f() public view {
+		assert(address(this).balance > 100); // should hold
+		assert(address(this).balance > 200); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (153-188): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ value: 101 }\nC.f()

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive.sol

@@ -0,0 +1,17 @@
+contract C {
+	uint prevBalance;
+	constructor() payable {
+		prevBalance = address(this).balance;
+	}
+	function f() public payable {
+		assert(address(this).balance == prevBalance + msg.value); // should fail because there might be funds from selfdestruct/block.coinbase
+		assert(address(this).balance < prevBalance + msg.value); // should fail
+		assert(address(this).balance >= prevBalance + msg.value); // should hold
+		prevBalance = address(this).balance;
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (132-188): CHC: Assertion violation happens here.\nCounterexample:\nprevBalance = 0\n\nTransaction trace:\nC.constructor()\nState: prevBalance = 0\nC.f(){ value: 168 }
+// Warning 6328: (269-324): CHC: Assertion violation happens here.\nCounterexample:\nprevBalance = 0\n\nTransaction trace:\nC.constructor()\nState: prevBalance = 0\nC.f(){ value: 1201 }

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol

@@ -0,0 +1,19 @@
+contract C {
+	uint x;
+	bool once;
+	constructor() payable {
+		x = address(this).balance;
+	}
+	function f() public payable {
+		require(!once);
+		once = true;
+		require(msg.value > 0);
+		assert(address(this).balance > x); // should hold
+		assert(address(this).balance > x + 10); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 4984: (266-272): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639926, once = true\n\nTransaction trace:\nC.constructor(){ value: 28100 }\nState: x = 115792089237316195423570985008687907853269984665640564039457584007913129639926, once = false\nC.f(){ value: 8 }
+// Warning 6328: (235-273): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, once = true\n\nTransaction trace:\nC.constructor()\nState: x = 0, once = false\nC.f(){ value: 8 }

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_3.sol

@@ -0,0 +1,9 @@
+contract C {
+	constructor() payable {
+		assert(address(this).balance == msg.value); // should fail because there might be funds from before deployment
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (40-82): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol

@@ -0,0 +1,21 @@
+contract C {
+	uint c;
+	function f() public payable {
+		require(msg.value > 10);
+		++c;
+	}
+	function inv() public view {
+		assert(address(this).balance >= c * 10); // should hold
+		assert(address(this).balance >= c * 12); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 4984: (82-85): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 4984: (154-160): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 4984: (212-218): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 6328: (180-219): CHC: Assertion violation happens here.\nCounterexample:\nc = 1\n\nTransaction trace:\nC.constructor()\nState: c = 0\nC.f(){ value: 11 }\nState: c = 1\nC.inv()
+// Warning 2661: (82-85): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 2661: (154-160): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 2661: (212-218): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_5.sol

@@ -0,0 +1,14 @@
+contract C {
+	uint sum = msg.value;
+	function f() public payable {
+		sum += msg.value;
+	}
+	function inv() public view {
+		assert(address(this).balance == sum); // should fail
+		assert(address(this).balance >= sum); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (122-158): CHC: Assertion violation happens here.\nCounterexample:\nsum = 0\n\nTransaction trace:\nC.constructor()\nState: sum = 0\nC.inv()

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_calls.sol

@@ -0,0 +1,26 @@
+contract C {
+	bool once;
+	function f() public payable {
+		require(!once);
+		once = true;
+		require(msg.value == 10);
+		assert(address(this).balance >= 10); // should hold
+		assert(address(this).balance >= 20); // should fail
+		g();
+	}
+	function g() internal view {
+		assert(address(this).balance >= 10); // should hold
+		assert(address(this).balance >= 20); // should fail
+		h();
+	}
+	function h() internal view {
+		assert(address(this).balance >= 10); // should hold
+		assert(address(this).balance >= 20); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (173-208): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ value: 10 }
+// Warning 6328: (321-356): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ value: 10 }\n    C.g(){ value: 10 } -- internal call
+// Warning 6328: (469-504): CHC: Assertion violation happens here.\nCounterexample:\nonce = true\n\nTransaction trace:\nC.constructor()\nState: once = false\nC.f(){ value: 10 }\n    C.g(){ value: 10 } -- internal call\n        C.h(){ value: 10 } -- internal call

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol

@@ -0,0 +1,17 @@
+interface I {
+	function ext() external;
+}
+
+contract C {
+	function f(I _i) public {
+		uint x = address(this).balance;
+		_i.ext();
+		assert(address(this).balance == x); // should fail
+		assert(address(this).balance >= x); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 1218: (131-165): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (131-165): CHC: Assertion violation might happen here.

test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol

@@ -0,0 +1,13 @@
+contract C {
+	function f(address _a) public {
+		uint x = address(this).balance;
+		_a.call("");
+		assert(address(this).balance == x); // should fail
+		assert(address(this).balance >= x); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 9302: (82-93): Return value of low-level calls not used.
+// Warning 6328: (97-131): CHC: Assertion violation happens here.\nCounterexample:\n\n_a = 0\nx = 5921\n\nTransaction trace:\nC.constructor()\nC.f(0)\n    _a.call("") -- untrusted external call, synthesized as:\n        C.f(0) -- reentrant call\n            _a.call("") -- untrusted external call