Skip to content

Conversation

@wmdietl
Copy link
Member

@wmdietl wmdietl commented May 4, 2024

@txiang61 @Ao-senXiong I've split off the recent pushes to master into this PR.
Please modify #45 to fix this example before we merge it.

@aosen-xiong
Copy link

Thanks!

@aosen-xiong
Copy link

aosen-xiong commented May 8, 2024

@wmdietl @txiang61 Let's use this PR for discussion then.

I have run this example use current PICO checker in #43 with the following errors issued.

JavaExamples.java:10: error: [assignment.type.incompatible] incompatible types in assignment.
        @Mutable Set<String> new_s1 = s; // ERROR, type incompatible
                                      ^
  found   : @Immutable Set<@Immutable String>
  required: @Mutable Set<@Immutable String>
JavaExamples.java:11: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        new_s.add("x"); // ERROR
                 ^
  found   : @Immutable Set</*RAW*/>
  required: @Mutable Set</*RAW*/>
JavaExamples.java:18: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        new_s.add("x"); // ERROR
                 ^
  found   : @Immutable Set</*RAW*/>
  required: @Mutable Set</*RAW*/>
JavaExamples.java:30: error: [assignment.type.incompatible] incompatible types in assignment.
        @Mutable List<String> v2 = s.get(l); // ERROR
                                        ^
  found   : @Immutable List<@Immutable String>
  required: @Mutable List<@Immutable String>
JavaExamples.java:31: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        v.add("x"); // ERROR
             ^
  found   : @Immutable List</*RAW*/>
  required: @Mutable List</*RAW*/>
JavaExamples.java:36: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        p.family.add("Jenny"); // ERROR, can not mutate immut list
                    ^
  found   : @Immutable List</*RAW*/>
  required: @Mutable List</*RAW*/>
JavaExamples.java:54: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        this.family.add("Mom"); // ERROR
                       ^
  found   : @Immutable List</*RAW*/>
  required: @Mutable List</*RAW*/>
JavaExamples.java:62: error: [return.type.incompatible] incompatible types in return.
        return family; // ERROR, type incompatible
               ^
  type of expression: @Immutable List<@Immutable String>
  method return type: @Mutable List<@Immutable String>
JavaExamples.java:87: error: [type.argument.type.incompatible] incompatible type argument for type parameter T of MutList.
    void foo1 (ImmutSet<MutList<T>> s) {  // ERROR
                                ^
  found   : T extends @Readonly Object
  required: [extends @Readonly Object super @Mutable NullType]
9 errors

@aosen-xiong
Copy link

After this PR on CF eisop/checker-framework#793,

the error message are expected:

JavaExamples.java:10: error: [assignment.type.incompatible] incompatible types in assignment.
        @Mutable Set<String> new_s1 = s; // ERROR, type incompatible
                                      ^
  found   : @Immutable Set<@Immutable String>
  required: @Mutable Set<@Immutable String>
JavaExamples.java:11: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        new_s.add("x"); // ERROR
                 ^
  found   : @Immutable Set<@Immutable String>
  required: @Mutable Set<@Immutable String>
JavaExamples.java:18: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        new_s.add("x"); // ERROR
                 ^
  found   : @Immutable Set<@Immutable String>
  required: @Mutable Set<@Immutable String>
JavaExamples.java:30: error: [assignment.type.incompatible] incompatible types in assignment.
        @Mutable List<String> v2 = s.get(l); // ERROR
                                        ^
  found   : @Immutable List<@Immutable String>
  required: @Mutable List<@Immutable String>
JavaExamples.java:31: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        v.add("x"); // ERROR
             ^
  found   : @Immutable List<@Immutable String>
  required: @Mutable List<@Immutable String>
JavaExamples.java:36: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        p.family.add("Jenny"); // ERROR, can not mutate immut list
                    ^
  found   : @Immutable List<@Immutable String>
  required: @Mutable List<@Immutable String>
JavaExamples.java:54: error: [method.invocation.invalid] call to add(E) not allowed on the given receiver.
        this.family.add("Mom"); // ERROR
                       ^
  found   : @Immutable List<@Immutable String>
  required: @Mutable List<@Immutable String>
JavaExamples.java:62: error: [return.type.incompatible] incompatible types in return.
        return family; // ERROR, type incompatible
               ^
  type of expression: @Immutable List<@Immutable String>
  method return type: @Mutable List<@Immutable String>
JavaExamples.java:87: error: [type.argument.type.incompatible] incompatible type argument for type parameter T of MutList.
    void foo1 (ImmutSet<MutList<T>> s) {  // ERROR
                                ^
  found   : T extends @Readonly Object
  required: [extends @Readonly Object super @Mutable NullType]

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants