docs: @Requires({
      "oldLocals != null",
      "extraIndex >= -1"
    })
    @Ensures("result >= 0")
    protected int getPostDescOffset(List<Integer> oldLocals, int extraIndex) {
      int off = 0;
      if (extraIndex != -1) {
        ++off;
      }
      off += oldLocals.size();
      return off;
    }