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

[Viewpoint test checker] RDQ method parameter is not adapted. #1037

Open
Ao-senXiong opened this issue Dec 31, 2024 · 0 comments
Open

[Viewpoint test checker] RDQ method parameter is not adapted. #1037

Ao-senXiong opened this issue Dec 31, 2024 · 0 comments

Comments

@Ao-senXiong
Copy link
Member

Method parameter should be adapted based on receiver type, which current does not. this.f=rdqObject and this.f = rdqObject; should be okay at declaration site. For call site, it seems working correctly.

This should be fixed otherwise @A and @B can not invoke rdqMethod.

This test case also contains a bunch of errors should be fixed by #1032.

public class RDQTest {
    @ReceiverDependentQual class RDQClass {
        @ReceiverDependentQual Object f;
        void aMethod(@A RDQClass this, @ReceiverDependentQual Object rdqObject, @A Object aObject) {
            this.f = rdqObject;
            this.f = aObject;
        }
        void bMethod(@B RDQClass this, @ReceiverDependentQual Object rdqObject, @B Object bObject) {
            this.f = rdqObject;
            this.f = bObject;
        }

        void rdqMethod(@ReceiverDependentQual RDQClass this, @ReceiverDependentQual Object rdqObject) {
            this.f = rdqObject;
        }
    }

    void test(@A Object aObject, @B Object bObject, @ReceiverDependentQual Object rdqObject) {
        RDQClass aInstance = new @A RDQClass();
        RDQClass bInstance = new @B RDQClass();
        RDQClass rdqInstance = new @ReceiverDependentQual RDQClass();
        aInstance.aMethod(aObject, aObject);
        aInstance.bMethod(bObject, bObject);
        aInstance.rdqMethod(rdqObject);
        bInstance.aMethod(aObject, aObject);
        bInstance.bMethod(bObject, bObject);
        bInstance.rdqMethod(rdqObject);
        rdqInstance.aMethod(aObject, aObject);
        rdqInstance.bMethod(bObject, bObject);
        rdqInstance.rdqMethod(rdqObject);
    }
}

Error message:

framework/tests/viewpointtest/RDQTest.java:7: warning: [inconsistent.constructor.type] Constructor type (@ReceiverDependentQual) is a subtype of the top type (@Top), therefore it cannot be statically verified.
    @ReceiverDependentQual class RDQClass {
                           ^
framework/tests/viewpointtest/RDQTest.java:7: error: [super.invocation.invalid] Constructor of type @ReceiverDependentQual cannot call super() of type @Top.
    @ReceiverDependentQual class RDQClass {
                           ^
framework/tests/viewpointtest/RDQTest.java:9: error: [type.invalid.annotations.on.use] invalid type: annotations [@A] conflict with declaration of type RDQTest.RDQClass
        void aMethod(@A RDQClass this, @ReceiverDependentQual Object rdqObject, @A Object aObject) {
                                 ^
framework/tests/viewpointtest/RDQTest.java:10: error: [assignment.type.incompatible] incompatible types in assignment.
            this.f = rdqObject;
                     ^
  found   : @ReceiverDependentQual Object
  required: @A Object
framework/tests/viewpointtest/RDQTest.java:13: error: [type.invalid.annotations.on.use] invalid type: annotations [@B] conflict with declaration of type RDQTest.RDQClass
        void bMethod(@B RDQClass this, @ReceiverDependentQual Object rdqObject, @B Object bObject) {
                                 ^
framework/tests/viewpointtest/RDQTest.java:14: error: [assignment.type.incompatible] incompatible types in assignment.
            this.f = rdqObject;
                     ^
  found   : @ReceiverDependentQual Object
  required: @B Object
framework/tests/viewpointtest/RDQTest.java:28: error: [argument.type.incompatible] incompatible argument for parameter rdqObject of RDQClass.bMethod.
        aInstance.bMethod(bObject, bObject);
                          ^
  found   : @B Object
  required: @A Object
framework/tests/viewpointtest/RDQTest.java:28: error: [method.invocation.invalid] call to bMethod(java.lang.@viewpointtest.quals.ReceiverDependentQual Object,java.lang.@viewpointtest.quals.B Object) not allowed on the given receiver.
        aInstance.bMethod(bObject, bObject);
                         ^
  found   : @Top RDQTest.@A RDQClass
  required: @Top RDQTest.@B RDQClass
framework/tests/viewpointtest/RDQTest.java:29: error: [argument.type.incompatible] incompatible argument for parameter rdqObject of RDQClass.rdqMethod.
        aInstance.rdqMethod(rdqObject);
                            ^
  found   : @ReceiverDependentQual Object
  required: @A Object
framework/tests/viewpointtest/RDQTest.java:30: error: [argument.type.incompatible] incompatible argument for parameter rdqObject of RDQClass.aMethod.
        bInstance.aMethod(aObject, aObject);
                          ^
  found   : @A Object
  required: @B Object
framework/tests/viewpointtest/RDQTest.java:30: error: [method.invocation.invalid] call to aMethod(java.lang.@viewpointtest.quals.ReceiverDependentQual Object,java.lang.@viewpointtest.quals.A Object) not allowed on the given receiver.
        bInstance.aMethod(aObject, aObject);
                         ^
  found   : @Top RDQTest.@B RDQClass
  required: @Top RDQTest.@A RDQClass
framework/tests/viewpointtest/RDQTest.java:32: error: [argument.type.incompatible] incompatible argument for parameter rdqObject of RDQClass.rdqMethod.
        bInstance.rdqMethod(rdqObject);
                            ^
  found   : @ReceiverDependentQual Object
  required: @B Object
framework/tests/viewpointtest/RDQTest.java:33: error: [argument.type.incompatible] incompatible argument for parameter rdqObject of RDQClass.aMethod.
        rdqInstance.aMethod(aObject, aObject);
                            ^
  found   : @A Object
  required: @ReceiverDependentQual Object
framework/tests/viewpointtest/RDQTest.java:33: error: [method.invocation.invalid] call to aMethod(java.lang.@viewpointtest.quals.ReceiverDependentQual Object,java.lang.@viewpointtest.quals.A Object) not allowed on the given receiver.
        rdqInstance.aMethod(aObject, aObject);
                           ^
  found   : @Top RDQTest.@ReceiverDependentQual RDQClass
  required: @Top RDQTest.@A RDQClass
framework/tests/viewpointtest/RDQTest.java:34: error: [argument.type.incompatible] incompatible argument for parameter rdqObject of RDQClass.bMethod.
        rdqInstance.bMethod(bObject, bObject);
                            ^
  found   : @B Object
  required: @ReceiverDependentQual Object
framework/tests/viewpointtest/RDQTest.java:34: error: [method.invocation.invalid] call to bMethod(java.lang.@viewpointtest.quals.ReceiverDependentQual Object,java.lang.@viewpointtest.quals.B Object) not allowed on the given receiver.
        rdqInstance.bMethod(bObject, bObject);
                           ^
  found   : @Top RDQTest.@ReceiverDependentQual RDQClass
  required: @Top RDQTest.@B RDQClass
15 errors
1 warning
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

No branches or pull requests

1 participant