Replace transfer (deprecated) occurrences with call in smt tests

test/cmdlineTests/model_checker_targets_all_chc/err

@@ -1,14 +1,9 @@
-Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: <amount>}("")' instead.
-  --> input.sol:10:3:
-   |
-10 | 		a.transfer(x);
-   | 		^^^^^^^^^^
-
 Warning: CHC: Underflow (resulting value less than 0) happens here.
 Counterexample:
 arr = []
 a = 0x0
 x = 0
+success = false
 
 Transaction trace:
 test.constructor()
@@ -24,6 +19,7 @@ Counterexample:
 arr = []
 a = 0x0
 x = 1
+success = false
 
 Transaction trace:
 test.constructor()
@@ -39,6 +35,7 @@ Counterexample:
 arr = []
 a = 0x0
 x = 0
+success = false
 
 Transaction trace:
 test.constructor()
@@ -54,44 +51,48 @@ Counterexample:
 arr = []
 a = 0x0
 x = 0
+success = true
 
 Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0x0, 1)
-  --> input.sol:11:3:
+    a.call{value: x}("") -- untrusted external call
+  --> input.sol:12:3:
    |
-11 | 		assert(x > 0);
+12 | 		assert(x > 0);
    | 		^^^^^^^^^^^^^
 
 Warning: CHC: Empty array "pop" happens here.
 Counterexample:
 arr = []
 a = 0x0
 x = 0
+success = true
 
 Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0x0, 1)
-  --> input.sol:12:3:
+    a.call{value: x}("") -- untrusted external call
+  --> input.sol:13:3:
    |
-12 | 		arr.pop();
+13 | 		arr.pop();
    | 		^^^^^^^^^
 
 Warning: CHC: Out of bounds access happens here.
 Counterexample:
 arr = []
 a = 0x0
 x = 0
+success = true
 
 Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0x0, 1)
-  --> input.sol:13:3:
+    a.call{value: x}("") -- untrusted external call
+  --> input.sol:14:3:
    |
-13 | 		arr[x];
+14 | 		arr[x];
    | 		^^^^^^
-
-Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/cmdlineTests/model_checker_targets_all_chc/input.sol

@@ -7,9 +7,10 @@ contract test {
 		--x;
 		x + type(uint).max;
 		2 / x;
-		a.transfer(x);
+		(bool success, ) = a.call{value: x}("");
+		require(success);
 		assert(x > 0);
 		arr.pop();
 		arr[x];
     }
-}
+}

test/cmdlineTests/model_checker_targets_assert_chc/err

@@ -1,20 +1,16 @@
-Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: <amount>}("")' instead.
-  --> input.sol:10:3:
-   |
-10 | 		a.transfer(x);
-   | 		^^^^^^^^^^
-
 Warning: CHC: Assertion violation happens here.
 Counterexample:
 arr = []
 a = 0x0
 x = 0
+success = true
 
 Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0x0, 1)
-  --> input.sol:11:3:
+    a.call{value: x}("") -- untrusted external call
+  --> input.sol:12:3:
    |
-11 | 		assert(x > 0);
+12 | 		assert(x > 0);
    | 		^^^^^^^^^^^^^

test/cmdlineTests/model_checker_targets_assert_chc/input.sol

@@ -7,9 +7,10 @@ contract test {
 		--x;
 		x + type(uint).max;
 		2 / x;
-		a.transfer(x);
+		(bool success, ) = a.call{value: x}("");
+		require(success);
 		assert(x > 0);
 		arr.pop();
 		arr[x];
     }
-}
+}

test/cmdlineTests/model_checker_targets_balance_chc/input.sol

@@ -8,7 +8,8 @@ contract test {
 		--x;
 		x + type(uint).max;
 		2 / x;
-		a.transfer(x);
+		(bool success, ) = a.call{value: x}("");
+		require(success);
 		assert(x > 0);
 		arr.pop();
 		arr[x];

test/cmdlineTests/model_checker_targets_constant_condition_chc/input.sol

@@ -8,7 +8,8 @@ contract test {
 		--x;
 		x + type(uint).max;
 		2 / x;
-		a.transfer(x);
+		(bool success, ) = a.call{value: x}("");
+		require(success);
 		assert(x > 0);
 		arr.pop();
 		arr[x];

test/cmdlineTests/model_checker_targets_default_all_engines/err

@@ -1,14 +1,9 @@
-Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: <amount>}("")' instead.
-  --> input.sol:10:3:
-   |
-10 | 		a.transfer(x);
-   | 		^^^^^^^^^^
-
 Warning: CHC: Division by zero happens here.
 Counterexample:
 arr = []
 a = 0x0
 x = 0
+success = false
 
 Transaction trace:
 test.constructor()
@@ -24,48 +19,52 @@ Counterexample:
 arr = []
 a = 0x0
 x = 0
+success = true
 
 Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0x0, 1)
