Inheritance of specs in overloaded functions

[hajduakos]

basic/ExplicitScopings.sol gives

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

======= test/solc-verify/basic/ExplicitScopings.sol =======
Annotation:1:10: solc-verify error: Undeclared identifier.
x + 1 == y 
         ^

where y is the return value of the annotated function

[dddejan]

contract A {
    /** @notice postcondition x + 1 == y */
    function g(int x) public pure virtual returns (int y) {
        return A.f(x); // Explicit scoping with current contract name
    }
}

contract B is A {
    function g(int x) public pure override returns (int) {
        int z = A.g(x); // Explicit scoping with base name
        assert(z == x + 1);
        return z;
    }
}

This is happening because B::g overrides A::g and seems to inherits the tags (and hence the spec) of A::g.

[dddejan]

Bug that might be related ethereum#9947

[dddejan]

I've fixed the test case, but the issue of inheriting the specs is very complicated and needs to be discussed.