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

Tuple assignments done element wise #41

Closed hajduakos closed 5 years ago

hajduakos commented 5 years ago

Currently, tuple assignments are performed element-wise in a left-to-right order, which gives an incorrect result. Example:

pragma solidity >=0.5.0;

contract Swap {
    uint a;
    uint b;

    function() external payable {
        uint x = 1;
        uint y = 2;
        (x, y) = (y, x);
        assert(x == 2);
        assert(y == 1);

        a = 1;
        b = 2;
        (a, b) = (b, a);
        assert(a == 2);
        assert(b == 1);
    }
}

The assertions should hold in this case, but fail in solc-verify.

hajduakos commented 5 years ago

Fixed in 9185d2d and b4e41d4