-  --> input.sol:11:3:
+    a.call{value: x}("") -- untrusted external call
+  --> input.sol:12:3:
    |
-11 | 		assert(x > 0);
+12 | 		assert(x > 0);
    | 		^^^^^^^^^^^^^
 
 Warning: CHC: Empty array "pop" happens here.
 Counterexample:
 arr = []
 a = 0x0
 x = 0
+success = true
 
 Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0x0, 1)
-  --> input.sol:12:3:
+    a.call{value: x}("") -- untrusted external call
+  --> input.sol:13:3:
    |
-12 | 		arr.pop();
+13 | 		arr.pop();
    | 		^^^^^^^^^
 
 Warning: CHC: Out of bounds access happens here.
 Counterexample:
 arr = []
 a = 0x0
 x = 0
+success = true
 
 Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0x0, 1)
-  --> input.sol:13:3:
+    a.call{value: x}("") -- untrusted external call
+  --> input.sol:14:3:
    |
-13 | 		arr[x];
+14 | 		arr[x];
    | 		^^^^^^
 
-Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
-
 Warning: BMC: Condition is always true.
  --> input.sol:6:11:
   |

test/cmdlineTests/model_checker_targets_default_all_engines/input.sol

@@ -7,9 +7,10 @@ contract test {
 		--x;
 		x + type(uint).max;
 		2 / x;
-		a.transfer(x);
+		(bool success, ) = a.call{value: x}("");
+		require(success);
 		assert(x > 0);
 		arr.pop();
 		arr[x];
 	}
-}
+}

test/cmdlineTests/model_checker_targets_default_chc/err

@@ -1,14 +1,9 @@
-Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: <amount>}("")' instead.
-  --> input.sol:10:3:
-   |
-10 | 		a.transfer(x);
-   | 		^^^^^^^^^^
-
 Warning: CHC: Division by zero happens here.
 Counterexample:
 arr = []
 a = 0x0
 x = 0
+success = false
 
 Transaction trace:
 test.constructor()
@@ -24,44 +19,48 @@ Counterexample:
 arr = []
 a = 0x0
 x = 0
+success = true
 
 Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0x0, 1)
-  --> input.sol:11:3:
+    a.call{value: x}("") -- untrusted external call
+  --> input.sol:12:3:
    |
-11 | 		assert(x > 0);
+12 | 		assert(x > 0);
    | 		^^^^^^^^^^^^^
 
 Warning: CHC: Empty array "pop" happens here.
 Counterexample:
 arr = []
 a = 0x0
 x = 0
+success = true
 
 Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0x0, 1)
-  --> input.sol:12:3:
+    a.call{value: x}("") -- untrusted external call
+  --> input.sol:13:3:
    |
-12 | 		arr.pop();
+13 | 		arr.pop();
    | 		^^^^^^^^^
 
 Warning: CHC: Out of bounds access happens here.
 Counterexample:
 arr = []
 a = 0x0
 x = 0
+success = true
 
 Transaction trace:
 test.constructor()
 State: arr = []
 test.f(0x0, 1)
-  --> input.sol:13:3:
+    a.call{value: x}("") -- untrusted external call
+  --> input.sol:14:3:
    |
-13 | 		arr[x];
+14 | 		arr[x];
    | 		^^^^^^
-
-Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/cmdlineTests/model_checker_targets_default_chc/input.sol

@@ -7,9 +7,10 @@ contract test {
 		--x;
 		x + type(uint).max;
 		2 / x;
-		a.transfer(x);
+		(bool success, ) = a.call{value: x}("");
+		require(success);
 		assert(x > 0);
 		arr.pop();
 		arr[x];
 	}
-}
+}

test/cmdlineTests/model_checker_targets_div_by_zero_chc/err

@@ -1,14 +1,9 @@
-Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: <amount>}("")' instead.
-  --> input.sol:10:3:
-   |
-10 | 		a.transfer(x);
-   | 		^^^^^^^^^^
-
 Warning: CHC: Division by zero happens here.
 Counterexample:
 arr = []
 a = 0x0
 x = 0
+success = false
 
 Transaction trace:
 test.constructor()

test/cmdlineTests/model_checker_targets_div_by_zero_chc/input.sol

@@ -7,9 +7,10 @@ contract test {
 		--x;
 		x + type(uint).max;
 		2 / x;
-		a.transfer(x);
+		(bool success, ) = a.call{value: x}("");
+		require(success);
 		assert(x > 0);
 		arr.pop();
 		arr[x];
     }
-}
+}

test/cmdlineTests/model_checker_targets_error/input.sol

@@ -7,9 +7,10 @@ contract test {
 		--x;
 		x + type(uint).max;
 		2 / x;
-		a.transfer(x);
+		(bool success, ) = a.call{value: x}("");
+		require(success);
 		assert(x > 0);
 		arr.pop();
 		arr[x];
     }
-}
+}