I encountered this issue when translating a contract that calls the ERC20 transfer function. In the boogie output, rather than calling the corresponding function, Verisol instead treats the call as a transfer to send funds. This is related to #157, but Verisol does not raise any errors (such as function overloading disallowed) even though the boogie output produced has a syntax error. The issue can easily be replicated with the following code:
pragma solidity >=0.5.0;
import "./ERC20.sol";
contract Test {
constructor(ERC20 token) public {
token.transfer(msg.sender, 1);
}
}
shuvendu-lahiri
commented
4 years ago
I encountered this issue when translating a contract that calls the ERC20 transfer function. In the boogie output, rather than calling the corresponding function, Verisol instead treats the call as a transfer to send funds. This is related to #157, but Verisol does not raise any errors (such as function overloading disallowed) even though the boogie output produced has a syntax error. The issue can easily be replicated with the following code:
pragma solidity >=0.5.0;
import "./ERC20.sol";
contract Test { constructor(ERC20 token) public { token.transfer(msg.sender, 1); } }