Update tests

test/libsolidity/smtCheckerTests/complex/slither/external_function.sol

@@ -84,9 +84,7 @@ contract InternalCall {
 // Warning 2018: (1179-1241): Function state mutability can be restricted to pure
 // Warning 2018: (1247-1309): Function state mutability can be restricted to pure
 // Warning 4588: (681-716): Assertion checker does not yet implement this type of function call.
-// Warning 4588: (727-782): Assertion checker does not yet implement this type of function call.
 // Warning 4588: (854-886): Assertion checker does not yet implement this type of function call.
 // Warning 4588: (681-716): Assertion checker does not yet implement this type of function call.
-// Warning 4588: (727-782): Assertion checker does not yet implement this type of function call.
 // Warning 4588: (854-886): Assertion checker does not yet implement this type of function call.
 // Warning 5729: (1370-1375): BMC does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/external_calls/call_constructor_1.sol

@@ -0,0 +1,11 @@
+contract C {
+	uint x;
+	constructor(address _a) {
+		_a.call("aaaa");
+		assert(x == 0); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 9302: (51-66): Return value of low-level calls not used.

test/libsolidity/smtCheckerTests/external_calls/call_constructor_2.sol

@@ -0,0 +1,14 @@
+contract C {
+	uint x;
+	function f(uint _x) public {
+		x = _x;
+	}
+	constructor(address _a) {
+		_a.call("aaaa");
+		assert(x == 0); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 9302: (94-109): Return value of low-level calls not used.

test/libsolidity/smtCheckerTests/external_calls/call_mutex.sol

@@ -0,0 +1,25 @@
+contract C {
+	uint x;
+
+	bool lock;
+	modifier mutex {
+		require(!lock);
+		lock = true;
+		_;
+		lock = false;
+	}
+
+	function set(uint _x) mutex public {
+		x = _x;
+	}
+
+	function f(address _a) mutex public {
+		uint y = x;
+		_a.call("aaaaa");
+		assert(y == x); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 9302: (218-234): Return value of low-level calls not used.

test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol

@@ -0,0 +1,26 @@
+contract C {
+	uint x;
+
+	bool lock;
+	modifier mutex {
+		require(!lock);
+		lock = true;
+		_;
+		lock = false;
+	}
+
+	function set(uint _x) mutex public {
+		x = _x;
+	}
+
+	function f(address _a) public {
+		uint y = x;
+		_a.call("aaaaa");
+		assert(y == x); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 9302: (212-228): Return value of low-level calls not used.
+// Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, lock = false\n_a = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.f(0)\n    _a.call("aaaaa") -- untrusted external call, synthesized as:\n        C.set(1) -- reentrant call

test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_1.sol

@@ -0,0 +1,17 @@
+contract C {
+	uint x;
+	function s(uint _x) public {
+		x = _x;
+	}
+	function f(address a) public {
+		(bool s, bytes memory data) = a.call("");
+		assert(x == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 2519: (100-106): This declaration shadows an existing declaration.
+// Warning 2072: (100-106): Unused local variable.
+// Warning 2072: (108-125): Unused local variable.
+// Warning 6328: (143-157): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ns = false\ndata = [36, 5, 5, 5, 5, 5]\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.s(1)\nState: x = 1\nC.f(0)\n    a.call("") -- untrusted external call

test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol

@@ -0,0 +1,16 @@
+contract C {
+	uint x;
+	function s(uint _x) public view {
+		x == _x;
+	}
+	function f(address a) public {
+		(bool s, bytes memory data) = a.call("");
+		assert(x == 0); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 2519: (106-112): This declaration shadows an existing declaration.
+// Warning 2072: (106-112): Unused local variable.
+// Warning 2072: (114-131): Unused local variable.

test/libsolidity/smtCheckerTests/external_calls/call_return_1.sol

@@ -0,0 +1,15 @@
+contract C {
+	uint x;
+	function f(address a) public {
+		(bool s, bytes memory data) = a.call("");
+		assert(s); // should fail
+		assert(!s); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 2072: (65-82): Unused local variable.
+// Warning 6328: (100-109): CHC: Assertion violation happens here.
+// Warning 6328: (128-138): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/call_return_2.sol

@@ -0,0 +1,13 @@
+contract C {
+	uint x;
+	function f(address a) public {
+		(bool s, bytes memory data) = a.call("");
+		assert(data.length > 10); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 2072: (57-63): Unused local variable.
+// Warning 6328: (100-124): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/call_safe.sol

@@ -0,0 +1,12 @@
+contract C {
+	uint x;
+	function f(address a) public {
+		(bool s, bytes memory data) = a.call("");
+		assert(x == 0); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 2072: (57-63): Unused local variable.
+// Warning 2072: (65-82): Unused local variable.

test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex.sol

@@ -0,0 +1,25 @@
+contract C {
+	uint x;
+
+	bool lock;
+	modifier mutex {
+		require(!lock);
+		lock = true;
+		_;
+		lock = false;
+	}
+
+	function set(uint _x) mutex public {
+		x = _x;
+	}
+
+	function f(address _a) mutex public {
+		uint y = x;
+		_a.staticcall("aaaaa");
+		assert(y == x); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 9302: (218-240): Return value of low-level calls not used.

test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex_2.sol

@@ -0,0 +1,26 @@
+contract C {
+	uint x;
+
+	bool lock;
+	modifier mutex {
+		require(!lock);
+		lock = true;
+		_;
+		lock = false;
+	}
+
+	function set(uint _x) mutex public {
+		x = _x;
+	}
+
+	function f(address _a) public {
+		uint y = x;
+		_a.staticcall("aaaaa");
+		assert(y == x); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 9302: (212-234): Return value of low-level calls not used.
+// Warning 2018: (164-271): Function state mutability can be restricted to view

test/libsolidity/smtCheckerTests/external_calls/staticcall_reentrancy_view.sol

@@ -0,0 +1,17 @@
+contract C {
+	uint x;
+	function s(uint _x) public view {
+		x == _x;
+	}
+	function f(address a) public {
+		(bool s, bytes memory data) = a.staticcall("");
+		assert(x == 0); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 2519: (106-112): This declaration shadows an existing declaration.
+// Warning 2072: (106-112): Unused local variable.
+// Warning 2072: (114-131): Unused local variable.
+// Warning 2018: (72-188): Function state mutability can be restricted to view

test/libsolidity/smtCheckerTests/file_level/new_operator.sol

@@ -16,5 +16,5 @@ contract D {
 // ----
 // Warning 4588: (78-85): Assertion checker does not yet implement this type of function call.
 // Warning 4588: (78-85): Assertion checker does not yet implement this type of function call.
-// Warning 6328: (133-152): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nD.constructor()\nD.f()\n    test() -- internal call
+// Warning 6328: (133-152): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nD.constructor()\nD.f()\n    test() -- internal call\n        (new C()).x() -- untrusted external call
 // Warning 4588: (78-85): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/functions/getters/function.sol

@@ -15,5 +15,5 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (152-170): CHC: Assertion violation happens here.\nCounterexample:\ng = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: g = 0\nC.f()
-// Warning 6328: (262-278): CHC: Assertion violation happens here.\nCounterexample:\ng = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: g = 0\nC.f()
+// Warning 6328: (152-170): CHC: Assertion violation happens here.\nCounterexample:\ng = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: g = 0\nC.f()\n    e() -- untrusted external call\n    g() -- untrusted external call
+// Warning 6328: (262-278): CHC: Assertion violation happens here.\nCounterexample:\ng = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: g = 0\nC.f()\n    e() -- untrusted external call\n    g() -- untrusted external call\n    e() -- untrusted external call

test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_external.sol

@@ -6,4 +6,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (123-143): CHC: Assertion violation happens here.\nCounterexample:\n\ng = 0\nh = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)
+// Warning 6328: (123-143): CHC: Assertion violation happens here.\nCounterexample:\n\ng = 0\nh = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)\n    g(2) -- untrusted external call\n    h(2) -- untrusted external call

test/libsolidity/smtCheckerTests/types/address_call.sol

@@ -19,9 +19,4 @@ contract C
 // SMTIgnoreCex: yes
 // ----
 // Warning 2072: (191-207): Unused local variable.
-// Warning 4588: (211-223): Assertion checker does not yet implement this type of function call.
 // Warning 6328: (227-242): CHC: Assertion violation happens here.
-// Warning 6328: (246-260): CHC: Assertion violation happens here.
-// Warning 6328: (264-283): CHC: Assertion violation happens here.
-// Warning 6328: (287-311): CHC: Assertion violation happens here.
-// Warning 4588: (211-223): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol

@@ -12,5 +12,3 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 4588: (110-129): Assertion checker does not yet implement this type of function call.
-// Warning 4588: (110-129): Assertion checker does not yet implement this type of function call.