Update smt tests

Author: matheusaaguiar

test/cmdlineTests/model_checker_targets_all_all_engines/err

@@ -1,14 +1,9 @@
-Warning: 'transfer' is deprecated and scheduled for removal in the next breaking version (0.9). 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,48 +51,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_all_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_all_bmc/err

@@ -1,9 +1,3 @@
-Warning: 'transfer' is deprecated and scheduled for removal in the next breaking version (0.9). Use 'call{value: <amount>}("")' instead.
-  --> input.sol:10:3:
-   |
-10 | 		a.transfer(x);
-   | 		^^^^^^^^^^
-
 Warning: BMC: Condition is always true.
  --> input.sol:6:11:
   |
@@ -19,10 +13,12 @@ Warning: BMC: Underflow (resulting value less than 0) happens here.
 Note: Counterexample:
   <result> = (- 1)
   a = 0
+  success = false
   x = 0
 
 Note: Callstack:
-Note:
+Note: 
+Note that external function calls are not inlined, even if the source code of the function is available. This is due to the possibility that the actual called contract has the same ABI but implements the function differently.
 
 Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
  --> input.sol:8:3:
@@ -32,10 +28,12 @@ Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 Note: Counterexample:
   <result> = 2**256
   a = 0
+  success = false
   x = 1
 
 Note: Callstack:
-Note:
+Note: 
+Note that external function calls are not inlined, even if the source code of the function is available. This is due to the possibility that the actual called contract has the same ABI but implements the function differently.
 
 Warning: BMC: Division by zero happens here.
  --> input.sol:9:3:
@@ -45,31 +43,23 @@ Warning: BMC: Division by zero happens here.
 Note: Counterexample:
   <result> = 0
   a = 0
+  success = false
   x = 0
 
 Note: Callstack:
-Note:
-
-Warning: BMC: Insufficient funds happens here.
-  --> input.sol:10:3:
-   |
-10 | 		a.transfer(x);
-   | 		^^^^^^^^^^^^^
-Note: Counterexample:
-  a = 0
-  x = 0
-
-Note: Callstack:
-Note:
+Note: 
+Note that external function calls are not inlined, even if the source code of the function is available. This is due to the possibility that the actual called contract has the same ABI but implements the function differently.
 
 Warning: BMC: Assertion violation happens here.
-  --> input.sol:11:3:
+  --> input.sol:12:3:
    |
-11 | 		assert(x > 0);
+12 | 		assert(x > 0);
    | 		^^^^^^^^^^^^^
 Note: Counterexample:
   a = 0
+  success = true
   x = 0
 
 Note: Callstack:
-Note:
+Note: 
+Note that external function calls are not inlined, even if the source code of the function is available. This is due to the possibility that the actual called contract has the same ABI but implements the function differently.

test/cmdlineTests/model_checker_targets_all_bmc/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_all_chc/err

@@ -1,14 +1,9 @@
-Warning: 'transfer' is deprecated and scheduled for removal in the next breaking version (0.9). 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_bmc/err

@@ -1,17 +1,13 @@
-Warning: 'transfer' is deprecated and scheduled for removal in the next breaking version (0.9). Use 'call{value: <amount>}("")' instead.
-  --> input.sol:10:3:
-   |
-10 | 		a.transfer(x);
-   | 		^^^^^^^^^^
-
 Warning: BMC: Assertion violation happens here.
-  --> input.sol:11:3:
+  --> input.sol:12:3:
    |
-11 | 		assert(x > 0);
+12 | 		assert(x > 0);
    | 		^^^^^^^^^^^^^
 Note: Counterexample:
   a = 0
+  success = true
   x = 0
 
 Note: Callstack:
-Note:
+Note: 
+Note that external function calls are not inlined, even if the source code of the function is available. This is due to the possibility that the actual called contract has the same ABI but implements the function differently.

test/cmdlineTests/model_checker_targets_assert_bmc/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 in the next breaking version (0.9). 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];
     }
-}
+}