Replace `transfer` (deprecated) occurrences with `call` in smt tests #16291

matheusaaguiar · 2025-11-19T16:15:34Z

transfer is deprecated and will be removed in the next breaking release.
depends on #16174.

cameel

This needs a look from @blishko.

Looks like some of the balance tests actually do depend on properties of transfer() and SMTChecker is not able to prove the same things with call(). We'd need something else to replace it.

Also, some of the CLI tests for specific targets have empty output for those targets, which means we're not actually testing that the things works.

I'm not sure how much of it is actually worth fixing. We plan to deprecate BMC in 0.9 anyway. Some of these apply to CMC though.

cameel · 2025-11-26T16:28:08Z

test/cmdlineTests/model_checker_targets_all_all_engines/err

-  --> input.sol:13:3:
+    a.call{value: x}("") -- untrusted external call
+  --> input.sol:14:3:


Hmm... so transfer() was not treated as an untrusted external call but call() is? Perhaps SMTChecker should treat call() with empty payload and a gas limit specially?

cameel · 2025-11-26T16:29:08Z

test/cmdlineTests/model_checker_targets_all_bmc/err

 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.


Apparently SMTChecker can figure this out with transfer() but not with call()?

cameel · 2025-11-26T16:31:47Z

test/cmdlineTests/model_checker_targets_balance_bmc/err

Looks like SMTChecker can no longer detect insufficient balance when we use call(). Since this is the point of the test, we should replace it with something that actually does trigger this.

Alternatively, we could also keep transfer() in this particular test. There's a chance we'll drop BMC before we drop transfer() and send() anyway.

cameel · 2025-11-26T16:33:35Z

test/cmdlineTests/model_checker_targets_balance_chc/err

Same here, but we're not dropping CHC, so this one needs an actual fix.

cameel · 2025-11-26T16:34:30Z

test/cmdlineTests/model_checker_targets_constant_condition_chc/err

Looks like SMTChecker fails to detect the constant condition here (though it was like this already before this PR).

cameel · 2025-11-26T16:36:39Z

test/cmdlineTests/model_checker_targets_out_of_bounds_bmc/err

Another case where the target is not actually reported.

cameel · 2025-11-26T16:40:18Z

test/cmdlineTests/standard_model_checker_targets_assert_bmc/output.json

            "component": "general",
-            "errorCode": "9207",
-            "formattedMessage": "Warning: 'transfer' is deprecated and scheduled for removal in the next breaking version (0.9). Use 'call{value: <amount>}(\"\")' 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 in the next breaking version (0.9). Use 'call{value: <amount>}(\"\")' instead.",
-            "severity": "warning",
-            "sourceLocation": {
-                "end": 234,
-                "file": "A",
-                "start": 224
-            },
-            "type": "Warning"
-        },
-        {
-            "component": "general",
-            "errorCode": "4661",
-            "formattedMessage": "Warning: BMC: Assertion violation happens here.
-  --> A:12:7:
-   |
-12 | \t\t\t\t\t\tassert(x > 0);
-   | \t\t\t\t\t\t^^^^^^^^^^^^^
-Note: Counterexample:
-  a = 0
-  x = 0
-
-Note: Callstack:
-Note:
-
-",
-            "message": "BMC: Assertion violation happens here.",
-            "secondarySourceLocations": [
-                {
-                    "message": "Counterexample:
-  a = 0
-  x = 0
-"
-                },
-                {
-                    "message": "Callstack:"
-                },
-                {
-                    "message": ""
-                }
-            ],
-            "severity": "warning",
-            "sourceLocation": {
-                "end": 258,
-                "file": "A",
-                "start": 245
-            },
-            "type": "Warning"
-        }
-    ],
-    "sources": {
-        "A": {
-            "id": 0
+            "formattedMessage": "parse error at line 7, column 458: syntax error while parsing object - unexpected string literal; expected '}'",
+            "message": "parse error at line 7, column 458: syntax error while parsing object - unexpected string literal; expected '}'",
+            "severity": "error",
+            "type": "JSONError"
        }


This is not the expected output here. I think you broke it by not escaping the quotes in JSON.

cameel · 2025-11-26T16:43:40Z

test/libsolidity/smtCheckerTests/blockchain_state/transfer_2.sol

 	function shouldHold() public {
 		uint tempAmount = address(this).balance;
-		recipient.transfer(tempAmount);
-		recipient.transfer(amount);
+		(bool success, ) = recipient.call{value: tempAmount}("");
+		require(success);
+		(success, ) = recipient.call{value: amount}("");
+		require(success);
 	}
 }
 // ====
 // SMTEngine: chc
 // ----
