Function: withdraw(address token, address to, uint256 amount)

Allows to withdraw assets from the vault.

Inputs

• token

  • Control: Arbitrary.

  • Constraints: None.

  • Impact: Determines the asset to withdraw (ETH corresponds to the special address 0x0).

• to

  • Control: Arbitrary.

  • Constraints: None.

  • Impact: Determines the recipient of the transfer.

• amount

  • Control: Arbitrary.

  • Constraints: amount <= balances[token][msg.sender].

  • Impact: Determines the amount to be withdrawn.

Branches and code coverage (including function calls)

Intended branches

Allows to withdraw ETH.

Allows to withdraw an ERC20 asset.

Negative behavior Reverts if msg.sender balance is insufficient.

Function call analysis

The function has three flows.

Transfer ETH

• rootFunction -> TransferHelper.safeTransferETH(to, amount)

  • What is controllable? to, amount.

  • If return value controllable, how is it used and how can it go wrong? N/A.

  • What happens if it reverts, reenters, or does other unusual control flow? Reverts are bubbled up; reentrancy is prevented with the nonReentrant modifier.

Transfer WETH

• rootFunction -> _wrapAndTransferWETH(to, amount)

  • What is controllable? to, amount.

  • If return value controllable, how is it used and how can it go wrong? N/A.

  • What happens if it reverts, reenters, or does other unusual control flow? Reverts are bubbled up; reentrancy is prevented with the nonReentrant modifier.

• _wrapAndTransferWETH -> IWETH(wETH).deposit{value: amount}()

  • What is controllable? amount.

  • If return value controllable, how is it used and how can it go wrong? N/A.

  • What happens if it reverts, reenters, or does other unusual control flow? Reverts are bubbled up; reentrancy is not a concern (WETH is trusted and immutable).

• _wrapAndTransferWETH -> IWETH(wETH).transfer(to, amount)

  • What is controllable? to, amount.

  • If return value controllable, how is it used and how can it go wrong? N/A.

  • What happens if it reverts, reenters, or does other unusual control flow? Reverts are bubbled up; reentrancy is not a concern (WETH is trusted and immutable).

Transfer other ERC20

• _wrapAndTransferWETH -> TransferHelper.safeTransfer(token, to, amount)

  • What is controllable? token, to, amount.

  • If return value controllable, how is it used and how can it go wrong? N/A.

  • What happens if it reverts, reenters, or does other unusual control flow? Reverts are bubbled up; reentrancy is prevented with the nonReentrant modifier.

• TransferHelper.safeTransfer -> address(token).transfer(to, value)

  • What is controllable? token, to, value.

  • If return value controllable, how is it used and how can it go wrong? The return value must encode bool(true), otherwise execution is reverted.

  • What happens if it reverts, reenters, or does other unusual control flow? Reverts are bubbled up; reentrancy is prevented with the nonReentrant modifier.