Local storage pointers and inheritance

[hajduakos]

Depending on the target of verification, the postcondition of setB0 might or might not hold.

pragma solidity >=0.5.0;

contract A {
  struct S {
      int x;
  }
  function setA0(S storage s_ptr) internal {
    s_ptr.x = 0;
  }
}

contract B is A {
  S s;
  /// @notice postcondition s.x == 0
  function setB0(S storage s_ptr) internal {
    setA0(s_ptr);
  }
}

contract LocalStorageSpec is B {
  S s;
  function setC0(S storage s_ptr) internal {
    setB0(s_ptr);
  }
  function() external payable {
    setC0(s);
    assert(s.x == 0);
  }

}

If we only target B without C, it should hold. Otherwise it should not.