Open hajduakos opened 4 years ago
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
.
Bug that might be related https://github.com/ethereum/solidity/issues/9947
I've fixed the test case, but the issue of inheriting the specs is very complicated and needs to be discussed.
basic/ExplicitScopings.sol
giveswhere
y
is the return value of the annotated function