Skip to content

Commit

Permalink
Correct the test cases
Browse files Browse the repository at this point in the history
  • Loading branch information
Ao-senXiong committed Jan 7, 2025
1 parent 6a7fb65 commit 44a70e6
Show file tree
Hide file tree
Showing 3 changed files with 1 addition and 38 deletions.
2 changes: 0 additions & 2 deletions checker/tests/pico-immutability/ClassAnnotation.java
Original file line number Diff line number Diff line change
Expand Up @@ -55,11 +55,9 @@ void method1(/* @Immutable */ ImmutableClassImplict this) {}

void method2(@Immutable ImmutableClassImplict this) {}

// TODO(Aosen) maybe we should even issue error here since we know the bound can only be
// @Immutable
void method3(@Readonly ImmutableClassImplict this) {}

// TODO(Aosen) should we issue error here, it can only be called by @Immutable and @Bottom
void method4(@PolyMutable ImmutableClassImplict this) {}

// :: error: (type.invalid.annotations.on.use)
Expand Down
7 changes: 1 addition & 6 deletions checker/tests/pico-immutability/ImmutableClass.java
Original file line number Diff line number Diff line change
Expand Up @@ -10,14 +10,9 @@ public class ImmutableClass {
@ReceiverDependentMutable Object rdmField;
@Immutable Object immutableField;

@Immutable ImmutableClass(@ReceiverDependentMutable Object rdmObject, @Immutable Object immutableObject) {
this.readonlyField = rdmObject;
@Immutable ImmutableClass(@Immutable Object immutableObject) {
this.readonlyField = immutableObject;
// :: error: (assignment.type.incompatible)
this.rdmField = rdmObject; // TODO: parameter should be adapted as well.
this.rdmField = immutableObject;
// :: error: (assignment.type.incompatible)
this.immutableField = rdmObject;
this.immutableField = immutableObject;
}

Expand Down
30 changes: 0 additions & 30 deletions checker/tests/pico-immutability/ViewpointAdaptationRules.java
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,6 @@
import org.checkerframework.checker.pico.qual.Readonly;
import org.checkerframework.checker.pico.qual.ReceiverDependentMutable;

// TODO The test case is almost right but reflect the method parameter is not adapted at the moment,
// which should be adapted. Otherwise, one can not invoke the constructor correctly to create both
// immutable and mutable instance.
@ReceiverDependentMutable public class ViewpointAdaptationRules {

@Assignable @Readonly Object assignableReadonlyField;
Expand All @@ -28,7 +25,6 @@
void mutatableReceiver(
@Mutable ViewpointAdaptationRules this,
@Mutable Object mutableObject,
@ReceiverDependentMutable Object rdmObject,
@Immutable Object immutableObject,
@Readonly Object readonlyObject) {
this.assignableReadonlyField = mutableObject;
Expand All @@ -37,14 +33,6 @@ void mutatableReceiver(
this.immutableField = mutableObject;
this.assingableMuatbleField = mutableObject;

this.assignableReadonlyField = rdmObject;
// :: error: (assignment.type.incompatible)
this.rdmField = rdmObject; // The field is adapted to Mutable but method parameters are not?
// :: error: (assignment.type.incompatible)
this.immutableField = rdmObject;
// :: error: (assignment.type.incompatible)
this.assingableMuatbleField = rdmObject; // The method parameter is not adapted?

this.assignableReadonlyField = immutableObject;
// :: error: (assignment.type.incompatible)
this.rdmField = immutableObject; // The field is adapted to mutable
Expand Down Expand Up @@ -103,7 +91,6 @@ void receiverDependentMutableReceiver(
void ImmutableReceiver(
@Immutable ViewpointAdaptationRules this,
@Mutable Object mutableObject,
@ReceiverDependentMutable Object rdmObject,
@Immutable Object immutableObject,
@Readonly Object readonlyObject) {
this.assignableReadonlyField = mutableObject;
Expand All @@ -113,14 +100,6 @@ void ImmutableReceiver(
this.immutableField = mutableObject;
this.assingableMuatbleField = mutableObject;

this.assignableReadonlyField = rdmObject;
// :: error: (assignment.type.incompatible) :: error: (illegal.field.write)
this.rdmField = rdmObject; // Field is adpated to immutable but method parameters are not?
// :: error: (assignment.type.incompatible) :: error: (illegal.field.write)
this.immutableField = rdmObject; // Method parameter are not adapate?
// :: error: (assignment.type.incompatible)
this.assingableMuatbleField = rdmObject;

this.assignableReadonlyField = immutableObject;
// :: error: (illegal.field.write)
this.rdmField = immutableObject;
Expand All @@ -141,7 +120,6 @@ void ImmutableReceiver(
void ReadonlyReceiver(
@Readonly ViewpointAdaptationRules this,
@Mutable Object mutableObject,
@ReceiverDependentMutable Object rdmObject,
@Immutable Object immutableObject,
@Readonly Object readonlyObject) {
this.assignableReadonlyField = mutableObject;
Expand All @@ -151,14 +129,6 @@ void ReadonlyReceiver(
this.immutableField = mutableObject;
this.assingableMuatbleField = mutableObject;

this.assignableReadonlyField = rdmObject;
// :: error: (assignment.type.incompatible) :: error: (illegal.field.write)
this.rdmField = rdmObject;
// :: error: (assignment.type.incompatible) :: error: (illegal.field.write)
this.immutableField = rdmObject;
// :: error: (assignment.type.incompatible)
this.assingableMuatbleField = rdmObject;

this.assignableReadonlyField = immutableObject;
// :: error: (assignment.type.incompatible) :: error: (illegal.field.write)
this.rdmField = immutableObject;
Expand Down

0 comments on commit 44a70e6

Please sign in to comment.