Modifies specs for libraries with local storage pointers

[hajduakos]

While we can add specs to libraries with local storage pointers, modifies specs are not yet working for them, because they are bound to state variables. Seems to be extendable to function parameters with local storage type, but requires a few hours.

Currently we show a warning that it is ignored:

$ cat Test.sol && solc-verify.py Test.sol --show-warnings
pragma solidity>=0.5.0;

library Test {
    struct S {
        int x;
    }

    /// @notice modifies self.x if y > 0
    function f(S storage self, int y) public {
        if (y > 0) self.x += y;
    }
}

Test.sol:9:5: solc-verify warning: Modifies specification for non-state variable 'self' ignored
solc-verify warning: Balance modifications due to gas consumption or miner rewards are not modeled
Test::f: OK
Test::[implicit_constructor]: OK
No errors found.

[dddejan]

Is there some compelling example for this?

[hajduakos]

https://github.com/OpenZeppelin/openzeppelin-contracts/blob/54182bf31c78fb1b16dfdce40fc9a6a177cb3bca/contracts/access/Roles.sol#L12-L18

We might want to say for add that modifies role.bearer[account] if !role.bearer[account].