Support Using For

[newcodepusher]

Сan you add support for similar solidity instructions?
solidity using-for

[cd1m0]

Can you clarify what you mean for support for using-for or add a sample that you wish to be supported? When I try to instrument the following sample:

library L {
        function plusOne(uint x) internal pure returns (uint) {
                return x + 1;
        }
}

contract Foo {
        using L for uint;

        /// if_succeeds old(x).plusOne() == x;
        function inc(uint x) public returns (uint) {
                return x + 1;
        }
}

I get the following instrumented code, which seems correct:

pragma solidity 0.8.3;

library L {
    function plusOne(uint x) internal pure returns (uint) {
        return x + 1;
    }
}

contract Foo {
    using L for uint;

    event AssertionFailed(string message);

    struct vars0 {
        uint256 old_0;
    }

    function inc(uint x) public returns (uint RET_0) {
        vars0 memory _v;
        unchecked {
            _v.old_0 = x;
        }
        RET_0 = _original_Foo_inc(x);
        unchecked {
            if (!(_v.old_0.plusOne() == x)) {
                emit AssertionFailed("0: ");
                assert(false);
            }
        }
    }

    function _original_Foo_inc(uint x) private returns (uint) {
        return x + 1;
    }
}
/// Utility contract holding a stack counter
contract __scribble_ReentrancyUtils {
    bool __scribble_out_of_contract = true;
}

[newcodepusher]

Your example works, but this one does not

pragma solidity >=0.6.0 <0.8.0;

library Token {
    function balanceOf(address x) internal pure returns (uint) {
        return 123;
    }
}

contract Foo {
    using Token for address;

    /// if_succeeds x.balanceOf() == 123;
    function balanceOf(address x) public returns (uint) {
        return x.balanceOf();
    }
}

Test.sol:12:36 TypeError: Address type expression x doesn't have a builtin member balanceOf

[cd1m0]

Got it! Thank you for the sample. Will try to fix this promptly

[cd1m0]

The issue is that the typechecking logic below is too aggressive. The same problem would happen if the argument was Foo x instead of address x and we had this.balanceOf() in the expression. Fix coming in shortly, and will be merged in the next release.

https://github.com/ConsenSys/scribble/blob/6e737c9ff7db2e0466825411b86a810a6079f988/src/spec-lang/tc/typecheck.ts#L1559