eisop / checker-framework

Pluggable type-checking for Java
https://eisop.github.io/
Other
17 stars 16 forks source link

Fix initial store ignoring viewpoint adaption #681

Open flo2702 opened 7 months ago

flo2702 commented 7 months ago

This branch fixes a bug where the initial store contains a field's unadapted type in some cases.

The bug only surfaces when the field's declared type is adapted to a more general type.

For example, consider a partial hierarchy @Top <: @C where for a field of declared type @C Object c, the access this.c has type @Top if this is @Top, and type @C otherwise, as in the following listing.

public class ReceiverAdaption {

    @C Object c;

    void testTop(@Top ReceiverAdaption this) {
        // this.c has the adapted type @Top ◀ @C = @Top, so this should throw an error
        // but the initial store contains the unadapted type @C for c
        @C Object varC = this.c;
    }
}