-// Warning 9207: (133-151): 'transfer' is deprecated and scheduled for removal in the next breaking version (0.9). Use 'call{value: <amount>}("")' instead.
-// Warning 9207: (167-185): 'transfer' is deprecated and scheduled for removal in the next breaking version (0.9). Use 'call{value: <amount>}("")' instead.
-// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.


This test no longer is proved safe with call().

blishko · 2025-11-26T16:56:25Z

How important is this right now?
I guess we need to implement handling of call with value the same way we now handle transfer?

cameel · 2025-11-26T17:24:22Z

How important is this right now?

We will have to deal with it in some way eventually, because send()/transfer() are going to be removed and these tests will start failing, but it will only happen in 0.9, so it's not urgent at all. It only came up now because in #16174 we're adding deprecation warnings and it seemed straightforward to update these tests. Looks like it's not that straightforward after all :)

I guess we need to implement handling of call with value the same way we now handle transfer?

Another option is also to wait for the PAY opcode and replace it with that. If it gets into Glamsterdam it could even happen before 0.9 ships :)

Maybe just leaving it as is and going back to it when the bultins are actually removed is the best course of action here. But I was just wondering whether you'd still plan to address this properly or if we should rather assume that this will just become irrelevant at some point due to changing plans (deprecations, move to Core Solidity, new tool for verification at Yul level, etc.).

blishko · 2025-11-27T12:35:21Z

I believe it will eventually become irrelevant, but we might need to fix it properly before that.
I can do it before 0.9, but I would prefer to do all the necessary things in one batch.

So I would wait with this a bit to see if the situation is clearer in the future (e.g., the PAY opcode).

cameel · 2025-11-27T16:00:02Z

ok. In that case in this PR we'll just replace the simple cases that cause no issues and leave the ones that do (e.g. the ones that are related to balance or specifically test transfer()) unchanged, to be dealt with later.

matheusaaguiar changed the base branch from develop to deprecation_warnings November 19, 2025 16:15

matheusaaguiar added the has dependencies The PR depends on other PRs that must be merged first label Nov 19, 2025

matheusaaguiar mentioned this pull request Nov 19, 2025

Add deprecation warnings for send(), transfer(), ABI coder v1, contract comparisons, virtual modifiers and memory-safe-assembly comment #16174

Open

matheusaaguiar force-pushed the deprecation_warnings branch from c55108b to d97549f Compare November 19, 2025 16:36

Update smt tests

3b6fdc2

matheusaaguiar force-pushed the update-deprecated-smt-tests branch from 50bc5f0 to 3b6fdc2 Compare November 19, 2025 16:37

cameel reviewed Nov 26, 2025

View reviewed changes

cameel added refactor smt testing 🔨 and removed refactor labels Nov 26, 2025

Replace transfer (deprecated) occurrences with call in smt tests #16291

Are you sure you want to change the base?

Replace transfer (deprecated) occurrences with call in smt tests #16291

Conversation

matheusaaguiar commented Nov 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

cameel left a comment

Choose a reason for hiding this comment

Uh oh!

cameel Nov 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

cameel Nov 26, 2025

Choose a reason for hiding this comment

Uh oh!

cameel Nov 26, 2025

Choose a reason for hiding this comment

Uh oh!

cameel Nov 26, 2025

Choose a reason for hiding this comment

Uh oh!

cameel Nov 26, 2025

Choose a reason for hiding this comment

Uh oh!

cameel Nov 26, 2025

Choose a reason for hiding this comment

Uh oh!

cameel Nov 26, 2025

Choose a reason for hiding this comment

Uh oh!

cameel Nov 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

cameel Nov 26, 2025

Choose a reason for hiding this comment

Uh oh!

blishko commented Nov 26, 2025

Uh oh!

cameel commented Nov 26, 2025

Uh oh!

blishko commented Nov 27, 2025

Uh oh!

cameel commented Nov 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Replace `transfer` (deprecated) occurrences with `call` in smt tests #16291

Replace `transfer` (deprecated) occurrences with `call` in smt tests #16291

matheusaaguiar commented Nov 19, 2025 •

edited

Loading

cameel Nov 26, 2025 •

edited

Loading

cameel Nov 26, 2025 •

edited

Loading