Checker Framework 3.16.0

Version 3.16.0 (July 13, 2021)

User-visible changes:

You can run the Checker Framework on a JDK 16 JVM. You can pass the --release 16 command-line argument to the compiler. You may need to add additional command-line options, such as --add-opens; see the Checker Framework manual. New syntax, such as records and switch expressions, is not yet supported or type-checked; that will be added in a future release. Thanks to Neil Brown for the JDK 16 support.

The Lock Checker supports a new type, @NewObject, for the result of a constructor invocation.

The -Ainfer command-line argument now outputs purity annotations even if neither -AsuggestPureMethods nor AcheckPurityAnnotations is supplied on the command line.

Implementation details:

Method renamings (the old methods remain but are deprecated):

• AnnotationFileElementTypes.getDeclAnnotation => getDeclAnnotations

Method renamings (the old methods were removed):

• AnnotatedTypeMirror.clearAnnotations => clearPrimaryAnnotations`

Method renamings in DefaultTypeHierarchy (the old methods were removed):

• visitIntersectionSupertype => visitIntersectionSupertype
• visitIntersectionSubtype => visitIntersection_Type
• visitUnionSubtype => visitUnion_Type
• visitTypevarSubtype => visitTypevar_Type
• visitTypevarSupertype => visitType_Typevar
• visitWildcardSubtype => visitWildcard_Type
• visitWildcardSupertype => visitType_Wildcard

Method renamings in AnnotatedTypes (the old methods were removed):

• expandVarArgs => expandVarArgsParameters
• expandVarArgsFromTypes => expandVarArgsParametersFromTypes

Closed issues:
#3013, #3754, #3791, #3845, #4523, #4767.

Checker Framework 3.15.0

Version 3.15.0 (June 18, 2021)

User-visible changes:

The Resource Leak Checker ensures that certain methods are called on an object before it is de-allocated. By default, it enforces that close() is called on any expression whose compile-time type implements java.io.Closeable.

Implementation details:

Method renamings (the old methods remain but are deprecated):

• AnnotatedDeclaredType#wasRaw => isUnderlyingTypeRaw
• AnnotatedDeclaredType#setWasRaw => setIsUnderlyingTypeRaw

Closed issues:
#4549, #4646, #4684, and #4699.

Checker Framework 3.14.0

Version 3.14.0 (June 1, 2021)

User-visible changes:

The Units Checker supports new qualifiers (thanks to Rene Kraneis):

• @Volume, @m3, @mm3, @km3
• @Force, @N, @kN
• @t (metric ton, a unit of mass)

Stub files can now override declaration annotations in the annotated JDK. Previously, stub files only overrode type annotations in the annotated JDK.

Command-line argument -AstubWarnIfNotFound is treated as true for stub files provided on the command line.

Implementation details:

Method SourceChecker.getProperties takes a third formal parameter permitNonExisting.

Method TreeUtils.getMethodName() returns a String rather than a Name.

Removed CheckerDevelMain.

Closed issues:
#3993, #4116, #4586, #4598, #4612, #4614.

Checker Framework 3.13.0

Version 3.13.0 (May 3, 2021)

Survey:

If you use the Checker Framework, please answer a 3-question survey about what version of Java you use. It will take less than 1 minute to complete. Please answer it at
https://docs.google.com/forms/d/1Bbt34c_3nDItHsBnmEfumoyrR-Zxhvo3VTHucXwfMcQ .
Thanks!

User-visible changes:

Command-line argument -AassumeKeyFor makes the Nullness Checker and Map Key Checker unsoundly assume that the argument to Map.get is a key for the receiver map.

Warning message keys are shorter. This reduces clutter in error messages and in @SuppressWarnings annotations. Most ".type.invalid", ".type.incompatible", ".invalid", and ".not.satisfied" suffixes and "type.invalid." prefixes have been removed, and most ".invalid." substrings have been changed to ".".

The Checker Framework no longer crashes on code that contains binding variables (introduced in Java 14 for instanceof pattern matching), and such variables are reflected in the control flow graph (CFG). Thanks to Chris Day for this change. However, note that the Checker Framework only has full support for Java 8 and Java 11.

New command-line argument -AstubWarnNote makes stub file warnings notes rather than warnings.

Removed the StubGenerator section from the manual, because changes in JDK 11 have broken the StubGenerator program.

Implementation details:

Method renamings:

• DependentTypesHelper.atReturnType => atMethodBody

Closed issues:
#1268, #3039, #4410, #4550, #4558, #4563, #4566, #4567, #4571, #4584, #4591, #4594, #4600.

Checker Framework 3.12.0

Version 3.12.0, April 1, 2021

User-visible changes:

New FAQ item "How should I annotate code that uses generics?" gives examples of annotations on type variables, together with their meaning.

-Ainfer=ajava uses ajava files (rather than jaif files or stub files) internally during whole-program inference.

The Optional Checker supports a new annotation @OptionalBottom that stands for (only) the null value.

The value element/argument to @EnumVal is now required. Previously it defaulted to an empty array.

Implementation details:

A precondition or normal postcondition annotation's value element must have type String[], not String. A conditinoal postcondition annotation's expression element must have type String[], not String. These changes will not affect users (any programmer-written annotation that was legal before will still be legal), but it may affect checker implementations.

JavaExpressionParseUtil:
JavaExpressionParseUtil#parse no longer viewpoint-adapts Java expressions. It just converts the expression String to a JavaExpression. To that end, JavaExpressionParseUtil.JavaExpressionContext has been removed and JavaExpressionParseUtil#parse no longer takes a context object. Most calls to JavaExpressionParseUtil#parse should be replaced with a call to one of the methods in StringToJavaExpressions.

Renamed AnnotatedTypeComparer to DoubleAnnotatedTypeScanner. In the new class, the method compare was renamed defaultAction. The method combineRs was replaced by reduce.

Removed methods:

• AnnotationUtils.getElementValueArrayOrSingleton
• DependentTypesHelper.standardizeNewClassTree: use atExpression instead
• DependentTypesHelper.standardizeString: override one of the methods explained in the Javadoc of convertAnnotationMirror

Method renamings:

• DefaultQualifierForUseTypeAnnotator.getSupportAnnosFromDefaultQualifierForUses => getDefaultQualifierForUses
• In DependentTypesHelper:
  • check* => check*ForErrorExpressions
  • viewpointAdaptConstructor => atConstructorInvocation
  • viewpointAdaptMethod => atMethodInvocation
  • viewpointAdaptTypeVariableBounds => atParameterizedTypeUse
  • standardizeClass => atTypeDecl
  • standardizeExpression => atExpression
  • standardizeFieldAccess => atFieldAccess
  • standardizeReturnType => atReturnType
  • standardizeVariable => atVariableDeclaration

Deprecated some overloads in AnnotationUtils that take a CharSequence
(use an overload that takes an ExecutablElement):

• getElementValueArray
• getElementValueClassName
• getElementValueClassNames
• getElementValueEnumArray
• getElementValueEnum
• getElementValue
• getElementValuesWithDefaults

Deprecated methods in AnnotationUtils:

• areSameByClass: use areSameByName
• getElementValuesWithDefaults: use a getElementValue* method

Removed deprecated PluginUtil class.

Closed issues:
#1376, #3740, #3970, #4041, #4254, #4346, #4355, #4358, #4372, #4381, #4384, #4417, #4449, #4452, #4480.

Checker Framework 3.11.0

Version 3.11.0, March 1, 2021

User-visible changes:

In a stub file for a class C, you may write a declaration for a method that is inherited by C but not defined by it. Previously, such stub declarations were ignored. For more information, see the manual's documentation of "fake overrides".

Nullness Checker error message key changes:

• known.nonnull => nulltest.redundant
• initialization.static.fields.uninitialized => initialization.static.field.uninitialized, and it is now issued on the field rather than on the class
• new initialization.field.uninitialized is issued on the field instead of initialization.fields.uninitialized on the class, if there is no explicitly-written constructor.

Signature Checker supports two new type qualifiers:

• @CanonicalNameAndBinaryName
• @CanonicalNameOrPrimitiveType

Implementation details:

You can make a variable's default type depend on its name, or a method return type default depend on the method's name. To support this feature, @DefaultFor has new elements names and namesExceptions.

Changes to protected fields in OverrideChecker:

• Removed overriderMeth, overriderTyp, overriddenMeth, overriddenTyp
• Renamed methodReference => isMethodReference
• Renamed overridingType => overriderType
• Renamed overridingReturnType => overriderReturnType

Changes to JavaExpression parsing:

• The signatures of these methods changed; see Javadoc.
  • JavaExpressionParseUtil#parse
  • DependentTypesHelper#standardizeString
• These methods moved:
  • GenericAnnotatedTypeFactory#standardizeAnnotationFromContract => DependentTypesHelper
  • JavaExpressionParseUtil#fromVariableTree => JavaExpression

Changes to JavaExpressionContext:

• New method JavaExpressionContext#buildContextForMethodDeclaration(MethodTree, SourceChecker) replaces all overloads of buildContextForMethodDeclaration.

Parsing a Java expression no longer requires the formal parameters AnnotationProvider provider or boolean allowNonDeterministic. Methods in JavaExpression with simplified signatures include

• fromArrayAccess
• fromNodeFieldAccess
• fromNode
• fromTree
• getParametersOfEnclosingMethod
• getReceiver

CFAbstractStore.insertValue does nothing if passed a nondeterministic expression. Use new method CFAbstractStore.insertValuePermitNondeterministic to map a nondeterministic expression to a value.

Closed issues:
#862, #3631, #3991, #4031, #4206, #4207, #4226, #4231, #4248, #4263, #4265, #4279, #4286, #4289.

Checker Framework 3.10.0

Version 3.10.0, February 1, 2021

User-visible changes:

Moved utility classes from checker-qual.jar to the new checker-util.jar.
Also, added util to the end of all the packages of the utility classes.

In Maven Central, checker.jar no longer contains duplicates of qualifiers in checker-qual.jar, but rather uses a Maven dependency. A fat jar file with all the dependencies (like the old checker.jar) is available in Maven Central with the classifier "all".

When supplying the -Ainfer=... command-line argument, you must also supply -Awarns.

Replaced several error message keys:

• contracts.precondition.expression.parameter.name
• contracts.postcondition.expression.parameter.name
• contracts.conditional.postcondition.expression.parameter.name
• method.declaration.expression.parameter.name
  by new message keys:
• expression.parameter.name.invalid
• expression.parameter.name.shadows.field

Implementation details:

Deprecated ElementUtils.enclosingClass; use ElementUtils.enclosingTypeElement.

Removed classes (use SourceChecker instead):

• BaseTypeContext
• CFContext
• BaseContext

Removed methods:

• SourceChecker.getContext(): it returned the receiver
• SourceChecker.getChecker(): it returned the receiver
• AnnotatedTypeFactory.getContext(): use getChecker()
• methods on TreePaths from class 'TreeUtils; use the versions in TreePathUtil`.

