How do I annotate an implicit parameter in a stub

Question

I'm trying to use the Nullness Checker to build a subclass of JPanel.

class MyView<R extends @NonNull Object> extends JPanel {
  // ...
  // constructor calls this method:
  @RequiresNonNull({"labelPanel", "fieldPanel", "checkBoxPanel"})
  private void makeTopPanel(@UnderInitialization MyView<R> this) {
    JPanel topPanel = new JPanel(new BorderLayout());
    topPanel.add(labelPanel, BorderLayout.LINE_START);
    topPanel.add(fieldPanel, BorderLayout.CENTER);
    topPanel.add(checkBoxPanel, BorderLayout.LINE_END);

    // Error here: [method.invocation.invalid] call to add(java.awt.Component,java.lang.Object)
    // not allowed on the given receiver.
    add(topPanel, BorderLayout.PAGE_START);
    setBorder(new MatteBorder(1, 0, 0, 0, Color.black));
  }
}

The error message says this:

error: [method.invocation.invalid] call to add(java.awt.Component,java.lang.Object) not allowed 
on the given receiver.
  found   : @UnderInitialization @NonNull Container
  required: @Initialized @NonNull Container

The problem seems to be that the add method assumes the this is initialized. But it's very safe to call a Container's add method inside a constructor. So to prevent this error, I want to create a stub file with an annotated implicit parameter:

package java.awt;
public class Container extends Component {
  public void add(@UnknownInitialization Container, @NonNull Component, @NonNull Object);
}

It doesn't seem to recognize the add() method here as the java.awt.Container.add(Component, Object) method.

Here's the complete stub file:

import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.checker.initialization.qual.UnknownInitialization;
import javax.swing.border.Border;
import java.awt.Component;
import java.awt.Container;

package javax.swing;

public class Timer {
  public Timer(int delay, @Nullable ActionListener listener);
}

public class JOptionPane {
  public static void showMessageDialog(@Nullable Component parentComponent,
          Object message, String title, int messageType)
          throws HeadlessException;
}

package java.awt;
public class Container extends Component {
  public void setBorder(@UnknownInitialization JComponent this, @Nullable Border border);
  public void add(@UnknownInitialization Container this, @NonNull Component, @NonNull Object);
}

I know I can suppress the warning with an annotation, but the stub file feels like a cleaner approach. Is there any way to fix this stub file?

Answer 1

There are two problems.

The first problem is that your stub file is malformed.

The line

  public void add(@UnknownInitialization Container this, @NonNull Component, @NonNull Object);

should be

  public void add(@UnknownInitialization Container this, @NonNull Component comp, @NonNull Object constraints);

because Java method declarations require formal parameter names.

Furthermore, it was missing an import statement:

import org.checkerframework.checker.nullness.qual.NonNull;

The second problem is that you must not have been passing an -Astubs=... command-line argument, or you would have received warnings about your malformed stub file. (You didn't say how you invoked javac, which would have helped to diagnose your problem.)

When I corrected these problems, the Checker Framework worked as expected. Running the command

$CHECKERFRAMEWORK/checker/bin/javac -processor nullness -g MyView.java

issues the warning, and

$CHECKERFRAMEWORK/checker/bin/javac -processor nullness -g MyView.java -Astubs=mystub.astub

issues no warning.

Corrected files (that is, they are complete and more minimal) appear below.

MyView.java:

import java.awt.BorderLayout;
import javax.swing.JPanel;
import org.checkerframework.checker.initialization.qual.UnderInitialization;

class MyView extends JPanel {

  MyView() {
    makeTopPanel();
  }

  private void makeTopPanel(@UnderInitialization MyView this) {
    JPanel topPanel = new JPanel(new BorderLayout());
    add(topPanel, BorderLayout.PAGE_START);
  }
}

mystub.astub:

import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.checker.initialization.qual.UnknownInitialization;
import javax.swing.border.Border;
import java.awt.Component;
import java.awt.Container;

package javax.swing;

public class Timer {
  public Timer(int delay, @Nullable ActionListener listener);
}

public class JOptionPane {
  public static void showMessageDialog(@Nullable Component parentComponent,
          Object message, String title, int messageType)
          throws HeadlessException;
}

package java.awt;
public class Container extends Component {
  public void setBorder(@UnknownInitialization JComponent this, @Nullable Border border);
  public void add(@UnknownInitialization Container this, @NonNull Component comp, @NonNull Object constraints);
}