microsoft / verisol

A formal verifier and analysis tool for Solidity Smart Contracts
Other
245 stars 46 forks source link

Solidity Casting between address and int types #247

Closed stephensj2 closed 4 years ago

stephensj2 commented 4 years ago

When one casts from an address to a uint (or vice versa) boogie produces the following error: Error: mismatched types in assignment command (cannot assign Ref to int)

This can be reproduced as follows:

Code:

pragma solidity >=0.5.0;

contract Test {
    function test(address addr) public pure returns (uint) {
        uint addrInt = uint(addr);
        return addrInt;
    }
}

Commands: VeriSol test.sol Test /noChk /noprf boogie /noVerify __SolToBoogieTest_out.bpl