EnsuresNonNull false positive

[npepinpe]

First off, I'm just starting out with the Checker Framework, so it's possible I'm simply doing something wrong, but it seems to me like the documentation implies I can use EnsuresNonNull for the following:

I have a class as so:

final class BoundedTransactionalRecordBatch {
  @NonNull private final KafkaProducerFactory producerFactory;
  @NonNull private final ProducerConfig config;
  @NonNull private final String producerId;
  @NonNull private final Logger logger;

  @Nullable private Producer<RecordId, byte[]> producer;
  private boolean producerInitialized = false;

  @EnsuresNonNull("producer")
  private void ensureProducer() {
    if (producer != null) {
      return;
    }

    producer = producerFactory.newProducer(config, producerId);
    logger.trace("Created new producer");
  }

  @EnsuresNonNull("producer")
  private void ensureProducerInitialized() {
    ensureProducer();

    if (!producerInitialized) {
      producer.initTransactions();
      producerInitialized = true;
      logger.trace("Initialized producer for transactions");
    }
  }
}

Note that producerFactory.newProducer() returns a @NonNull annotated type. When running the framework, I still get the following error:

[ERROR] /home/nicolas/src/github.com/camunda-community-hub/zeebe-kafka-exporter/exporter/src/main/java/io/zeebe/exporters/kafka/producer/BoundedTransactionalRecordBatch.java:[220,15] error: [contracts.postcondition] postcondition of ensureProducer is not satisfied.
[ERROR]   found   : no information about this.producer
[ERROR]   required: this.producer is @NonNull

I use the Maven integration as specified in the docs, and simply run mvn compile. I didn't change the profiles or any of the settings from the docs. I'm also on Java 11.

I expect here that the method correctly ensures that producer is never null, and that other methods can transitively declare the same by calling this method.

Note that the producer property is annotated as @Nullable on purpose, as the producer may be null'd at times.

[mernst]

I'm sorry you are having trouble.

The Nullness Checker does infer that producer is null after the assignment to producer in ensureProducer(). However, after that, ensureProducer calls both initTransactions and logger.trace(). Those methods might have arbitrary effects -- in particular, one might call back into class BoundedTransactionalRecordBatch and might set producer to null. (It probably does not in this case, but it could. For example, if a logger was passed an object to print, it might call that object's toString, which could have side effects.)

Here are three things you could do for the logger.trace() call:

• suppress the warning, with a note that you trust logger.trace to have no side effects.
• write a stub file that applies the @SideEffectFree annotation to Logger.trace().
• place the call to logger.trace() within ProducerConfig.initTransactions(). You will still have to deal with initTransactions().

(A side note: it's easier to experiment with your code if you provide a compilable example. Your example is missing import statements and uses many classes that are not part of the JDK. Also, the error message refers to line 220, which does not exist in the code snippet you provided.)

[mernst]

@npepinpe Does the answer resolve your problem?

[mernst]

I'm closing this because of no answer from the original poster after (I believe) resolving the issue.