Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add some examples #48

Open
wants to merge 5 commits into
base: master
Choose a base branch
from
Open

Add some examples #48

wants to merge 5 commits into from

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.

@Ao-senXiong
Copy link

Thanks!

@Ao-senXiong
Copy link

Ao-senXiong 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

@Ao-senXiong
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.

3 participants