New tests

test/libsolidity/smtCheckerTests/special/blockhash.sol

@@ -12,4 +12,3 @@ contract C
 // ----
 // Warning 6328: (85-109): CHC: Assertion violation happens here.
 // Warning 6328: (113-137): CHC: Assertion violation happens here.
-// Warning 6328: (155-191): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/special/msg_data.sol

@@ -4,7 +4,23 @@ contract C
 {
 	function f() public payable {
 		assert(msg.data.length > 0);
+		// Fails since calldata size should be 4
+		assert(msg.data.length > 4);
+		// f's sig is 0x26121ff0
+		assert(msg.data[0] == 0x26);
+		assert(msg.data[1] == 0x12);
+		assert(msg.data[2] == 0x1f);
+		assert(msg.data[3] == 0xf0);
+	}
+	function g() public payable {
+		// g's sig is 0xe2179b8e
+		assert(msg.data[0] == 0xe2);
+		assert(msg.data[1] == 0x17);
+		assert(msg.data[2] == 0x9b);
+		// Fails
+		assert(msg.data[3] == 0x8f);
 	}
 }
 // ----
-// Warning 6328: (79-106): CHC: Assertion violation happens here.
+// Warning 6328: (153-180): CHC: Assertion violation happens here.
+// Warning 6328: (500-527): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/special/msg_sig.sol

@@ -2,9 +2,29 @@ pragma experimental SMTChecker;
 
 contract C
 {
-	function f() public payable {
+	function f() public pure {
 		assert(msg.sig == 0x00000000);
+		assert(msg.sig == 0x26121ff0);
+		fi();
+		gi();
+	}
+	function fi() internal pure {
+		assert(msg.sig == 0x26121ff0);
+	}
+	function g() public pure {
+		assert(msg.sig == 0xe2179b8e);
+		gi();
+	}
+	function gi() internal pure {
+		// Fails since f can also call gi in which case msg.sig == 0x26121ff0
+		assert(msg.sig == 0xe2179b8e);
+	}
+	function h() public pure {
+		// Fails since gi can also call h in which case msg.sig can be f() or g()
+		assert(msg.sig == 0xe2179b8e);
 	}
 }
 // ----
-// Warning 6328: (79-108): CHC: Assertion violation happens here.
+// Warning 6328: (76-105): CHC: Assertion violation happens here.
+// Warning 6328: (403-432): CHC: Assertion violation happens here.
+// Warning 6328: (543-572): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/special/tx_data_gasleft_changes.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint gleft;
+
+	function f() public payable {
+		gleft = gasleft();
+
+		fi();
+
+		assert(gleft == gasleft());
+		assert(gleft >= gasleft());
+	}
+
+	function fi() internal view {
+		assert(gleft == gasleft());
+	}
+}
+// ----
+// Warning 6328: (124-150): CHC: Assertion violation happens here.
+// Warning 6328: (219-245): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/special/tx_data_immutable.sol

@@ -0,0 +1,61 @@
+pragma experimental SMTChecker;
+
+contract C {
+	bytes32 bhash;
+	address coin;
+	uint dif;
+	uint glimit;
+	uint number;
+	uint tstamp;
+	bytes mdata;
+	address sender;
+	bytes4 sig;
+	uint value;
+	uint gprice;
+	address origin;
+
+	function f() public payable {
+		bhash = blockhash(12);
+		coin = block.coinbase;
+		dif = block.difficulty;
+		glimit = block.gaslimit;
+		number = block.number;
+		tstamp = block.timestamp;
+		mdata = msg.data;
+		sender = msg.sender;
+		sig = msg.sig;
+		value = msg.value;
+		gprice = tx.gasprice;
+		origin = tx.origin;
+
+		fi();
+
+		assert(bhash == blockhash(12));
+		assert(coin == block.coinbase);
+		assert(dif == block.difficulty);
+		assert(glimit == block.gaslimit);
+		assert(number == block.number);
+		assert(tstamp == block.timestamp);
+		assert(mdata.length == msg.data.length);
+		assert(sender == msg.sender);
+		assert(sig == msg.sig);
+		assert(value == msg.value);
+		assert(gprice == tx.gasprice);
+		assert(origin == tx.origin);
+	}
+
+	function fi() internal view {
+		assert(bhash == blockhash(12));
+		assert(coin == block.coinbase);
+		assert(dif == block.difficulty);
+		assert(glimit == block.gaslimit);
+		assert(number == block.number);
+		assert(tstamp == block.timestamp);
+		assert(mdata.length == msg.data.length);
+		assert(sender == msg.sender);
+		assert(sig == msg.sig);
+		assert(value == msg.value);
+		assert(gprice == tx.gasprice);
+		assert(origin == tx.origin);
+	}
+}

