Specifying library with storage references

[dddejan]

While we can specify library functions if the function operates on storage references the encoding will fail.

pragma solidity >=0.5.0;

library L1 {
    /// @notice postcondition result >= 0
    function square(int x) public pure returns (int result) {
        return x*x;
    }
}

library L2 {
    struct S { int a; }

    /// @notice postcondition self.a >= 0
    function square(S storage self) public {
        self.a *= self.a;
    }
}

In above example, L1 passes OK, while L2 fails with

solc-verify.py Issue80.sol --output .
Error while running compiler, details:
Warning: This is a pre-release compiler version, please do not use it in production.

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

======= Issue80.sol =======
Issue80.sol:15:9: solc-verify error: Nothing to unpack, perhaps there are no instances of the type
        self.a *= self.a;
        ^--^
Issue80.sol:15:9: solc-verify error: Nothing to unpack, perhaps there are no instances of the type
        self.a *= self.a;
        ^--^
Issue80.sol:15:19: solc-verify error: Nothing to unpack, perhaps there are no instances of the type
        self.a *= self.a;
                  ^--^
Issue80.sol:15:19: solc-verify error: Nothing to unpack, perhaps there are no instances of the type
        self.a *= self.a;
                  ^--^
Annotation:1:1: solc-verify error: Nothing to unpack, perhaps there are no instances of the type
self.a >= 0
^--^
Annotation:1:1: solc-verify error: Nothing to unpack, perhaps there are no instances of the type
self.a >= 0
^--^
Issue80.sol:14:5: solc-verify warning: Errors while translating function body, will be skipped
    function square(S storage self) public {
    ^ (Relevant source part starts here and spans across multiple lines).
Issue80.sol:14:5: solc-verify error: Error(s) while processing annotation for node
    function square(S storage self) public {
    ^ (Relevant source part starts here and spans across multiple lines).

[hajduakos]

Done in 6e51436cb725abe30553388492bf5ed612fc622b by adding a default array to point to.