Initialize implicit this.

[smillst]

No description provided.

[mernst]

Thanks!

[mernst]

@smillst Tests are failing.

[jyoo980]

The following test case is failing:

@EnsuresNonEmptyIf(result = false, expression = "this")
public boolean isEmpty2() {
  return size() == 0 ? true : false;
}

With the error:

error: [contracts.conditional.postcondition] conditional postcondition is not satisfied when isEmpty2 returns false.
    return size() == 0 ? true : false;
    ^
  found   : this is @UnknownNonEmpty
  required: this is @NonEmpty

And I'm wondering now if it's still a valid test case. Is there enough information to determine whether the container is indeed non-empty in the case that this method returns false?

For context, the implementation of size() used in this method is:

@Pure
@Override
public int size() {
  return -1;
}

Which overrides the size() method provided by the JDK.

[smillst]

And I'm wondering now if it's still a valid test case. Is there enough information to determine whether the container is indeed non-empty in the case that this method returns false?

I think it is. The non-empty checker is assuming that size is implemented correctly. Also the other two similar test cases in that file still pass.

  @EnsuresNonEmptyIf(result = false, expression = "this")
  public boolean isEmpty3() {
    return size() == 0;
  }

  @Pure
  @Override
  @EnsuresNonEmptyIf(result = false, expression = "this")
  public boolean isEmpty() {
    if (size() == 0) {
      return true;
    } else {
      return false;
    }
  }

So I think this failure indicates a bug somewhere in dataflow. Conditional expressions have a different implementation than if statements in dataflow. I'm working on this now.

[jyoo980]

@smillst I see, thanks!