Moved class:

• org.checkerframework.framework.util.PurityUnqualified to org.checkerframework.framework.qual.PurityUnqualified

Renamed methods:

• AnnotatedTypeMirror.directSuperTypes => directSupertypes (note capitalization) for consistency with javax.lang.model.util.Types
• AnnotatedTypeMirror.removeAnnotation(Class) => removeAnnotationByClass
• MethodCall.getParameters => getArguments
• MethodCall.containsSyntacticEqualParameter => containsSyntacticEqualArgument
• ArrayAccess.getReceiver => getArray

Closed issues:
#3325 , #3474.

Checker Framework 3.9.1

Version 3.9.1, January 13, 2021

Implementation details:

Copied methods on TreePaths from class 'TreeUtilsto new classTreePathUtil`.
(The methods in TreePath will be deleted in the next release.)

• TreeUtils.enclosingClass => TreePathUtil.enclosingClass
• TreeUtils.enclosingMethod => TreePathUtil.enclosingMethod
• TreeUtils.enclosingMethodOrLambda => TreePathUtil.enclosingMethodOrLambda
• TreeUtils.enclosingNonParen => TreePathUtil.enclosingNonParen
• TreeUtils.enclosingOfClass => TreePathUtil.enclosingOfClass
• TreeUtils.enclosingOfKind => TreePathUtil.enclosingOfKind
• TreeUtils.enclosingTopLevelBlock => TreePathUtil.enclosingTopLevelBlock
• TreeUtils.enclosingVariable => TreePathUtil.enclosingVariable
• TreeUtils.getAssignmentContext => TreePathUtil.getAssignmentContext
• TreeUtils.inConstructor => TreePathUtil.inConstructor
• TreeUtils.isTreeInStaticScope => TreePathUtil.isTreeInStaticScope
• TreeUtils.pathTillClass => TreePathUtil.pathTillClass
• TreeUtils.pathTillOfKind => TreePathUtil.pathTillOfKind

Closed issues:
#789, #3202, #4071, #4083, #4114, #4115.

Checker Framework 3.9.0

Version 3.9.0, January 4, 2021

New scripts checker/bin/wpi.sh and checker/bin/wpi-many.sh run whole-program inference, without modifying the source code of the target programs.

The -Ainfer command-line argument now infers

• method preconditions (@RequiresQualifiers, @RequiresNonNull)
• method postconditions (@EnsuresQualifiers, @EnsuresNonNull)
• @MonotonicNonNull

The Called Methods Checker supports the -AdisableReturnsReceiver command-line option.

The Format String Checker recognizes Error Prone's @FormatMethod annotation.

Use of @SuppressWarnings("fbc") to suppress initialization warnings is deprecated.

Implementation details:

Class renamings:

• StubParser => AnnotationFileParser
• Receiver => JavaExpression
  • also related class and method renamings
• In the Dataflow Framework:
  • ThisLiteralNode => ThisNode
  • ExplicitThisLiteralNode => ExplicitThisNode
  • ImplicitThisLiteralNode => ImplicitThisNode

Method deprecations:

• Deprecated AnnotatedTypeFactory.addAliasedAnnotation; use addAliasedTypeAnnotation

Closed issues:
#765, #2452, #2953, #3377, #3496, #3499, #3826, #3956, #3971, #3974, #3994, #4004, #4005, #4018, #4032, #4068, #4070.

Checker Framework 3.8.0

Version 3.8.0, December 1, 2020

The Initialized Fields Checker warns when a field is not initialized by a constructor. This is more general than the Initialization Checker, which only checks that @NonNull fields are initialized.

The manual describes how to modify an sbt build file to run the Checker Framework.

The -AwarnUnneededSuppressions command-line option warns only about suppression strings that contain a checker name.

The -AwarnUnneededSuppressionsExceptions=REGEX command-line option partially disables -AwarnUnneededSuppressions. Most users don't need this.

Implementation details:

Added classes SubtypeIsSubsetQualifierHierarchy and SubtypeIsSupersetQualifierHierarchy.

Moved the contractsUtils field from the visitor to the type factory.

Class renamings:

• ContractsUtils => ContractsFromMethod

Method renamings:

• ElementUtils.getVerboseName => ElementUtils.getQualifiedName
• ElementUtils.getSimpleName => ElementUtils.getSimpleSignature

Field renamings:

• AnnotatedTypeMirror.actualType => AnnotatedTypeMirror.underlyingType

Added a formal parameter to methods in MostlyNoElementQualifierHierarchy:

• leastUpperBoundWithElements
• greatestLowerBoundWithElements

Removed a formal parameter from methods in BaseTypeVisitor:

• checkPostcondition
• checkConditionalPostcondition

In Analysis.runAnalysisFor(), changed boolean parameter to enum BeforeOrAfter.

Removed org.checkerframework.framework.util.AnnotatedTypes#getIteratedType; use AnnotatedTypeFactory#getIterableElementType(ExpressionTree) instead.

Closed issues:
#3287, #3390, #3681, #3839, #3850, #3851, #3862, #3871, #3884, #3888, #3908, #3929, #3932, #3935.