Checker initialization warnings

[Jon Schewe]

I'm working on annotating one of my projects to remove all checker Nullness warnings. This also means that I am handling the initialization warnings as well as these 2 checkers work hand in hand. I've managed to work through a couple of packages of the project and now am working on a package that has GUI classes as well as lots of objects referencing each other at construction time. I'm finding quite a few warnings about calling methods while the class is under initialization. Particularly about constructing the GUI itself. 

1) For the JDK GUI methods is the answer to annotate the JDK to allow most methods to be called while under initialization or is there another pattern to use?

See https://github.com/jpschewe/fll-sw/blob/checker/fll.xml/src/main/java/fll/xml/ui/ChallengeDescriptionFrame.java#L168 for an example of calling setSize. I see similar issues with getContentPane and setLayout.

2) I'm finding that I need a lot of NotOnlyInitialized annotations with objects referencing each other during construction. Is this expected?

For example see the instance variables in https://github.com/jpschewe/fll-sw/blob/checker/fll.xml/src/main/java/fll/xml/AbstractConditionStatement.java

3) In https://github.com/jpschewe/fll-sw/blob/checker/fll.xml/src/main/java/fll/xml/ScoreCategory.java#L50 I would expect "group" to be initialized once the GoalGroup constructor has completed. However checker is telling me that the argument to "goalElements.add" is @UnderInitialization(fll.xml.ComputedGoal.class) @NonNull GoalElement. Is that because "this" was passed to the "GoalGroup" constructor?

Is there a good pattern for handling this kind of reference chain?

4) Lambdas don't appear to be handled well either. When methods are called from inside a lambda that isn't being executed yet, but the lambda is constructed inside the constructor causes the method calls inside the lambda to be tagged with this being under initialization, however the lambda isn't executed until after the constructor is completed. Moving the lambda to an explicit inner class fixed these warnings.

See https://github.com/jpschewe/fll-sw/commit/92679390315a46b341708b87ac7449ae3fd353a7 for the changes.

5) Looking at https://github.com/jpschewe/fll-sw/blob/checker/fll.xml/src/main/java/fll/xml/ui/ChallengeDescriptionEditor.java#L299 all instance variables of ChallengeDescriptionEditor have been assigned, yet the methods being called generate warnings that the ChallengeDescriptionEditor is still not initialized. What am I missing here?

/home/jpschewe/projects/fll-sw/working-dir/src/main/java/fll/xml/ui/ChallengeDescriptionEditor.java:299: warning: [methodref.receiver.bound.invalid] Incompatible receiver type

    mDescription.getSubjectiveCategories().forEach(this::addSubjectiveCategory);

                                                   ^

  found   : @UnderInitialization(javax.swing.JPanel.class) @NonNull ChallengeDescriptionEditor

  required: @Initialized @NonNull ChallengeDescriptionEditor

  Consequence: method

    @UnderInitialization(javax.swing.JPanel.class) @NonNull ChallengeDescriptionEditor

  is not a valid method reference for

    @NonNull void addSubjectiveCategory(@Initialized @NonNull ChallengeDescriptionEditor this, @Initialized @NonNull SubjectiveScoreCategory p0) in @UnderInitialization(javax.swing.JPanel.class) @NonNull ChallengeDescriptionEditor

/home/jpschewe/projects/fll-sw/working-dir/src/main/java/fll/xml/ui/ChallengeDescriptionEditor.java:300: warning: [methodref.receiver.bound.invalid] Incompatible receiver type

    mDescription.getNonNumericCategories().forEach(this::addNonNumericCategory);

                                                   ^

  found   : @UnderInitialization(javax.swing.JPanel.class) @NonNull ChallengeDescriptionEditor

  required: @Initialized @NonNull ChallengeDescriptionEditor

  Consequence: method

    @UnderInitialization(javax.swing.JPanel.class) @NonNull ChallengeDescriptionEditor

  is not a valid method reference for

    @NonNull void addNonNumericCategory(@Initialized @NonNull ChallengeDescriptionEditor this, @Initialized @NonNull NonNumericCategory p0) in @UnderInitialization(javax.swing.JPanel.class) @NonNull ChallengeDescriptionEditor

Thank you for any insights,

Jon

[Jon Schewe]

A couple of updates.

2) Better code reference is https://github.com/jpschewe/fll-sw/blob/checker/fll.xml/src/main/java/fll/xml/ui/ChallengeDescriptionEditor.java#L80

5) I'm expecting that I should see UnderInitialization(ChallengeDescriptionEditor.class) not UnderInitialization(JPanel.class).

--

---
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/bd30e25eaf766aa01fd8b813996a2dbdf3ad3e6e.camel%40mtu.net.