diff --git a/test/cmdlineTests/model_checker_targets_all_chc/err b/test/cmdlineTests/model_checker_targets_all_chc/err index 0c04c2f2c9a5..ce494c90aa63 100644 --- a/test/cmdlineTests/model_checker_targets_all_chc/err +++ b/test/cmdlineTests/model_checker_targets_all_chc/err @@ -1,14 +1,9 @@ -Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }("")' 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,14 +51,16 @@ 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. @@ -69,14 +68,16 @@ 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. @@ -84,14 +85,14 @@ 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. diff --git a/test/cmdlineTests/model_checker_targets_all_chc/input.sol b/test/cmdlineTests/model_checker_targets_all_chc/input.sol index 33b5bfab3ff7..0061441c0cf8 100644 --- a/test/cmdlineTests/model_checker_targets_all_chc/input.sol +++ b/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]; } -} \ No newline at end of file +} diff --git a/test/cmdlineTests/model_checker_targets_assert_chc/err b/test/cmdlineTests/model_checker_targets_assert_chc/err index 096773e68ee0..fb4d9fcc598d 100644 --- a/test/cmdlineTests/model_checker_targets_assert_chc/err +++ b/test/cmdlineTests/model_checker_targets_assert_chc/err @@ -1,20 +1,16 @@ -Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }("")' 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); | ^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/model_checker_targets_assert_chc/input.sol b/test/cmdlineTests/model_checker_targets_assert_chc/input.sol index 33b5bfab3ff7..0061441c0cf8 100644 --- a/test/cmdlineTests/model_checker_targets_assert_chc/input.sol +++ b/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]; } -} \ No newline at end of file +} diff --git a/test/cmdlineTests/model_checker_targets_balance_chc/err b/test/cmdlineTests/model_checker_targets_balance_chc/err deleted file mode 100644 index c6d3091d167a..000000000000 --- a/test/cmdlineTests/model_checker_targets_balance_chc/err +++ /dev/null @@ -1,7 +0,0 @@ -Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }("")' instead. - --> input.sol:11:3: - | -11 | a.transfer(x); - | ^^^^^^^^^^ - -Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/cmdlineTests/model_checker_targets_balance_chc/input.sol b/test/cmdlineTests/model_checker_targets_balance_chc/input.sol index 4b521b3deba1..4103252cad56 100644 --- a/test/cmdlineTests/model_checker_targets_balance_chc/input.sol +++ b/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]; diff --git a/test/cmdlineTests/model_checker_targets_constant_condition_chc/err b/test/cmdlineTests/model_checker_targets_constant_condition_chc/err deleted file mode 100644 index 4876e936610a..000000000000 --- a/test/cmdlineTests/model_checker_targets_constant_condition_chc/err +++ /dev/null @@ -1,5 +0,0 @@ -Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }("")' instead. - --> input.sol:11:3: - | -11 | a.transfer(x); - | ^^^^^^^^^^ diff --git a/test/cmdlineTests/model_checker_targets_constant_condition_chc/input.sol b/test/cmdlineTests/model_checker_targets_constant_condition_chc/input.sol index 4b521b3deba1..4103252cad56 100644 --- a/test/cmdlineTests/model_checker_targets_constant_condition_chc/input.sol +++ b/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]; diff --git a/test/cmdlineTests/model_checker_targets_default_all_engines/err b/test/cmdlineTests/model_checker_targets_default_all_engines/err index 763f8f16c5f4..837729abf661 100644 --- a/test/cmdlineTests/model_checker_targets_default_all_engines/err +++ b/test/cmdlineTests/model_checker_targets_default_all_engines/err @@ -1,14 +1,9 @@ -Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }("")' 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,14 +19,16 @@ 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. @@ -39,14 +36,16 @@ 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. @@ -54,18 +53,18 @@ 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: | diff --git a/test/cmdlineTests/model_checker_targets_default_all_engines/input.sol b/test/cmdlineTests/model_checker_targets_default_all_engines/input.sol index ddeb1d125363..40641ad1a012 100644 --- a/test/cmdlineTests/model_checker_targets_default_all_engines/input.sol +++ b/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]; } -} \ No newline at end of file +} diff --git a/test/cmdlineTests/model_checker_targets_default_chc/err b/test/cmdlineTests/model_checker_targets_default_chc/err index d4a342ac0b33..081a389deb65 100644 --- a/test/cmdlineTests/model_checker_targets_default_chc/err +++ b/test/cmdlineTests/model_checker_targets_default_chc/err @@ -1,14 +1,9 @@ -Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }("")' 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,14 +19,16 @@ 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. @@ -39,14 +36,16 @@ 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. @@ -54,14 +53,14 @@ 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. diff --git a/test/cmdlineTests/model_checker_targets_default_chc/input.sol b/test/cmdlineTests/model_checker_targets_default_chc/input.sol index ddeb1d125363..40641ad1a012 100644 --- a/test/cmdlineTests/model_checker_targets_default_chc/input.sol +++ b/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]; } -} \ No newline at end of file +} diff --git a/test/cmdlineTests/model_checker_targets_div_by_zero_chc/err b/test/cmdlineTests/model_checker_targets_div_by_zero_chc/err index 3e00272485e6..b9b84f2917de 100644 --- a/test/cmdlineTests/model_checker_targets_div_by_zero_chc/err +++ b/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: }("")' 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() diff --git a/test/cmdlineTests/model_checker_targets_div_by_zero_chc/input.sol b/test/cmdlineTests/model_checker_targets_div_by_zero_chc/input.sol index 33b5bfab3ff7..0061441c0cf8 100644 --- a/test/cmdlineTests/model_checker_targets_div_by_zero_chc/input.sol +++ b/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]; } -} \ No newline at end of file +} diff --git a/test/cmdlineTests/model_checker_targets_error/input.sol b/test/cmdlineTests/model_checker_targets_error/input.sol index 33b5bfab3ff7..0061441c0cf8 100644 --- a/test/cmdlineTests/model_checker_targets_error/input.sol +++ b/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]; } -} \ No newline at end of file +} diff --git a/test/cmdlineTests/model_checker_targets_out_of_bounds_chc/err b/test/cmdlineTests/model_checker_targets_out_of_bounds_chc/err index 9026ef934dba..cefc673499de 100644 --- a/test/cmdlineTests/model_checker_targets_out_of_bounds_chc/err +++ b/test/cmdlineTests/model_checker_targets_out_of_bounds_chc/err @@ -1,20 +1,16 @@ -Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }("")' instead. - --> input.sol:10:3: - | -10 | a.transfer(x); - | ^^^^^^^^^^ - 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]; | ^^^^^^ diff --git a/test/cmdlineTests/model_checker_targets_out_of_bounds_chc/input.sol b/test/cmdlineTests/model_checker_targets_out_of_bounds_chc/input.sol index 33b5bfab3ff7..0061441c0cf8 100644 --- a/test/cmdlineTests/model_checker_targets_out_of_bounds_chc/input.sol +++ b/test/cmdlineTests/model_checker_targets_out_of_bounds_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]; } -} \ No newline at end of file +} diff --git a/test/cmdlineTests/model_checker_targets_overflow_chc/err b/test/cmdlineTests/model_checker_targets_overflow_chc/err index 178b59a44e73..bbaee177831f 100644 --- a/test/cmdlineTests/model_checker_targets_overflow_chc/err +++ b/test/cmdlineTests/model_checker_targets_overflow_chc/err @@ -1,14 +1,9 @@ -Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }("")' instead. - --> input.sol:10:3: - | -10 | a.transfer(x); - | ^^^^^^^^^^ - Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here. Counterexample: arr = [] a = 0x0 x = 1 +success = false Transaction trace: test.constructor() diff --git a/test/cmdlineTests/model_checker_targets_overflow_chc/input.sol b/test/cmdlineTests/model_checker_targets_overflow_chc/input.sol index 33b5bfab3ff7..0061441c0cf8 100644 --- a/test/cmdlineTests/model_checker_targets_overflow_chc/input.sol +++ b/test/cmdlineTests/model_checker_targets_overflow_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]; } -} \ No newline at end of file +} diff --git a/test/cmdlineTests/model_checker_targets_pop_empty_chc/err b/test/cmdlineTests/model_checker_targets_pop_empty_chc/err index e4c1bbc0effa..78524bd90385 100644 --- a/test/cmdlineTests/model_checker_targets_pop_empty_chc/err +++ b/test/cmdlineTests/model_checker_targets_pop_empty_chc/err @@ -1,20 +1,16 @@ -Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }("")' instead. - --> input.sol:10:3: - | -10 | a.transfer(x); - | ^^^^^^^^^^ - 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(); | ^^^^^^^^^ diff --git a/test/cmdlineTests/model_checker_targets_pop_empty_chc/input.sol b/test/cmdlineTests/model_checker_targets_pop_empty_chc/input.sol index 33b5bfab3ff7..0061441c0cf8 100644 --- a/test/cmdlineTests/model_checker_targets_pop_empty_chc/input.sol +++ b/test/cmdlineTests/model_checker_targets_pop_empty_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]; } -} \ No newline at end of file +} diff --git a/test/cmdlineTests/model_checker_targets_underflow_chc/err b/test/cmdlineTests/model_checker_targets_underflow_chc/err index f9fbf82eec31..f245215584d2 100644 --- a/test/cmdlineTests/model_checker_targets_underflow_chc/err +++ b/test/cmdlineTests/model_checker_targets_underflow_chc/err @@ -1,14 +1,9 @@ -Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }("")' 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() diff --git a/test/cmdlineTests/model_checker_targets_underflow_chc/input.sol b/test/cmdlineTests/model_checker_targets_underflow_chc/input.sol index 33b5bfab3ff7..0061441c0cf8 100644 --- a/test/cmdlineTests/model_checker_targets_underflow_chc/input.sol +++ b/test/cmdlineTests/model_checker_targets_underflow_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]; } -} \ No newline at end of file +} diff --git a/test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/err b/test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/err index f91c067026a8..8388d76eded1 100644 --- a/test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/err +++ b/test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/err @@ -1,14 +1,9 @@ -Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }("")' 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,12 +35,14 @@ 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); | ^^^^^^^^^^^^^ diff --git a/test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/input.sol b/test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/input.sol index 33b5bfab3ff7..0061441c0cf8 100644 --- a/test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/input.sol +++ b/test/cmdlineTests/model_checker_targets_underflow_overflow_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]; } -} \ No newline at end of file +} diff --git a/test/cmdlineTests/model_checker_targets_underflow_overflow_chc/err b/test/cmdlineTests/model_checker_targets_underflow_overflow_chc/err index 44faa5ae8388..5751c9072251 100644 --- a/test/cmdlineTests/model_checker_targets_underflow_overflow_chc/err +++ b/test/cmdlineTests/model_checker_targets_underflow_overflow_chc/err @@ -1,14 +1,9 @@ -Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }("")' 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() diff --git a/test/cmdlineTests/model_checker_targets_underflow_overflow_chc/input.sol b/test/cmdlineTests/model_checker_targets_underflow_overflow_chc/input.sol index 33b5bfab3ff7..0061441c0cf8 100644 --- a/test/cmdlineTests/model_checker_targets_underflow_overflow_chc/input.sol +++ b/test/cmdlineTests/model_checker_targets_underflow_overflow_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]; } -} \ No newline at end of file +} diff --git a/test/cmdlineTests/standard_model_checker_targets_assert_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_assert_chc/input.json index a9a7b3fcdb92..e28a8d2259b1 100644 --- a/test/cmdlineTests/standard_model_checker_targets_assert_chc/input.json +++ b/test/cmdlineTests/standard_model_checker_targets_assert_chc/input.json @@ -11,7 +11,8 @@ --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]; diff --git a/test/cmdlineTests/standard_model_checker_targets_assert_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_assert_chc/output.json index d7cfd4a82c4b..6bdd27918bd2 100644 --- a/test/cmdlineTests/standard_model_checker_targets_assert_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_assert_chc/output.json @@ -1,24 +1,5 @@ { "errors": [ - { - "component": "general", - "errorCode": "9207", - "formattedMessage": "Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead. - --> A:11:7: - | -11 | \t\t\t\t\t\ta.transfer(x); - | \t\t\t\t\t\t^^^^^^^^^^ - -", - "message": "'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead.", - "severity": "warning", - "sourceLocation": { - "end": 234, - "file": "A", - "start": 224 - }, - "type": "Warning" - }, { "component": "general", "errorCode": "6328", @@ -27,14 +8,16 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] test.f(0x0, 1) - --> A:12:7: + a.call{value: x}(\"\") -- untrusted external call + --> A:13:7: | -12 | \t\t\t\t\t\tassert(x > 0); +13 | \t\t\t\t\t\tassert(x > 0); | \t\t\t\t\t\t^^^^^^^^^^^^^ ", @@ -43,16 +26,18 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] -test.f(0x0, 1)", +test.f(0x0, 1) + a.call{value: x}(\"\") -- untrusted external call", "severity": "warning", "sourceLocation": { - "end": 258, + "end": 308, "file": "A", - "start": 245 + "start": 295 }, "type": "Warning" } diff --git a/test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/input.json index 365ca122be50..a7e2be42943c 100644 --- a/test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/input.json +++ b/test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/input.json @@ -11,7 +11,8 @@ --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]; diff --git a/test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/output.json index d6a7b5a4ef07..f047ff70a9eb 100644 --- a/test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/output.json @@ -1,25 +1,4 @@ { - "errors": [ - { - "component": "general", - "errorCode": "9207", - "formattedMessage": "Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead. - --> A:11:7: - | -11 | \t\t\t\t\t\ta.transfer(x); - | \t\t\t\t\t\t^^^^^^^^^^ - -", - "message": "'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead.", - "severity": "warning", - "sourceLocation": { - "end": 234, - "file": "A", - "start": 224 - }, - "type": "Warning" - } - ], "sources": { "A": { "id": 0 diff --git a/test/cmdlineTests/standard_model_checker_targets_default_all_engines/input.json b/test/cmdlineTests/standard_model_checker_targets_default_all_engines/input.json index 0d913f0ba25a..4666e9ecf179 100644 --- a/test/cmdlineTests/standard_model_checker_targets_default_all_engines/input.json +++ b/test/cmdlineTests/standard_model_checker_targets_default_all_engines/input.json @@ -11,7 +11,8 @@ --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]; diff --git a/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json b/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json index 964bcd6c6013..48621ecf5cf3 100644 --- a/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json @@ -1,24 +1,5 @@ { "errors": [ - { - "component": "general", - "errorCode": "9207", - "formattedMessage": "Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead. - --> A:11:7: - | -11 | \t\t\t\t\t\ta.transfer(x); - | \t\t\t\t\t\t^^^^^^^^^^ - -", - "message": "'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead.", - "severity": "warning", - "sourceLocation": { - "end": 234, - "file": "A", - "start": 224 - }, - "type": "Warning" - }, { "component": "general", "errorCode": "4281", @@ -27,6 +8,7 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = false Transaction trace: test.constructor() @@ -43,6 +25,7 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = false Transaction trace: test.constructor() @@ -64,14 +47,16 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] test.f(0x0, 1) - --> A:12:7: + a.call{value: x}(\"\") -- untrusted external call + --> A:13:7: | -12 | \t\t\t\t\t\tassert(x > 0); +13 | \t\t\t\t\t\tassert(x > 0); | \t\t\t\t\t\t^^^^^^^^^^^^^ ", @@ -80,16 +65,18 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] -test.f(0x0, 1)", +test.f(0x0, 1) + a.call{value: x}(\"\") -- untrusted external call", "severity": "warning", "sourceLocation": { - "end": 258, + "end": 308, "file": "A", - "start": 245 + "start": 295 }, "type": "Warning" }, @@ -101,14 +88,16 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] test.f(0x0, 1) - --> A:13:7: + a.call{value: x}(\"\") -- untrusted external call + --> A:14:7: | -13 | \t\t\t\t\t\tarr.pop(); +14 | \t\t\t\t\t\tarr.pop(); | \t\t\t\t\t\t^^^^^^^^^ ", @@ -117,16 +106,18 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] -test.f(0x0, 1)", +test.f(0x0, 1) + a.call{value: x}(\"\") -- untrusted external call", "severity": "warning", "sourceLocation": { - "end": 275, + "end": 325, "file": "A", - "start": 266 + "start": 316 }, "type": "Warning" }, @@ -138,14 +129,16 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] test.f(0x0, 1) - --> A:14:7: + a.call{value: x}(\"\") -- untrusted external call + --> A:15:7: | -14 | \t\t\t\t\t\tarr[x]; +15 | \t\t\t\t\t\tarr[x]; | \t\t\t\t\t\t^^^^^^ ", @@ -154,29 +147,21 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] -test.f(0x0, 1)", +test.f(0x0, 1) + a.call{value: x}(\"\") -- untrusted external call", "severity": "warning", "sourceLocation": { - "end": 289, + "end": 339, "file": "A", - "start": 283 + "start": 333 }, "type": "Warning" }, - { - "component": "general", - "errorCode": "1391", - "formattedMessage": "Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them. - -", - "message": "CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them.", - "severity": "info", - "type": "Info" - }, { "component": "general", "errorCode": "6838", diff --git a/test/cmdlineTests/standard_model_checker_targets_default_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_default_chc/input.json index d030e0388fa0..8a1109646fd1 100644 --- a/test/cmdlineTests/standard_model_checker_targets_default_chc/input.json +++ b/test/cmdlineTests/standard_model_checker_targets_default_chc/input.json @@ -11,7 +11,8 @@ --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]; diff --git a/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json index 5f1f5a9c5537..50ec605bc34b 100644 --- a/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json @@ -1,24 +1,5 @@ { "errors": [ - { - "component": "general", - "errorCode": "9207", - "formattedMessage": "Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead. - --> A:11:7: - | -11 | \t\t\t\t\t\ta.transfer(x); - | \t\t\t\t\t\t^^^^^^^^^^ - -", - "message": "'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead.", - "severity": "warning", - "sourceLocation": { - "end": 234, - "file": "A", - "start": 224 - }, - "type": "Warning" - }, { "component": "general", "errorCode": "4281", @@ -27,6 +8,7 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = false Transaction trace: test.constructor() @@ -43,6 +25,7 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = false Transaction trace: test.constructor() @@ -64,14 +47,16 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] test.f(0x0, 1) - --> A:12:7: + a.call{value: x}(\"\") -- untrusted external call + --> A:13:7: | -12 | \t\t\t\t\t\tassert(x > 0); +13 | \t\t\t\t\t\tassert(x > 0); | \t\t\t\t\t\t^^^^^^^^^^^^^ ", @@ -80,16 +65,18 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] -test.f(0x0, 1)", +test.f(0x0, 1) + a.call{value: x}(\"\") -- untrusted external call", "severity": "warning", "sourceLocation": { - "end": 258, + "end": 308, "file": "A", - "start": 245 + "start": 295 }, "type": "Warning" }, @@ -101,14 +88,16 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] test.f(0x0, 1) - --> A:13:7: + a.call{value: x}(\"\") -- untrusted external call + --> A:14:7: | -13 | \t\t\t\t\t\tarr.pop(); +14 | \t\t\t\t\t\tarr.pop(); | \t\t\t\t\t\t^^^^^^^^^ ", @@ -117,16 +106,18 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] -test.f(0x0, 1)", +test.f(0x0, 1) + a.call{value: x}(\"\") -- untrusted external call", "severity": "warning", "sourceLocation": { - "end": 275, + "end": 325, "file": "A", - "start": 266 + "start": 316 }, "type": "Warning" }, @@ -138,14 +129,16 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] test.f(0x0, 1) - --> A:14:7: + a.call{value: x}(\"\") -- untrusted external call + --> A:15:7: | -14 | \t\t\t\t\t\tarr[x]; +15 | \t\t\t\t\t\tarr[x]; | \t\t\t\t\t\t^^^^^^ ", @@ -154,28 +147,20 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] -test.f(0x0, 1)", +test.f(0x0, 1) + a.call{value: x}(\"\") -- untrusted external call", "severity": "warning", "sourceLocation": { - "end": 289, + "end": 339, "file": "A", - "start": 283 + "start": 333 }, "type": "Warning" - }, - { - "component": "general", - "errorCode": "1391", - "formattedMessage": "Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them. - -", - "message": "CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them.", - "severity": "info", - "type": "Info" } ], "sources": { diff --git a/test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/input.json index 1c7af8d5c1f7..c7476eface2a 100644 --- a/test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/input.json +++ b/test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/input.json @@ -11,7 +11,8 @@ --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]; diff --git a/test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/output.json index e5a54e4c871a..867decb52adf 100644 --- a/test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/output.json @@ -1,24 +1,5 @@ { "errors": [ - { - "component": "general", - "errorCode": "9207", - "formattedMessage": "Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead. - --> A:11:7: - | -11 | \t\t\t\t\t\ta.transfer(x); - | \t\t\t\t\t\t^^^^^^^^^^ - -", - "message": "'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead.", - "severity": "warning", - "sourceLocation": { - "end": 234, - "file": "A", - "start": 224 - }, - "type": "Warning" - }, { "component": "general", "errorCode": "4281", @@ -27,6 +8,7 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = false Transaction trace: test.constructor() @@ -43,6 +25,7 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = false Transaction trace: test.constructor() diff --git a/test/cmdlineTests/standard_model_checker_targets_empty_array/input.json b/test/cmdlineTests/standard_model_checker_targets_empty_array/input.json index cb51e490582a..40ccfcbeb91e 100644 --- a/test/cmdlineTests/standard_model_checker_targets_empty_array/input.json +++ b/test/cmdlineTests/standard_model_checker_targets_empty_array/input.json @@ -11,7 +11,8 @@ --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]; diff --git a/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/input.json index cd0ba6d13594..63ccad902ffb 100644 --- a/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/input.json +++ b/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/input.json @@ -11,7 +11,8 @@ --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]; diff --git a/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/output.json index ecb01eac357d..80d919066305 100644 --- a/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/output.json @@ -1,24 +1,5 @@ { "errors": [ - { - "component": "general", - "errorCode": "9207", - "formattedMessage": "Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead. - --> A:11:7: - | -11 | \t\t\t\t\t\ta.transfer(x); - | \t\t\t\t\t\t^^^^^^^^^^ - -", - "message": "'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead.", - "severity": "warning", - "sourceLocation": { - "end": 234, - "file": "A", - "start": 224 - }, - "type": "Warning" - }, { "component": "general", "errorCode": "6368", @@ -27,14 +8,16 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] test.f(0x0, 1) - --> A:14:7: + a.call{value: x}(\"\") -- untrusted external call + --> A:15:7: | -14 | \t\t\t\t\t\tarr[x]; +15 | \t\t\t\t\t\tarr[x]; | \t\t\t\t\t\t^^^^^^ ", @@ -43,16 +26,18 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] -test.f(0x0, 1)", +test.f(0x0, 1) + a.call{value: x}(\"\") -- untrusted external call", "severity": "warning", "sourceLocation": { - "end": 289, + "end": 339, "file": "A", - "start": 283 + "start": 333 }, "type": "Warning" } diff --git a/test/cmdlineTests/standard_model_checker_targets_overflow_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_overflow_chc/input.json index 522d2480ca57..0141cbdb0999 100644 --- a/test/cmdlineTests/standard_model_checker_targets_overflow_chc/input.json +++ b/test/cmdlineTests/standard_model_checker_targets_overflow_chc/input.json @@ -11,7 +11,8 @@ --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]; diff --git a/test/cmdlineTests/standard_model_checker_targets_overflow_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_overflow_chc/output.json index 1b0078d57975..6180cdef7a15 100644 --- a/test/cmdlineTests/standard_model_checker_targets_overflow_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_overflow_chc/output.json @@ -1,24 +1,5 @@ { "errors": [ - { - "component": "general", - "errorCode": "9207", - "formattedMessage": "Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead. - --> A:11:7: - | -11 | \t\t\t\t\t\ta.transfer(x); - | \t\t\t\t\t\t^^^^^^^^^^ - -", - "message": "'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead.", - "severity": "warning", - "sourceLocation": { - "end": 234, - "file": "A", - "start": 224 - }, - "type": "Warning" - }, { "component": "general", "errorCode": "4984", @@ -27,6 +8,7 @@ Counterexample: arr = [] a = 0x0 x = 1 +success = false Transaction trace: test.constructor() @@ -43,6 +25,7 @@ Counterexample: arr = [] a = 0x0 x = 1 +success = false Transaction trace: test.constructor() diff --git a/test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/input.json index 7d2dc69e31eb..430201dbf6f5 100644 --- a/test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/input.json +++ b/test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/input.json @@ -11,7 +11,8 @@ --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]; diff --git a/test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/output.json index 6ac6acd960f4..ee0e0a6efe72 100644 --- a/test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/output.json @@ -1,24 +1,5 @@ { "errors": [ - { - "component": "general", - "errorCode": "9207", - "formattedMessage": "Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead. - --> A:11:7: - | -11 | \t\t\t\t\t\ta.transfer(x); - | \t\t\t\t\t\t^^^^^^^^^^ - -", - "message": "'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead.", - "severity": "warning", - "sourceLocation": { - "end": 234, - "file": "A", - "start": 224 - }, - "type": "Warning" - }, { "component": "general", "errorCode": "2529", @@ -27,14 +8,16 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] test.f(0x0, 1) - --> A:13:7: + a.call{value: x}(\"\") -- untrusted external call + --> A:14:7: | -13 | \t\t\t\t\t\tarr.pop(); +14 | \t\t\t\t\t\tarr.pop(); | \t\t\t\t\t\t^^^^^^^^^ ", @@ -43,16 +26,18 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] -test.f(0x0, 1)", +test.f(0x0, 1) + a.call{value: x}(\"\") -- untrusted external call", "severity": "warning", "sourceLocation": { - "end": 275, + "end": 325, "file": "A", - "start": 266 + "start": 316 }, "type": "Warning" } diff --git a/test/cmdlineTests/standard_model_checker_targets_underflow_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_underflow_chc/input.json index ca33d2fdcc66..e590fcd4d888 100644 --- a/test/cmdlineTests/standard_model_checker_targets_underflow_chc/input.json +++ b/test/cmdlineTests/standard_model_checker_targets_underflow_chc/input.json @@ -11,7 +11,8 @@ --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]; diff --git a/test/cmdlineTests/standard_model_checker_targets_underflow_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_underflow_chc/output.json index 67218582ba8f..373646fa7002 100644 --- a/test/cmdlineTests/standard_model_checker_targets_underflow_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_underflow_chc/output.json @@ -1,24 +1,5 @@ { "errors": [ - { - "component": "general", - "errorCode": "9207", - "formattedMessage": "Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead. - --> A:11:7: - | -11 | \t\t\t\t\t\ta.transfer(x); - | \t\t\t\t\t\t^^^^^^^^^^ - -", - "message": "'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead.", - "severity": "warning", - "sourceLocation": { - "end": 234, - "file": "A", - "start": 224 - }, - "type": "Warning" - }, { "component": "general", "errorCode": "3944", @@ -27,6 +8,7 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = false Transaction trace: test.constructor() @@ -43,6 +25,7 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = false Transaction trace: test.constructor() diff --git a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/input.json index 50f0e82dc583..6d4ad0c74a50 100644 --- a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/input.json +++ b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/input.json @@ -11,7 +11,8 @@ --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]; diff --git a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/output.json index 8f28e7961574..0ab2d1d9884e 100644 --- a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_chc/output.json @@ -1,24 +1,5 @@ { "errors": [ - { - "component": "general", - "errorCode": "9207", - "formattedMessage": "Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead. - --> A:11:7: - | -11 | \t\t\t\t\t\ta.transfer(x); - | \t\t\t\t\t\t^^^^^^^^^^ - -", - "message": "'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead.", - "severity": "warning", - "sourceLocation": { - "end": 234, - "file": "A", - "start": 224 - }, - "type": "Warning" - }, { "component": "general", "errorCode": "3944", @@ -27,6 +8,7 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = false Transaction trace: test.constructor() @@ -43,6 +25,7 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = false Transaction trace: test.constructor() @@ -64,6 +47,7 @@ Counterexample: arr = [] a = 0x0 x = 1 +success = false Transaction trace: test.constructor() @@ -80,6 +64,7 @@ Counterexample: arr = [] a = 0x0 x = 1 +success = false Transaction trace: test.constructor() @@ -101,14 +86,16 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] test.f(0x0, 1) - --> A:12:7: + a.call{value: x}(\"\") -- untrusted external call + --> A:13:7: | -12 | \t\t\t\t\t\tassert(x > 0); +13 | \t\t\t\t\t\tassert(x > 0); | \t\t\t\t\t\t^^^^^^^^^^^^^ ", @@ -117,16 +104,18 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = true Transaction trace: test.constructor() State: arr = [] -test.f(0x0, 1)", +test.f(0x0, 1) + a.call{value: x}(\"\") -- untrusted external call", "severity": "warning", "sourceLocation": { - "end": 258, + "end": 308, "file": "A", - "start": 245 + "start": 295 }, "type": "Warning" } diff --git a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/input.json b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/input.json index 9fc834fd860f..a03420305891 100644 --- a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/input.json +++ b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/input.json @@ -11,7 +11,8 @@ --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]; diff --git a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/output.json index 97442455c0b8..44c3d234085e 100644 --- a/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_underflow_overflow_chc/output.json @@ -1,24 +1,5 @@ { "errors": [ - { - "component": "general", - "errorCode": "9207", - "formattedMessage": "Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead. - --> A:11:7: - | -11 | \t\t\t\t\t\ta.transfer(x); - | \t\t\t\t\t\t^^^^^^^^^^ - -", - "message": "'transfer' is deprecated and scheduled for removal. Use 'call{value: }(\"\")' instead.", - "severity": "warning", - "sourceLocation": { - "end": 234, - "file": "A", - "start": 224 - }, - "type": "Warning" - }, { "component": "general", "errorCode": "3944", @@ -27,6 +8,7 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = false Transaction trace: test.constructor() @@ -43,6 +25,7 @@ Counterexample: arr = [] a = 0x0 x = 0 +success = false Transaction trace: test.constructor() @@ -64,6 +47,7 @@ Counterexample: arr = [] a = 0x0 x = 1 +success = false Transaction trace: test.constructor() @@ -80,6 +64,7 @@ Counterexample: arr = [] a = 0x0 x = 1 +success = false Transaction trace: test.constructor() diff --git a/test/cmdlineTests/standard_model_checker_targets_wrong_target_types/input.json b/test/cmdlineTests/standard_model_checker_targets_wrong_target_types/input.json index a89271975cac..3e8b7414f08f 100644 --- a/test/cmdlineTests/standard_model_checker_targets_wrong_target_types/input.json +++ b/test/cmdlineTests/standard_model_checker_targets_wrong_target_types/input.json @@ -11,7 +11,8 @@ --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]; diff --git a/test/cmdlineTests/standard_model_checker_targets_wrong_target_types_2/input.json b/test/cmdlineTests/standard_model_checker_targets_wrong_target_types_2/input.json index 136ce0978f91..0f450668dd76 100644 --- a/test/cmdlineTests/standard_model_checker_targets_wrong_target_types_2/input.json +++ b/test/cmdlineTests/standard_model_checker_targets_wrong_target_types_2/input.json @@ -11,7 +11,8 @@ --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]; diff --git a/test/cmdlineTests/standard_model_checker_targets_wrong_targets/input.json b/test/cmdlineTests/standard_model_checker_targets_wrong_targets/input.json index 1788fb6d5508..a2f3606757b4 100644 --- a/test/cmdlineTests/standard_model_checker_targets_wrong_targets/input.json +++ b/test/cmdlineTests/standard_model_checker_targets_wrong_targets/input.json @@ -11,7 +11,8 @@ --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]; diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol b/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol index 75a02b7b5179..52012d9f348b 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol @@ -5,7 +5,8 @@ contract C { } function f(address payable a, uint x) public { require(address(this).balance >= x); - a.transfer(x); + (bool success, ) = a.call{value: x}(""); + require(success); } function inv() public view { // If only looking at `f`, it looks like this.balance always decreases. @@ -18,5 +19,3 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 9207: (160-170): 'transfer' is deprecated and scheduled for removal. Use 'call{value: }("")' instead. -// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.