Add new tests with semantic this and indirect storage changes

test/libsolidity/smtCheckerTests/deployment/deploy_bmc_trusted.sol

@@ -0,0 +1,18 @@
+contract D {
+	uint x;
+	function f() public view returns (uint) { return x; }
+}
+
+contract C {
+	function g() public {
+		D d = new D();
+		uint y = d.f();
+		assert(y == 0); // should fail in BMC
+	}
+}
+// ====
+// SMTEngine: bmc
+// SMTExtCalls: trusted
+// ----
+// Warning 8729: (124-131): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
+// Warning 4661: (153-167): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/deployment/deploy_bmc_untrusted.sol

@@ -0,0 +1,17 @@
+contract D {
+	uint x;
+	function f() public view returns (uint) { return x; }
+}
+
+contract C {
+	function g() public {
+		D d = new D();
+		uint y = d.f();
+		assert(y == 0); // should fail in ext calls untrusted mode
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 8729: (124-131): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
+// Warning 4661: (153-167): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/deployment/deploy_trusted.sol

@@ -0,0 +1,16 @@
+contract D {
+	uint x;
+	function f() public view returns (uint) { return x; }
+}
+
+contract C {
+	function g() public {
+		D d = new D();
+		uint y = d.f();
+		assert(y == 0); // should hold in ext calls trusted mode
+	}
+}
+// ====
+// SMTEngine: all
+// SMTExtCalls: trusted
+// ----

test/libsolidity/smtCheckerTests/deployment/deploy_trusted_addresses.sol

@@ -0,0 +1,19 @@
+contract D {
+	uint x;
+}
+
+contract C {
+	function f() public {
+		D d1 = new D();
+		D d2 = new D();
+
+		assert(d1 != d2); // should hold in ext calls trusted mode
+		assert(address(this) != address(d1)); // should hold in ext calls trusted mode
+		assert(address(this) != address(d2)); // should hold in ext calls trusted mode
+	}
+}
+// ====
+// SMTEngine: all
+// SMTExtCalls: trusted
+// ----
+// Info 1180: Contract invariant(s) for :C:\n(:var 0).isActive[address(this)]\n

test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol

@@ -0,0 +1,24 @@
+contract D {
+	uint x;
+	function inc() public { ++x; }
+	function f() public view returns (uint) { return x; }
+}
+
+contract C {
+	function f() public {
+		D d = new D();
+		assert(d.f() == 0); // should hold
+		d.inc();
+		assert(d.f() == 1); // should hold
+		d = new D();
+		assert(d.f() == 0); // should hold
+		assert(d.f() == 1); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// SMTExtCalls: trusted
+// ----
+// Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 6328: (304-322): CHC: Assertion violation happens here.
+// Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/deployment/deploy_trusted_keep_storage_constraints.sol

@@ -0,0 +1,17 @@
+contract D {
+	uint x;
+}
+
+contract C {
+	uint y;
+	function g() public {
+		D d = new D();
+		assert(y == 0); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// SMTExtCalls: trusted
+// ----
+// Warning 2072: (72-75): Unused local variable.
+// Info 1180: Contract invariant(s) for :C:\n(y <= 0)\n

test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol

@@ -0,0 +1,23 @@
+contract D {
+	uint x;
+	function inc() public { ++x; }
+	function f() public view returns (uint) { return x; }
+}
+
+contract C {
+	D d;
+	constructor() {
+		d = new D();
+		assert(d.f() == 0); // should hold
+	}
+	function g() public view {
+		assert(d.f() == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// SMTExtCalls: trusted
+// ----
+// Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 6328: (233-251): CHC: Assertion violation happens here.
+// Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_2.sol

@@ -0,0 +1,20 @@
+contract D {
+	uint x;
+	function f() public view returns (uint) { return x; }
+}
+
+contract C {
+	D d;
+	constructor() {
+		d = new D();
+		assert(d.f() == 0); // should hold
+	}
+	function g() public view {
+		assert(d.f() == 0); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// SMTExtCalls: trusted
+// ----
+// Info 1180: Contract invariant(s) for :C:\n((:var 1).storage.storage_D_12[d].x_3_D_12 <= 0)\nReentrancy property(ies) for :D:\n((x' <= 0) || !(x <= 0))\n

test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_3.sol

@@ -0,0 +1,23 @@
+contract D {
+	uint x;
+	function s(uint _x) public { x = _x; }
+	function f() public view returns (uint) { return x; }
+}
+
+contract C {
+	D d;
+	constructor() {
+		d = new D();
+	}
+	function g() public view {
+		assert(d.f() == 0); // should fail
+	}
+}
+// ====
+// SMTContract: C
+// SMTEngine: all
+// SMTExtCalls: trusted
+// ----
+// Warning 1218: (204-222): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (204-222): CHC: Assertion violation might happen here.
+// Warning 4661: (204-222): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_4.sol

@@ -0,0 +1,20 @@
+contract D {
+	bool b;
+	function s() public { b = true; }
+	function f() public view returns (bool) { return b; }
+}
+
+contract C {
+	D d;
+	constructor() {
+		d = new D();
+	}
+	function g() public view {
+		assert(d.f()); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// SMTExtCalls: trusted
+// ----
+// Warning 6328: (199-212): CHC: Assertion violation happens here.\nCounterexample:\nd = 0\n\nTransaction trace:\nC.constructor()\nState: d = 0\nC.g()\n    D.f() -- trusted external call

test/libsolidity/smtCheckerTests/deployment/deploy_untrusted.sol

@@ -0,0 +1,17 @@
+contract D {
+	uint x;
+	function f() public view returns (uint) { return x; }
+}
+
+contract C {
+	function g() public {
+		D d = new D();
+		uint y = d.f();
+		assert(y == 0); // should fail in ext calls untrusted mode
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 8729: (124-131): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
+// Warning 6328: (153-167): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0\ny = 1\n\nTransaction trace:\nC.constructor()\nC.g()\n    d.f() -- untrusted external call

test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_addresses.sol

@@ -0,0 +1,22 @@
+contract D {
+	uint x;
+}
+
+contract C {
+	function f() public {
+		D d1 = new D();
+		D d2 = new D();
+
+		assert(d1 != d2); // should fail in ext calls untrusted mode
+		assert(address(this) != address(d1)); // should fail in ext calls untrusted mode
+		assert(address(this) != address(d2)); // should fail in ext calls untrusted mode
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 8729: (70-77): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
+// Warning 8729: (88-95): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
+// Warning 6328: (100-116): CHC: Assertion violation happens here.\nCounterexample:\n\nd1 = 0\nd2 = 0\n\nTransaction trace:\nC.constructor()\nC.f()
+// Warning 6328: (163-199): CHC: Assertion violation happens here.\nCounterexample:\n\nd1 = 21238\nd2 = 21238\n\nTransaction trace:\nC.constructor()\nC.f()
+// Warning 6328: (246-282): CHC: Assertion violation happens here.\nCounterexample:\n\nd1 = 21238\nd2 = 21238\n\nTransaction trace:\nC.constructor()\nC.f()

test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_erase_storage_constraints.sol

@@ -0,0 +1,17 @@
+contract D {
+	uint x;
+}
+
+contract C {
+	uint y;
+	function g() public {
+		D d = new D();
+		assert(y == 0); // should fail in ext calls untrusted mode
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 2072: (72-75): Unused local variable.
+// Warning 8729: (78-85): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
+// Warning 6328: (89-103): CHC: Assertion violation happens here.\nCounterexample:\ny = 1\nd = 0\n\nTransaction trace:\nC.constructor()\nState: y = 0\nC.g()

test/libsolidity/smtCheckerTests/deployment/deployment_trusted_with_value_1.sol

@@ -0,0 +1,20 @@
+contract A {
+	constructor() payable {}
+}
+
+contract B {
+	function f() public payable {
+		require(address(this).balance == 100);
+		A a = new A{value: 50}();
+		assert(address(this).balance == 50); // should hold
+		assert(address(this).balance == 60); // should fail
+		assert(address(a).balance >= 50); // should hold
+		assert(address(a).balance == 50); // should fail
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// ----
+// Warning 6328: (211-246): CHC: Assertion violation happens here.
+// Warning 6328: (316-348): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1_trusted.sol

@@ -0,0 +1,21 @@
+contract State {
+	function f(uint _x) public pure returns (uint) {
+		assert(_x < 100);
+		return _x;
+	}
+}
+contract C {
+	State s;
+	uint z = s.f(2);
+
+	function f() public view {
+		assert(z == 2); // should hold in trusted mode
+	}
+}
+// ====
+// SMTContract: C
+// SMTEngine: all
+// SMTExtCalls: trusted
+// ----
+// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
+// Info 1180: Contract invariant(s) for :C:\n(!(z >= 3) && !(z <= 1))\n

test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2_trusted.sol

@@ -0,0 +1,17 @@
+contract C {
+	uint z = this.g(2);
+
+	function g(uint _x) public pure returns (uint) {
+		assert(_x > 0); // should fail
+		return _x;
+	}
+
+	function f() public view {
+		assert(z == 2); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nz = 2\n_x = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: z = 2\nC.g(0)
+// Info 1180: Contract invariant(s) for :C:\n(!(z >= 3) && !(z <= 1))\n

test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3_trusted.sol

@@ -0,0 +1,25 @@
+contract State {
+	function f(uint _x) public pure returns (uint) {
+		assert(_x < 100);
+		return _x;
+	}
+}
+contract C {
+	State s;
+	uint z;
+
+	constructor() {
+		z = s.f(2);
+	}
+
+	function f() public view {
+		assert(z == 2); // should hold in trusted mode
+	}
+}
+// ====
+// SMTContract: C
+// SMTEngine: all
+// SMTExtCalls: trusted
+// ----
+// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
+// Info 1180: Contract invariant(s) for :C:\n(!(z >= 3) && !(z <= 1))\n

test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol

@@ -0,0 +1,40 @@
+contract A {
+	uint x;
+	function setX(uint _x) public {
+		x = _x;
+	}
+	function getX() public view returns (uint) {
+		return x;
+	}
+}
+
+contract B {
+	A a;
+	constructor() {
+		a = new A();
+		assert(a.getX() == 0); // should hold
+	}
+	function g() public view {
+		assert(a.getX() == 0); // should fail because A.setX() can be called without B
+	}
+	function getX() public view returns (uint) {
+		return a.getX();
+	}
+}
+
+contract C {
+	B b;
+	constructor() {
+		b = new B();
+		assert(b.getX() == 0); // should hold
+	}
+	function f() public view {
+		assert(b.getX() == 0); // should fail because A.setX() can be called without A
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// ----
+// Warning 6328: (256-277): CHC: Assertion violation happens here.
+// Warning 6328: (533-554): CHC: Assertion violation might happen here.

test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_2.sol

@@ -0,0 +1,46 @@
+contract A {
+	uint x;
+	address immutable owner;
+	constructor() {
+		owner = msg.sender;
+	}
+	function setX(uint _x) public {
+		require(msg.sender == owner);
+		x = _x;
+	}
+	function getX() public view returns (uint) {
+		return x;
+	}
+}
+
+contract B {
+	A a;
+	constructor() {
+		a = new A();
+		assert(a.getX() == 0); // should hold
+	}
+	function g() public view {
+		assert(a.getX() == 0); // should hold
+	}
+	function getX() public view returns (uint) {
+		return a.getX();
+	}
+}
+
+contract C {
+	B b;
+	constructor() {
+		b = new B();
+		assert(b.getX() == 0); // should hold
+	}
+	function f() public view {
+		assert(b.getX() == 0); // should hold
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// ----
+// Warning 1218: (356-377): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (356-377): CHC: Assertion violation might happen here.
+// Warning 6328: (592-613): CHC: Assertion violation might happen here.

test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol

@@ -0,0 +1,44 @@
+contract A {
+	uint x;
+	address immutable owner;
+	constructor() {
+		owner = msg.sender;
+	}
+	function setX(uint _x) public {
+		require(msg.sender == owner);
+		x = _x;
+	}
+	function getX() public view returns (uint) {
+		return x;
+	}
+}
+
+contract B {
+	A a;
+	constructor() {
+		a = new A();
+		assert(a.getX() == 0); // should hold
+	}
+	function g() public {
+		a.setX(42);
+	}
+	function getX() public view returns (uint) {
+		return a.getX();
+	}
+}
+
+contract C {
+	B b;
+	constructor() {
+		b = new B();
+		assert(b.getX() == 0); // should hold
+	}
+	function f() public view {
+		assert(b.getX() == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// ----
+// Warning 6328: (561-582): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol

@@ -0,0 +1,48 @@
+contract A {
+	uint x;
+	address immutable owner;
+	constructor() {
+		owner = msg.sender;
+	}
+	function setX(uint _x) public {
+		require(msg.sender == owner);
+		x = _x;
+	}
+	function getX() public view returns (uint) {
+		return x;
+	}
+}
+
+contract B {
+	A a;
+	address immutable owner;
+	constructor() {
+		owner = msg.sender;
+		a = new A();
+		assert(a.getX() == 0); // should hold
+	}
+	function g() public {
+		require(msg.sender == owner);
+		a.setX(42);
+	}
+	function getX() public view returns (uint) {
+		return a.getX();
+	}
+}
+
+contract C {
+	B b;
+	constructor() {
+		b = new B();
+		assert(b.getX() == 0); // should hold
+	}
+	function f() public view {
+		assert(b.getX() == 0); // should hold
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// ----
+// Warning 1218: (641-662): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (641-662): CHC: Assertion violation might happen here.

test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_5.sol

@@ -0,0 +1,50 @@
+contract A {
+	uint x;
+	address immutable owner;
+	constructor() {
+		owner = msg.sender;
+	}
+	function setX(uint _x) public {
+		require(msg.sender == owner);
+		x = _x;
+	}
+	function getX() public view returns (uint) {
+		return x;
+	}
+}
+
+contract B {
+	A a;
+	address immutable owner;
+	constructor() {
+		owner = msg.sender;
+		a = new A();
+	}
+	function g() public {
+		require(msg.sender == owner);
+		a.setX(42);
+	}
+	function getX() public view returns (uint) {
+		return a.getX();
+	}
+}
+
+contract C {
+	B b;
+	constructor() {
+		b = new B();
+		assert(b.getX() == 0); // should hold
+	}
+	function f() public view {
+		assert(b.getX() == 0); // should fail
+	}
+	function h() public {
+		b.g();
+	}
+}
+// ====
+// SMTContract: C
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// ----
+// Warning 6328: (601-622): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol

@@ -0,0 +1,16 @@
+contract C {
+	uint x;
+	function i() public { ++x; }
+	function f() public {
+		x = 0;
+		this.i();
+		assert(x == 1); // should hold in trusted mode
+		assert(x != 1); // should fail
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTTargets: assert
+// ----
+// Warning 6328: (147-161): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n    C.i() -- trusted external call

test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_2.sol

@@ -0,0 +1,16 @@
+contract C {
+	uint x;
+	function i() public { ++x; }
+	function f() public {
+		x = 0;
+		((this)).i();
+		assert(x == 1); // should hold in trusted mode
+		assert(x != 1); // should fail
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTTargets: assert
+// ----
+// Warning 6328: (151-165): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_3.sol

@@ -0,0 +1,17 @@
+contract C {
+	uint x;
+	function i() public { ++x; }
+	function f() public {
+		x = 0;
+		C c = this;
+		c.i();
+		assert(x == 1); // should hold in trusted mode
+		assert(x != 1); // should fail
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTTargets: assert
+// ----
+// Warning 6328: (158-172): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure_trusted.sol

@@ -0,0 +1,33 @@
+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() {
+		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);
+	}
+}
+// ====
+// SMTContract: C
+// SMTEngine: all
+// SMTExtCalls: trusted
+// ----
+// Info 1180: Contract invariant(s) for :C:\n((sig_1 <= 0) && (sig_2 <= 0))\nReentrancy property(ies) for :Crypto:\n(<errorCode> = 0)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(prevOwner == owner)\n<errorCode> = 3 -> Assertion failed at assert(sig_1 == sig_2)\n

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2_trusted.sol

@@ -0,0 +1,47 @@
+contract State {
+	C c;
+	constructor(C _c) {
+		c = _c;
+	}
+	function f() public view returns (uint) {
+		return c.g();
+	}
+}
+
+contract C {
+	address owner;
+	uint y;
+	uint z;
+	State s;
+	bool insidef;
+
+	constructor() {
+		owner = msg.sender;
+		s = new State(this);
+	}
+
+	function zz() public {
+		require(insidef);
+		z = 3;
+	}
+
+	function f() public {
+		require(!insidef);
+		address prevOwner = owner;
+		insidef = true;
+		s.f();
+		assert(z == y);
+		assert(prevOwner == owner);
+		insidef = false;
+	}
+
+	function g() public view returns (uint) {
+		return y;
+	}
+}
+// ====
+// SMTContract: C
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// ----
+// Info 1180: Contract invariant(s) for :C:\n((y <= 0) && (insidef || (z <= 0)))\nReentrancy property(ies) for :State:\n(<errorCode> = 0)\n<errorCode> = 0 -> no errors\n<errorCode> = 2 -> Assertion failed at assert(z == y)\n<errorCode> = 3 -> Assertion failed at assert(prevOwner == owner)\n

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect_trusted.sol

@@ -0,0 +1,56 @@
+contract Other {
+	C c;
+	constructor(C _c) {
+		c = _c;
+	}
+	function h() public {
+		c.setOwner(address(0));
+	}
+}
+
+contract State {
+	uint x;
+	Other o;
+	C c;
+	constructor(C _c) {
+		c = _c;
+		o = new Other(_c);
+	}
+	function f() public returns (uint) {
+		o.h();
+		return c.g();
+	}
+}
+
+contract C {
+	address owner;
+	uint y;
+	State s;
+
+	constructor() {
+		owner = msg.sender;
+		s = new State(this);
+	}
+
+	function setOwner(address _owner) public {
+		owner = _owner;
+	}
+
+	function f() public {
+		address prevOwner = owner;
+		uint z = s.f();
+		assert(z == y); // should hold
+		assert(prevOwner == owner); // should not hold because of reentrancy
+	}
+
+	function g() public view returns (uint) {
+		return y;
+	}
+}
+// ====
+// SMTContract: C
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// ----
+// Warning 6328: (531-545): CHC: Assertion violation might happen here.
+// Warning 6328: (564-590): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_trusted.sol

@@ -0,0 +1,38 @@
+contract State {
+	C c;
+	constructor(C _c) {
+		c = _c;
+	}
+	function f() public view returns (uint) {
+		return c.g();
+	}
+}
+
+contract C {
+	address owner;
+	uint y;
+	State s;
+
+	constructor() {
+		owner = msg.sender;
+		s = new State(this);
+	}
+
+	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;
+	}
+}
+// ====
+// SMTContract: C
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// ----
+// Warning 6328: (314-328): CHC: Assertion violation might happen here.
+// Info 1180: Reentrancy property(ies) for :State:\n(<errorCode> = 0)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(z == y)\n<errorCode> = 2 -> Assertion failed at assert(prevOwner == owner)\n

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe_trusted.sol

@@ -0,0 +1,43 @@
+contract State {
+	C c;
+	constructor(C _c) {
+		c = _c;
+	}
+	function f() public returns (uint) {
+		c.setOwner(address(0));
+		return c.g();
+	}
+}
+
+contract C {
+	address owner;
+	uint y;
+	State s;
+
+	constructor() {
+		owner = msg.sender;
+		s = new State(this);
+	}
+
+	function setOwner(address _owner) public {
+		owner = _owner;
+	}
+
+	function f() public {
+		address prevOwner = owner;
+		uint z = s.f();
+		assert(z == y); // should hold
+		assert(prevOwner == owner); // should not hold because of reentrancy
+	}
+
+	function g() public view returns (uint) {
+		return y;
+	}
+}
+// ====
+// SMTContract: C
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// ----
+// Warning 6328: (396-410): CHC: Assertion violation might happen here.
+// Warning 6328: (429-455): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol

@@ -0,0 +1,35 @@
+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() {
+		s = new State();
+		owner = msg.sender;
+	}
+
+	function f() public {
+		address prevOwner = owner;
+		y = s.f();
+		z = s.f();
+		assert(prevOwner == owner);
+		assert(y != z);
+	}
+}
+// ====
+// SMTContract: C
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// ----
+// Warning 6328: (385-399): CHC: Assertion violation might happen here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe_trusted.sol

@@ -0,0 +1,40 @@
+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() {
+		owner = msg.sender;
+		s = new State();
+	}
+
+	function setOwner(address _owner) public {
+		owner = _owner;
+	}
+
+	function f() public {
+		address prevOwner = owner;
+		y = s.f();
+		z = s.f();
+		assert(prevOwner == owner);
+		assert(y != z);
+	}
+}
+// ====
+// SMTContract: C
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// ----
+// Warning 6328: (421-447): CHC: Assertion violation might happen here.
+// Warning 6328: (451-465): CHC: Assertion violation might happen here.

test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_correct.sol

@@ -0,0 +1,64 @@
+interface Token {
+	function balanceOf(address _a) external view returns (uint);
+	function transfer(address _to, uint _amt) external;
+}
+
+contract TokenCorrect is Token {
+	mapping (address => uint) balance;
+	constructor(address _a, uint _b) {
+		balance[_a] = _b;
+	}
+	function balanceOf(address _a) public view override returns (uint) {
+		return balance[_a];
+	}
+	function transfer(address _to, uint _amt) public override {
+		require(balance[msg.sender] >= _amt);
+		balance[msg.sender] -= _amt;
+		balance[_to] += _amt;
+	}
+}
+
+contract Test {
+	function property_transfer(address _token, address _to, uint _amt) public {
+		require(_to != address(this));
+
+		TokenCorrect t = TokenCorrect(_token);
+
+		uint xPre = t.balanceOf(address(this));
+		require(xPre >= _amt);
+		uint yPre = t.balanceOf(_to);
+
+		t.transfer(_to, _amt);
+		uint xPost = t.balanceOf(address(this));
+		uint yPost = t.balanceOf(_to);
+
+		assert(xPost == xPre - _amt);
+		assert(yPost == yPre + _amt);
+	}
+
+	function test_concrete() public {
+		TokenCorrect t = new TokenCorrect(address(this), 1000);
+
+		uint b = t.balanceOf(address(this));
+		assert(b == 1000);
+
+		address other = address(0x333);
+		require(address(this) != other);
+
+		uint c = t.balanceOf(other);
+		assert(c == 0);
+
+		t.transfer(other, 100);
+
+		uint d = t.balanceOf(address(this));
+		assert(d == 900);
+
+		uint e = t.balanceOf(other);
+		assert(e == 100);
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTContract: Test
+// SMTTargets: assert

test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_wrong.sol

@@ -0,0 +1,68 @@
+interface Token {
+	function balanceOf(address _a) external view returns (uint);
+	function transfer(address _to, uint _amt) external;
+}
+
+contract TokenWrong is Token {
+	mapping (address => uint) balance;
+	constructor(address _a, uint _b) {
+		balance[_a] = _b;
+	}
+	function balanceOf(address _a) public view override returns (uint) {
+		return balance[_a];
+	}
+	function transfer(address _to, uint _amt) public override {
+		require(balance[msg.sender] >= _amt);
+		// Commented out to make this token implementation wrong.
+		//balance[msg.sender] -= _amt;
+		balance[_to] += _amt;
+	}
+}
+
+contract Test {
+	function property_transfer(address _token, address _to, uint _amt) public {
+		require(_to != address(this));
+
+		TokenWrong t = TokenWrong(_token);
+
+		uint xPre = t.balanceOf(address(this));
+		require(xPre >= _amt);
+		uint yPre = t.balanceOf(_to);
+
+		t.transfer(_to, _amt);
+		uint xPost = t.balanceOf(address(this));
+		uint yPost = t.balanceOf(_to);
+
+		assert(xPost == xPre - _amt); // should fail
+		assert(yPost == yPre + _amt);
+	}
+
+	function test_concrete() public {
+		TokenWrong t = new TokenWrong(address(this), 1000);
+
+		uint b = t.balanceOf(address(this));
+		assert(b == 1000);
+
+		address other = address(0x333);
+		require(address(this) != other);
+
+		uint c = t.balanceOf(other);
+		assert(c == 0);
+
+		t.transfer(other, 100);
+
+		uint d = t.balanceOf(address(this));
+		assert(d == 900); // should fail
+
+		uint e = t.balanceOf(other);
+		assert(e == 100);
+	}
+}
+// ====
+// SMTContract: Test
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTTargets: assert
+// ----
+// Warning 6328: (950-978): CHC: Assertion violation happens here.
+// Warning 6328: (1370-1386): CHC: Assertion violation happens here.