SRI-CSL / solidity

This is solc-verify, a modular verifier for Solidity.
https://github.com/SRI-CSL/solidity/blob/boogie/SOLC-VERIFY-README.md
GNU General Public License v3.0
50 stars 14 forks source link

[0.7] Support for function options (gas, value, salt, ...) is broken (FunctionCallOptions) #163

Closed dddejan closed 3 years ago

dddejan commented 3 years ago
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.7.0;
contract FunctionOptions {
    function withdraw(uint256 amount) public {
        (bool ok, ) = msg.sender.call{value: amount}("");
        if (!ok) revert();
    }
}
solc-verify.py FunctionOptions.sol 
Error while running compiler, details:
Warning: This is a pre-release compiler version, please do not use it in production.

======= Converting to Boogie IVL =======

======= FunctionOptions.sol =======
solc-verify internal exception: Unhandled node (unknown)
Details:
/solidity/libsolidity/boogie/ASTBoogieExpressionConverter.cpp(1626): Throw in function virtual bool solidity::frontend::ASTBoogieExpressionConverter::visitNode(const solidity::frontend::ASTNode &)
Dynamic exception type: boost::wrapexcept<solidity::langutil::InternalCompilerError>
std::exception::what: Unhandled node (unknown)
[solidity::util::tag_comment*] = Unhandled node (unknown)

The unhandled node is FunctionCallOptions

hajduakos commented 3 years ago

Fixed in b16869c396d3b04937a4bba4ccbff34515f95f01 We support value, and ignore the rest (e.g., gas) with a warning, just as previously. This is actually a nice improvement in the compiler, which made our code a bit cleaner.