Question on assert violation reports

[jcrreis]

Hello,

I have a contract with a potential gasless transfer of ether to another contract with the following code:

 function pay(uint n, D1 d) public payable {
        
        uint old_balance = address(this).balance;

        address d1 = address(d);
        //payable(d1).send(n);
        (bool sent, ) = d1.call{value: n}("");
        require(sent);

       
        uint actual_balance = address(this).balance;
        assert(actual_balance == old_balance - n);
    }

If we use send we have a potential gasless send if D1 performs a state mutation on his fallback or receive function, however if we use call this code is free from that vulnerability.

When i run mythril through the command line I have the following output, in both cases (if I use send or call):

==== Exception State ====
SWC ID: 110
Severity: Medium
Contract: C
Function name: pay(uint256,address)
PC address: 785
Estimated Gas Usage: 1902 - 36373
An assertion violation was triggered.
It is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).
--------------------
In file: examples/GaslessTransfer/gaslesstransfer.sol:25

assert(actual_balance == old_balance - n)

--------------------
Initial State:

Account: [CREATOR], balance: 0x10000001, nonce:0, storage:{}
Account: [ATTACKER], balance: 0x0, nonce:0, storage:{}

Transaction Sequence:

Caller: [CREATOR], calldata: , value: 0x0
Caller: [SOMEGUY], function: pay(uint256,address), txdata: 0x31cbf5e300000000000000000000000000000000000000000000000000000000000000010000000000000000000000000901d12ebe1b195e5aa8748e62bd7734ae19b51f, value: 0x1

I think this assertion is only violated when we call send, since the transfer can actually fail if D1 performs some complex computation when it receives ether.. Also i'm having trouble reading the transaction trace, what values are actually passed into pay?

Thank you.

[norhh]

Hi @jcrreis, can you paste the full contract (or the smallest code fragment that reproduces this error), I couldn't reproduce it with the single function.