Update tests

Author: Leo Alt

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.