checker-framework icon indicating copy to clipboard operation
checker-framework copied to clipboard

Value Checker has issues with non-public fields initialized with a function

Open tmarback opened this issue 2 years ago • 7 comments

The Value Checker seems to have issues accessing constant fields that are initialized with a function but are not declared as public. If I try to compile this file:

import org.checkerframework.common.value.qual.StaticallyExecutable;
import org.checkerframework.dataflow.qual.Pure;

public class Foo {

    public static final int PUBLIC_CONSTANT = 1;
    public static final int PUBLIC_METHOD = bar( 2 );
    static final int DEFAULT_CONSTANT = 3;
    static final int DEFAULT_METHOD = bar( 4 );
    protected static final int PROTECTED_CONSTANT = 5;
    protected static final int PROTECTED_METHOD = bar( 6 );
    private static final int PRIVATE_CONSTANT = 7;
    private static final int PRIVATE_METHOD = bar( 8 );

    @Pure
    @StaticallyExecutable
    public static final int bar( final int v ) {

        return v + 1;

    }

    public static final int baz() {
        return PUBLIC_CONSTANT + PUBLIC_METHOD 
                + DEFAULT_CONSTANT + DEFAULT_METHOD
                + PROTECTED_CONSTANT + PROTECTED_METHOD
                + PRIVATE_CONSTANT + PRIVATE_METHOD;
    }

}

Using these commands:

> .\bin\javac.bat -cp . Foo.java -d out
> .\bin\javac.bat -cp . -processor value -processorpath .\out Foo.java -AreportEvalWarns -d out

I get these warnings:

Foo.java:26: warning: [field.access.failed] Failed to access field DEFAULT_METHOD in class Foo: class java.lang.NoSuchFieldException: DEFAULT_METHOD
                + DEFAULT_CONSTANT + DEFAULT_METHOD
                                     ^
Foo.java:27: warning: [field.access.failed] Failed to access field PROTECTED_METHOD in class Foo: class java.lang.NoSuchFieldException: PROTECTED_METHOD
                + PROTECTED_CONSTANT + PROTECTED_METHOD
                                       ^
Foo.java:28: warning: [field.access.failed] Failed to access field PRIVATE_METHOD in class Foo: class java.lang.NoSuchFieldException: PRIVATE_METHOD
                + PRIVATE_CONSTANT + PRIVATE_METHOD;
                                     ^
3 warnings

Seems that, if a constant value is determined with a function (even if @StaticallyExecutable), the checker cannot access it if it is not public, but it tries to anyway, causing a warning. Note that the problem doesn't seem to be with static execution, as if I take out @StaticallyExecutable I get the same warning.

The current directory for these commands is the root directory of the Checker 3.28.0 release artifact.

tmarback avatar Dec 09 '22 03:12 tmarback