RequiresNonNull checked?

[Steffen Heil]

Hi

I do not understand, why the following does not create a Warning?

public class Test {

  

  @Nullable

  Object o;

  

  

  @RequiresNonNull("#1.o")

  private static void test(Test p) {

    System.out.println(p.o.toString());

  }

  

  

  public static void main(String[] args) {

    test(new Test());

  }

  

}

Any hints?

Best regards,

   Steffen

[Michael Ernst]

It's odd that the Nullness Checker does not produce a warning for that code when you run it.  It does for me.

I used the following code (identical to yours except for added imports and putting "@Nullable Object" on one line):

import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;

public class Test {

  @Nullable Object o;

  @RequiresNonNull("#1.o")
  private static void test(Test p) {
    System.out.println(p.o.toString());
  }

  public static void main(String[] args) {
    test(new Test());
  }
}

I ran the command:

javacheck -processor nullness Test.java

where javacheck as is described in the Checker Framework manual.

The result was:

Test.java:14: error: [contracts.precondition] precondition of test is not satisfied.
    test(new Test());
        ^
  found   : no information about new Test().o
  required: new Test().o is @NonNull
1 error

Mike

--

---
You received this message because you are subscribed to the Google Groups "Checker Framework discussion" group.
To unsubscribe from this group and stop receiving emails from it, send an email to checker-framework-...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/checker-framework-discuss/4c2e5dda-894b-4325-a76c-35d79d7a9698n%40googlegroups.com.

[Steffen Heil]

Thanks for testing this. We finally figured out the problem.

We were running the checker through Maven. And our POM file contained the following part:

   <arg>-AonlyUses=our\.project\.package\.</arg>

Therefor all uses were ignored...

Sorry for the noise.

Steffen

[Michael Ernst]

Steffen-

No problem.  I'm glad it is working for you now.

Please let us know if you have any other problems or questions.

In the future, if you think there is a bug in the Checker Framework, it is probably best to open an issue in the issue tracker, per https://checkerframework.org/manual/#reporting-bugs .

Mike

To view this discussion on the web visit https://groups.google.com/d/msgid/checker-framework-discuss/c9a1624a-0850-4aa9-9ee1-3cb8d09d3114n%40googlegroups.com.