test/libsolidity/smtCheckerTests/special/tx_data_immutable_fail.sol

@@ -0,0 +1,86 @@
+pragma experimental SMTChecker;
+
+contract C {
+	bytes32 bhash;
+	address coin;
+	uint dif;
+	uint glimit;
+	uint number;
+	uint tstamp;
+	bytes mdata;
+	address sender;
+	bytes4 sig;
+	uint value;
+	uint gprice;
+	address origin;
+
+	function f() public payable {
+		bhash = blockhash(12);
+		coin = block.coinbase;
+		dif = block.difficulty;
+		glimit = block.gaslimit;
+		number = block.number;
+		tstamp = block.timestamp;
+		mdata = msg.data;
+		sender = msg.sender;
+		sig = msg.sig;
+		value = msg.value;
+		gprice = tx.gasprice;
+		origin = tx.origin;
+
+		fi();
+
+		assert(bhash == blockhash(122));
+		assert(coin != block.coinbase);
+		assert(dif != block.difficulty);
+		assert(glimit != block.gaslimit);
+		assert(number != block.number);
+		assert(tstamp != block.timestamp);
+		assert(mdata.length != msg.data.length);
+		assert(sender != msg.sender);
+		assert(sig != msg.sig);
+		assert(value != msg.value);
+		assert(gprice != tx.gasprice);
+		assert(origin != tx.origin);
+	}
+
+	function fi() internal view {
+		assert(bhash == blockhash(122));
+		assert(coin != block.coinbase);
+		assert(dif != block.difficulty);
+		assert(glimit != block.gaslimit);
+		assert(number != block.number);
+		assert(tstamp != block.timestamp);
+		assert(mdata.length != msg.data.length);
+		assert(sender != msg.sender);
+		assert(sig != msg.sig);
+		assert(value != msg.value);
+		assert(gprice != tx.gasprice);
+		assert(origin != tx.origin);
+	}
+}
+// ----
+// Warning 6328: (545-576): CHC: Assertion violation happens here.
+// Warning 6328: (580-610): CHC: Assertion violation happens here.
+// Warning 6328: (614-645): CHC: Assertion violation happens here.
+// Warning 6328: (649-681): CHC: Assertion violation happens here.
+// Warning 6328: (685-715): CHC: Assertion violation happens here.
+// Warning 6328: (719-752): CHC: Assertion violation happens here.
+// Warning 6328: (756-795): CHC: Assertion violation happens here.
+// Warning 6328: (799-827): CHC: Assertion violation happens here.
+// Warning 6328: (831-853): CHC: Assertion violation happens here.
+// Warning 6328: (857-883): CHC: Assertion violation happens here.
+// Warning 6328: (887-916): CHC: Assertion violation happens here.
+// Warning 6328: (920-947): CHC: Assertion violation happens here.
+// Warning 6328: (986-1017): CHC: Assertion violation happens here.
+// Warning 6328: (1021-1051): CHC: Assertion violation happens here.
+// Warning 6328: (1055-1086): CHC: Assertion violation happens here.
+// Warning 6328: (1090-1122): CHC: Assertion violation happens here.
+// Warning 6328: (1126-1156): CHC: Assertion violation happens here.
+// Warning 6328: (1160-1193): CHC: Assertion violation happens here.
+// Warning 6328: (1197-1236): CHC: Assertion violation happens here.
+// Warning 6328: (1240-1268): CHC: Assertion violation happens here.
+// Warning 6328: (1272-1294): CHC: Assertion violation happens here.
+// Warning 6328: (1298-1324): CHC: Assertion violation happens here.
+// Warning 6328: (1328-1357): CHC: Assertion violation happens here.
+// Warning 6328: (1361-1388): CHC: Assertion violation happens here.