Skip to content

@ThrowsException annotation for methods that always throw an exception #2076

@SwingGuy1024

Description

@SwingGuy1024

This is a feature request for a @ThrowsException method annotation, which indicates that the annotated method throws an exception.
This would be analogous to @TerminatesExecution, in that it would improve the dataflow analysis (flow-sensitive type refinement).

The original suggestion follows.


In my project at work, I encountered this line, which throws an exception:

BusinessException.builder()
        .detail(detailedMessage)
        .transitionFrom(ShippingState.RECEIVED)
        .withIdentifier(ProductSourceIdentifier.WAREHOUSE_ID, warehouseId)
        .buildAndThrow();

Should the Nullness Checker encounter this, it has no way of knowing that an exception is guaranteed to be thrown on this line. Granted, I would have written it like this:

throw BusinessException.builder()
        .detail(detailedMessage)
        .transitionFrom(ShippingState.RECEIVED)
        .withIdentifier(ProductSourceIdentifier.WAREHOUSE_ID, warehouseId)
        .build();

But I didn't write this code, and this is done all over the project.

Now suppose the Nullness Checker encountered something like this:

public ConnectionSource getConnection() {
  if (connectionSource == null) {
    BusinessException.builder()
        .doWhateverStuffIsNeeded()
        .buildAndThrow();
  }
  return connectionSource;
}

It would have no way of knowing that an exception gets thrown when connectionSource is null, so it would issue an error, believing that connectionSource could be null.

In principle, this could be handled by an annotation on the buildAndThrow() method that says that it throws an exception, under a condition. So let's imagine there's an annotation @throws(String expression) where it declares it will throw an exception if the expression is true. (This is similar to the JetBrains @contract annotation, which covers the same problem.) Then we could declare the method like this:

@Throws("true")
public void buildAndThrow() { ... }

Now the Nullness Checker would have the information it needs. It would know that an exception is always thrown when connectionSource is null, so would process the method correctly.

The Nullness Checker would be more useful with a facility like this. The preconditions and post conditions are useful, but they don't cover a case like this.

(Please don't suggest that @RequiresNonNull(connectionSource) would solve this problem. In this simplified version, it will, but the actual case was far more complicated, with several method parameters and various tests. In the real-world example where I found this, the only solution that makes sense would be to tell the checker that the buildAndThrow method will throw an exception.)

Metadata

Metadata

Assignees

No one assigned

    Labels

    Dataflowenhancementgood first issueA beginner-friendly place to start contributing to the Checker Framework

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions