diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index d0b8acbf71a..cfe6248ff80 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -1,7 +1,7 @@
# Contributing to the Checker Framework
Thank you for contributing to the Checker Framework! This project is a
-community effort of [more than 90
+community effort of [more than 110
developers](https://checkerframework.org/manual/#credits), plus countless
more people who have contributed bug reports and feature suggestions. We
couldn't do it without your help.
@@ -19,18 +19,30 @@ bug, and we want to fix it. Please report it.
## Submitting changes
-Please see the [pull requests](https://rawgit.com/typetools/checker-framework/master/docs/developer/developer-manual.html#pull-requests) section of the Developer Manual.
+Please see the [pull
+requests](https://rawgit.com/typetools/checker-framework/master/docs/developer/developer-manual.html#pull-requests)
+section of the Developer Manual.
+
+Submit changes to the annotated JDK at https://github.com/typetools/jdk/pulls .
+Annotations for other libraries can be contributed as stub files in this
+repository, in a fork of the library in https://github.com/typetools/, or
+in the library's own repository.
Do you want to contribute to the project, but you are not sure what issue
to fix or what feature to add? Use the tool in your daily work, and when
-you encounter a limitation that bothers you, fix that one.
+you encounter a limitation that bothers you, fix that one. The ["help
+wanted"](https://github.com/typetools/checker-framework/issues?q=is%3Aissue+is%3Aopen+label%3A%22help+wanted%22)
+label marks issues that require less deep knowledge and may be appropriate
+for a newcomer to the codebase.
## License
-By contributing, you agree that your contributions will be licensed under the existing [license](LICENSE.txt), usually GPL2 or MIT License.
+By contributing, you agree that your contributions will be licensed under the
+existing [license](LICENSE.txt), usually GPL2 or MIT License.
## Code of conduct
-In interactions with other people, please abide by the [Contributor Covenant](https://www.contributor-covenant.org/version/2/0/code_of_conduct).
+When interacting with other people, please abide by the [Contributor
+Covenant](https://www.contributor-covenant.org/version/2/0/code_of_conduct).
diff --git a/LICENSE.txt b/LICENSE.txt
index 8aa899e4c29..70d6a70fe2f 100644
--- a/LICENSE.txt
+++ b/LICENSE.txt
@@ -6,34 +6,39 @@ Most of the Checker Framework is licensed under the GNU General Public
License, version 2 (GPL2), with the classpath exception. The text of this
license appears below. This is the same license used for OpenJDK.
-A few parts of the Checker Framework have more permissive licenses.
-
- * The annotations are licensed under the MIT License. (The text of this
- license also appears below.) More specifically, all the parts of the
- Checker Framework that you might want to include with your own program
- use the MIT License. This is the checker-qual*.jar and
- checker-compat-qual*.jar files and all the files that appear in them:
- every file in a qual/ directory, plus utility files such as
- NullnessUtil.java, RegexUtil.java, SignednessUtil.java, etc. In
- addition, the cleanroom implementations of third-party annotations,
- which the Checker Framework recognizes as aliases for its own
- annotations, are licensed under the MIT License.
-
-Some external libraries that are included with the Checker Framework have
-different licenses.
+A few parts of the Checker Framework have more permissive licenses, notably
+the parts that you might want to include with your own program.
+
+ * The annotations and utility files are licensed under the MIT License.
+ (The text of this license also appears below.) This applies to the
+ checker-qual*.jar and all the files that appear in it: every file in a
+ qual/ directory, plus utility files FormatUtil.java,
+ I18nFormatUtil.java, NullnessUtil.java, Opt.java, PurityUnqualified.java,
+ RegexUtil.java, SignednessUtil.java, SignednessUtilExtra.java, and
+ UnitsTools.java. It also applies to the cleanroom implementations of
+ third-party annotations (in checker/src/testannotations/ and in
+ framework/src/main/java/org/jmlspecs/).
+
+The Checker Framework includes annotations for some libraries. Those in
+.astub files use the MIT License. Those in https://github.com/typetools/jdk
+(which appears in the annotated-jdk directory of file checker.jar) use the
+GPL2 license.
+
+Some external libraries that are included with the Checker Framework
+distribution have different licenses. Here are some examples.
* javaparser is dual licensed under the LGPL or the Apache license -- you
may use it under whichever one you want. (The javaparser source code
contains a file with the text of the GPL, but it is not clear why, since
- javaparser does not use the GPL.) See file stubparser/LICENSE
- and the source code of all its files.
+ javaparser does not use the GPL.) See
+ https://github.com/typetools/stubparser .
+
+ * Annotation Tools (https://github.com/typetools/annotation-tools) uses
+ the MIT license.
* Libraries in plume-lib (https://github.com/plume-lib/) are licensed
under the MIT License.
-The Checker Framework includes annotations for some libraries. Each annotated
-library uses the same license as the unannotated version of the library.
-
===========================================================================
The GNU General Public License (GPL)
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 4101d78127b..a9d5e18e382 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -10,25 +10,55 @@ pr:
jobs:
-- job: all_tests_jdk8
+- job: junit_tests_jdk8
+ dependsOn:
+ - junit_tests_jdk11
+ - nonjunit_tests_jdk11
+ - misc_jdk11
pool:
vmImage: 'ubuntu-latest'
container: mdernst/cf-ubuntu-jdk8:latest
steps:
- checkout: self
fetchDepth: 25
- - bash: ./checker/bin-devel/test-cftests-all.sh
- displayName: test-cftests-all.sh
-- job: all_tests_jdk11
+ - bash: ./checker/bin-devel/test-cftests-junit.sh
+ displayName: test-cftests-junit.sh
+- job: junit_tests_jdk11
pool:
vmImage: 'ubuntu-latest'
container: mdernst/cf-ubuntu-jdk11:latest
steps:
- checkout: self
fetchDepth: 25
- - bash: ./checker/bin-devel/test-cftests-all.sh
- displayName: test-cftests-all.sh
+ - bash: ./checker/bin-devel/test-cftests-junit.sh
+ displayName: test-cftests-junit.sh
+- job: nonjunit_tests_jdk8
+ dependsOn:
+ - junit_tests_jdk11
+ - nonjunit_tests_jdk11
+ - misc_jdk11
+ pool:
+ vmImage: 'ubuntu-latest'
+ container: mdernst/cf-ubuntu-jdk8:latest
+ steps:
+ - checkout: self
+ fetchDepth: 25
+ - bash: ./checker/bin-devel/test-cftests-nonjunit.sh
+ displayName: test-cftests-nonjunit.sh
+- job: nonjunit_tests_jdk11
+ pool:
+ vmImage: 'ubuntu-latest'
+ container: mdernst/cf-ubuntu-jdk11:latest
+ steps:
+ - checkout: self
+ fetchDepth: 25
+ - bash: ./checker/bin-devel/test-cftests-nonjunit.sh
+ displayName: test-cftests-nonjunit.sh
- job: misc_jdk8
+ dependsOn:
+ - junit_tests_jdk11
+ - nonjunit_tests_jdk11
+ - misc_jdk11
pool:
vmImage: 'ubuntu-latest'
container: mdernst/cf-ubuntu-jdk8-plus:latest
@@ -47,6 +77,11 @@ jobs:
- bash: ./checker/bin-devel/test-misc.sh
displayName: test-misc.sh
- job: cf_inference_jdk8
+ dependsOn:
+ - junit_tests_jdk11
+ - nonjunit_tests_jdk11
+ - misc_jdk11
+ - cf_inference_jdk11
pool:
vmImage: 'ubuntu-latest'
container: mdernst/cf-ubuntu-jdk8:latest
@@ -65,6 +100,11 @@ jobs:
- bash: ./checker/bin-devel/test-cf-inference.sh
displayName: test-cf-inference.sh
- job: daikon_jdk8
+ dependsOn:
+ - junit_tests_jdk11
+ - nonjunit_tests_jdk11
+ - misc_jdk11
+ - daikon_jdk11
pool:
vmImage: 'ubuntu-latest'
container: mdernst/cf-ubuntu-jdk8:latest
@@ -83,6 +123,11 @@ jobs:
- bash: ./checker/bin-devel/test-daikon.sh
displayName: test-daikon.sh
- job: guava_jdk8
+ dependsOn:
+ - junit_tests_jdk11
+ - nonjunit_tests_jdk11
+ - misc_jdk11
+ - guava_jdk11
pool:
vmImage: 'ubuntu-latest'
container: mdernst/cf-ubuntu-jdk8:latest
@@ -103,6 +148,11 @@ jobs:
- bash: ./checker/bin-devel/test-guava.sh
displayName: test-guava.sh
- job: plume_lib_jdk8
+ dependsOn:
+ - junit_tests_jdk11
+ - nonjunit_tests_jdk11
+ - misc_jdk11
+ - plume_lib_jdk11
pool:
vmImage: 'ubuntu-latest'
container: mdernst/cf-ubuntu-jdk8:latest
@@ -120,19 +170,24 @@ jobs:
fetchDepth: 25
- bash: ./checker/bin-devel/test-plume-lib.sh
displayName: test-plume-lib.sh
-- job: downstream_jdk11
+- job: downstream_jdk8
+ dependsOn:
+ - junit_tests_jdk11
+ - nonjunit_tests_jdk11
+ - misc_jdk11
+ - downstream_jdk11
pool:
vmImage: 'ubuntu-latest'
- container: mdernst/cf-ubuntu-jdk11:latest
+ container: mdernst/cf-ubuntu-jdk8:latest
steps:
- checkout: self
fetchDepth: 25
- bash: ./checker/bin-devel/test-downstream.sh
displayName: test-downstream.sh
-- job: downstream_jdk8
+- job: downstream_jdk11
pool:
vmImage: 'ubuntu-latest'
- container: mdernst/cf-ubuntu-jdk8:latest
+ container: mdernst/cf-ubuntu-jdk11:latest
steps:
- checkout: self
fetchDepth: 25
diff --git a/build.gradle b/build.gradle
index 9c25ac6ec20..7ffd2d6c521 100644
--- a/build.gradle
+++ b/build.gradle
@@ -4,14 +4,14 @@ plugins {
// https://plugins.gradle.org/plugin/com.github.johnrengelman.shadow (v5 requires Gradle 5)
id 'com.github.johnrengelman.shadow' version '6.0.0'
// https://plugins.gradle.org/plugin/de.undercouch.download
- id "de.undercouch.download" version "4.0.4"
+ id "de.undercouch.download" version "4.1.1"
id 'java'
// https://github.com/tbroyer/gradle-errorprone-plugin
id "net.ltgt.errorprone" version "1.2.1"
// https://plugins.gradle.org/plugin/org.ajoberstar.grgit
id 'org.ajoberstar.grgit' version '4.0.2' apply false
// https://github.com/n0mer/gradle-git-properties ; target is: generateGitProperties
- id "com.gorylenko.gradle-git-properties" version "2.2.2"
+ id "com.gorylenko.gradle-git-properties" version "2.2.3"
}
apply plugin: "de.undercouch.download"
@@ -101,7 +101,7 @@ allprojects {
// * any new checkers have been added,
// * the patch level is 9 (keep the patch level as a single digit), or
// * backward-incompatible changes have been made to APIs or elsewhere.
- version '3.5.0'
+ version '3.6.1-SNAPSHOT'
repositories {
mavenCentral()
@@ -220,8 +220,43 @@ allprojects {
if (isJava8) {
options.forkOptions.jvmArgs += ["-Xbootclasspath/p:${configurations.javacJar.asPath}"]
}
- // Don't use error-prone by default
- options.errorprone.enabled = false
+
+ // Error prone depends on checker-qual.jar, so don't run it on that project to avoid a circular dependency.
+ // All the classes in checker-qual are also in checker, so they are checked.
+ // TODO: enable Error Prone on test classes.
+ if (name.is('compileJava') && !project.name.startsWith('checker-qual')){
+ println "${project.name} ${name}"
+ // Error Prone must be available in the annotation processor path
+ options.annotationProcessorPath = configurations.errorprone
+ // Enable Error Prone
+ options.errorprone.enabled = true
+ options.errorprone.disableWarningsInGeneratedCode = true
+ options.errorprone.errorproneArgs = [
+ // Many compiler classes are interned.
+ '-Xep:ReferenceEquality:OFF',
+ // These might be worth fixing.
+ '-Xep:DefaultCharset:OFF',
+ // Not useful to suggest Splitter; maybe clean up.
+ '-Xep:StringSplitter:OFF',
+ // Too broad, rejects seemingly-correct code.
+ '-Xep:EqualsGetClass:OFF',
+ // Not a real problem
+ '-Xep:MixedMutabilityReturnType:OFF',
+ // Don't want to add a dependency to ErrorProne.
+ '-Xep:AnnotateFormatMethod:OFF',
+ // Warns for every use of "@checker_framework.manual"
+ '-Xep:InvalidBlockTag:OFF',
+ // @SuppressWarnings doesn't work: https://github.com/google/error-prone/issues/1650
+ '-Xep:InlineFormatString:OFF',
+ // -Werror halts the build if Error Prone issues a warning, which ensures that
+ // the errors get fixed. On the downside, Error Prone (or maybe the compiler?)
+ // stops as soon as it issues one warning, rather than outputting them all.
+ // https://github.com/google/error-prone/issues/436
+ '-Werror',
+ ]
+ } else {
+ options.errorprone.enabled = false
+ }
}
}
}
@@ -270,6 +305,9 @@ def createCheckTypeTask(projectName, checker, shortName, args = []) {
'-processor', "${checker}",
'-proc:only',
'-Xlint:-processing',
+ '-Xmaxerrs', '10000',
+ '-Xmaxwarns', '10000',
+ '-ArequirePrefixInWarningSuppressions',
]
options.compilerArgs += args
@@ -305,7 +343,10 @@ List getJavaFilesToFormat(projectName) {
}
// Collect all java files in tests directory
fileTree("${project(projectName).projectDir}/tests").visit { details ->
- if (!details.path.contains("nullness-javac-errors") && details.name.endsWith('java')) {
+ if (!details.path.contains("nullness-javac-errors")
+ && !details.path.contains("returnsreceiverdelomboked")
+ && !details.path.contains("build")
+ && details.name.endsWith('java')) {
javaFiles.add(details.file)
}
}
@@ -316,7 +357,7 @@ List getJavaFilesToFormat(projectName) {
}
}
- // Collect all java files in jtreg directory
+ // Collect all java files in jtregJdk11 directory
fileTree("${project(projectName).projectDir}/jtregJdk11").visit { details ->
if (!details.path.contains("nullness-javac-errors") && details.name.endsWith('java')) {
javaFiles.add(details.file)
@@ -524,7 +565,7 @@ subprojects {
// https://mvnrepository.com/artifact/com.google.errorprone/error_prone_core
// If you update this:
// * Temporarily comment out "-Werror" elsewhere in this file
- // * Repeatedly run `./gradlew clean runErrorProne` and fix all errors
+ // * Repeatedly run `./gradlew clean compileJava` and fix all errors
// * Uncomment "-Werror"
errorprone group: 'com.google.errorprone', name: 'error_prone_core', version: '2.4.0'
}
@@ -633,12 +674,14 @@ subprojects {
}
// Add tasks to run various checkers on all the main source sets.
- // TODO: fix or suppress all not.interned warnings and remove the suppression here.
- createCheckTypeTask(project.name, 'org.checkerframework.checker.interning.InterningChecker', 'Interning', ['-AsuppressWarnings=not.interned'])
- createCheckTypeTask(project.name, 'org.checkerframework.checker.nullness.NullnessChecker', 'Nullness')
- createCheckTypeTask(project.name, 'org.checkerframework.checker.nullness.NullnessChecker', 'WorkingNullness', ['-AskipUses=com.sun.*', '-AskipDefs=org.checkerframework.checker.*|org.checkerframework.common.*|org.checkerframework.framework.*|org.checkerframework.dataflow.cfg.CFGBuilder'])
+ // These pass and are run by nonJunitTests.
+ createCheckTypeTask(project.name, 'org.checkerframework.checker.interning.InterningChecker', 'Interning')
+ createCheckTypeTask(project.name, 'org.checkerframework.checker.nullness.NullnessChecker', 'NullnessOnlyAnnotatedFor', ['-AskipUses=com.sun.*', '-AuseConservativeDefaultsForUncheckedCode=source'])
createCheckTypeTask(project.name, 'org.checkerframework.framework.util.PurityChecker', 'Purity')
createCheckTypeTask(project.name, 'org.checkerframework.checker.signature.SignatureChecker', 'Signature')
+ // These pass on some subprojects, which nonJunitTests runs. TODO: Incrementally add @AnnotatedFor on classes.
+ createCheckTypeTask(project.name, 'org.checkerframework.checker.nullness.NullnessChecker', 'Nullness', ['-AskipUses=com.sun.*'])
+
// Add jtregTests to framework and checker modules
if (project.name.is('framework') || project.name.is('checker')) {
@@ -757,51 +800,9 @@ subprojects {
}
}
- // Create a runErrorProne task.
- tasks.create(name: 'runErrorProne', type: JavaCompile, group: 'Verification') {
- description 'Run the error-prone compiler on the main sources'
-
- source = sourceSets.main.java.asFileTree
- classpath = sourceSets.main.compileClasspath.asFileTree
- destinationDir = new File("${buildDir}", 'errorprone')
-
- // Error Prone must be available in the annotation processor path
- options.annotationProcessorPath = configurations.errorprone
- // Enable Error Prone
- options.errorprone.enabled = true
- options.errorprone.disableWarningsInGeneratedCode = true
- options.errorprone.errorproneArgs = [
- // Many compiler classes are interned.
- '-Xep:ReferenceEquality:OFF',
- // These might be worth fixing.
- '-Xep:DefaultCharset:OFF',
- // Not useful to suggest Splitter; maybe clean up.
- '-Xep:StringSplitter:OFF',
- // Too broad, rejects seemingly-correct code.
- '-Xep:EqualsGetClass:OFF',
- // Not a real problem
- '-Xep:MixedMutabilityReturnType:OFF',
- // Don't want to add a dependency to ErrorProne.
- '-Xep:AnnotateFormatMethod:OFF',
- // Warns for every use of "@checker_framework.manual"
- '-Xep:InvalidBlockTag:OFF',
- // @SuppressWarnings doesn't work: https://github.com/google/error-prone/issues/1650
- '-Xep:InlineFormatString:OFF',
- // -Werror halts the build if Error Prone issues a warning, which ensures that
- // the errors get fixed. On the downside, Error Prone (or maybe the compiler?)
- // stops as soon as it one warning, rather than outputting them all.
- // https://github.com/google/error-prone/issues/436
- '-Werror',
- ]
- }
-
// Create a nonJunitTests task per project
tasks.create(name: 'nonJunitTests', group: 'Verification') {
description 'Run all Checker Framework tests except for the Junit tests.'
- dependsOn('checkInterning', 'checkPurity', 'checkSignature', 'checkWorkingNullness')
- if (project.name.is('framework') || project.name.is('checker')) {
- dependsOn('checkCompilerMessages', 'jtregTests')
- }
if (project.name.is('framework')) {
dependsOn('wholeProgramInferenceTests', 'loaderTests')
}
@@ -815,15 +816,31 @@ subprojects {
if (project.name.is('dataflow')) {
dependsOn('liveVariableTest')
+ dependsOn('issue3447Test')
+ }
+ }
+
+ // Create a typecheck task per project (dogfooding the Checker Framework on itself).
+ // This isn't a test of the Checker Framework as the test and nonJunitTests are.
+ tasks.create(name: 'typecheck', group: 'Verification') {
+ description 'Run the Checker Framework on itself'
+ dependsOn('checkInterning', 'checkPurity', 'checkSignature')
+ if (project.name.is('framework') || project.name.is('checker')) {
+ dependsOn('checkNullnessOnlyAnnotatedFor')
+ } else {
+ dependsOn('checkNullness')
+ }
+ if (project.name.is('framework') || project.name.is('checker')) {
+ dependsOn('checkCompilerMessages', 'jtregTests')
}
}
// Create an allTests task per project.
- // allTests = test + nonJunitTests
+ // allTests = test + nonJunitTests + typecheck
tasks.create(name: 'allTests', group: 'Verification') {
description 'Run all Checker Framework tests'
// The 'test' target is just the JUnit tests.
- dependsOn('nonJunitTests', 'test')
+ dependsOn('nonJunitTests', 'test', 'typecheck')
}
task javadocPrivate(dependsOn: javadoc) {
@@ -845,6 +862,7 @@ task checkBasicStyle(group: 'Format') {
'.gradle',
'.idea',
'.plume-scripts',
+ '.run-google-java-format',
'annotated',
'api',
'bib',
@@ -877,6 +895,8 @@ task checkBasicStyle(group: 'Format') {
'manual.html',
'manual.html-e',
'junit.*.properties',
+ 'checker/dist/META-INF/maven/org.apache.bcel/bcel/pom.xml',
+ 'checker/dist/META-INF/maven/org.apache.commons/commons-text/pom.xml',
'framework/src/main/resources/git.properties']
doLast {
FileTree tree = fileTree(dir: projectDir)
@@ -889,12 +909,19 @@ task checkBasicStyle(group: 'Format') {
boolean failed = false
tree.visit {
if (!it.file.isDirectory()) {
- int isBlankLine
+ boolean blankLineAtEnd = false
+ String fileName = it.file.getName()
+ boolean checkTabs = !fileName.equals("Makefile")
it.file.eachLine { line ->
if (line.endsWith(' ')) {
println("Trailing whitespace: ${it.file.absolutePath}")
failed = true
}
+ if (checkTabs && line.contains('\t')) {
+ println("Contains tab (use spaces): ${it.file.absolutePath}")
+ failed = true
+ checkTabs = false
+ }
if (!line.startsWith('\\') &&
(line.matches('^.* (else|finally|try)\\{}.*$')
|| line.matches('^.*}(catch|else|finally) .*$')
@@ -904,13 +931,13 @@ task checkBasicStyle(group: 'Format') {
failed = true
}
if (line.isEmpty()) {
- isBlankLine++;
+ blankLineAtEnd = true;
} else {
- isBlankLine = 0;
+ blankLineAtEnd = false;
}
}
- if (isBlankLine > 1) {
+ if (blankLineAtEnd) {
println("Blank line at end of file: ${it.file.absolutePath}")
failed = true
}
diff --git a/changelog.txt b/changelog.txt
index a053d6d8121..2b1723d574e 100644
--- a/changelog.txt
+++ b/changelog.txt
@@ -1,3 +1,37 @@
+Version 3.6.0, August 3, 2020
+
+The Interning Checker supports method annotations @EqualsMethod and
+@CompareToMethod. Place them on methods like equals(), compareTo(), and
+compare() to permit certain uses of == on non-interned values.
+
+Added an overloaded version of NullnessUtil.castNonNull that takes an error message.
+
+Added a new option `-Aversion` to print the version of the Checker Framework.
+
+New CFGVisualizeLauncher command-line arguments:
+ * `--outputdir`: directory in which to write output files
+ * `--string`: print the control flow graph in the terminal
+All CFGVisualizeLauncher command-line arguments now start with `--` instead of `-`.
+
+Implementation details:
+
+commonAssignmentCheck() now takes an additional argument. Type system
+authors must update their overriding implementations.
+
+Renamed GenericAnnotatedTypeFactory#addAnnotationsFromDefaultQualifierForUse to
+#addAnnotationsFromDefaultForType and
+BaseTypeValidator#shouldCheckTopLevelDeclaredType to
+#shouldCheckTopLevelDeclaredOrPrimitiveType
+
+Removed org.checkerframework.framework.test.FrameworkPer(Directory/File)Test classes.
+Use CheckerFrameworkPer(Directory/File)Test instead.
+
+Closed issues:
+1395, 2483, 3207, 3223, 3224, 3313, 3381, 3422, 3424, 3428, 3429, 3438, 3442,
+3443, 3447, 3449, 3461, 3482, 3485, 3495, 3500, 3528.
+
+---------------------------------------------------------------------------
+
Version 3.5.0, July 1, 2020
Use "allcheckers:" instead of "all:" as a prefix in a warning suppression string.
@@ -111,7 +145,7 @@ Renamings:
For collection methods with `Object` formal parameter type, such as
contains, indexOf, and remove, the annotated JDK now forbids null as an
argument. To make the Nullness Checker permit null, pass
-`-Astubs=checker.jar/collection-object-parameters-may-be-null.astub`.
+`-Astubs=collection-object-parameters-may-be-null.astub`.
The argument to @SuppressWarnings can be a substring of a message key that
extends at each end to a period or an end of the key. (Previously, any
diff --git a/checker-qual-android/build.gradle b/checker-qual-android/build.gradle
index 022874e4e35..92eea98ad90 100644
--- a/checker-qual-android/build.gradle
+++ b/checker-qual-android/build.gradle
@@ -10,6 +10,7 @@ task copySources(type: Copy, dependsOn: ':checker-qual:copySources') {
}
from files('../checker-qual/src/main')
include "**/*.java"
+ exclude "**/SignednessUtilExtra.java"
into file('src/main')
// Not read only because "replaceAnnotations" tasks writes to the files.
diff --git a/checker-qual/build.gradle b/checker-qual/build.gradle
index 121e0c1067c..69c84442fbb 100644
--- a/checker-qual/build.gradle
+++ b/checker-qual/build.gradle
@@ -4,7 +4,7 @@ buildscript {
}
dependencies {
// Create OSGI bundles
- classpath "biz.aQute.bnd:biz.aQute.bnd.gradle:5.1.1"
+ classpath "biz.aQute.bnd:biz.aQute.bnd.gradle:5.1.2"
}
}
@@ -17,16 +17,19 @@ task copySources(type: Copy) {
}
from files('../checker/src/main/java', '../dataflow/src/main/java', '../framework/src/main/java')
+ // Qualifiers
+ include '**/org/checkerframework/**/qual/*.java'
+ include '**/PurityUnqualified.java' // TODO: Should we move this into a qual directory?
+ // Utility classes
+ // If you change this list, also update ../LICENSE.txt .
include "**/FormatUtil.java"
+ include "**/I18nFormatUtil.java"
include "**/NullnessUtil.java"
+ include "**/Opt.java"
include "**/RegexUtil.java"
- include "**/UnitsTools.java"
include "**/SignednessUtil.java"
- include "**/I18nFormatUtil.java"
- include '**/org/checkerframework/**/qual/*.java'
- include '**/Opt.java'
- // TODO: Should we move this into a qual directory?
- include '**/PurityUnqualified.java'
+ include "**/SignednessUtilExtra.java"
+ include "**/UnitsTools.java"
// Make files read only.
fileMode(0444)
diff --git a/checker/bin-devel/git.pre-commit b/checker/bin-devel/git.pre-commit
index 486ad95cc47..b2d1f81505c 100755
--- a/checker/bin-devel/git.pre-commit
+++ b/checker/bin-devel/git.pre-commit
@@ -12,13 +12,15 @@ set -e
# Need to keep checked files in sync with getJavaFilesToFormat in build.gradle.
# Otherwise `./gradlew reformat` might not reformat a file that this
# hook complains about.
-CHANGED_JAVA_FILES=`git diff --staged --name-only --diff-filter=ACM | grep '\.java$' | grep -v '/jdk/' | grep -v 'stubparser/' | grep -v '/nullness-javac-errors/' ` || true
-# echo CHANGED_JAVA_FILES "'"${CHANGED_JAVA_FILES}"'"
-if [ ! -z "$CHANGED_JAVA_FILES" ]; then
+CHANGED_JAVA_FILES=$(git diff --staged --name-only --diff-filter=ACM | grep '\.java$' | grep -v '/jdk/' | grep -v 'stubparser/' | grep -v '/nullness-javac-errors/' | grep -v 'dataflow/manual/examples/' ) || true
+# echo "CHANGED_JAVA_FILES=${CHANGED_JAVA_FILES}"
+if [ -n "$CHANGED_JAVA_FILES" ]; then
./gradlew getCodeFormatScripts -q
## For debugging:
# echo "CHANGED_JAVA_FILES: ${CHANGED_JAVA_FILES}"
- python checker/bin-devel/.run-google-java-format/check-google-java-format.py --aosp ${CHANGED_JAVA_FILES} || (echo "Try running: ./gradlew reformat" && /bin/false)
+
+ # shellcheck disable=SC2086
+ python checker/bin-devel/.run-google-java-format/check-google-java-format.py --aosp ${CHANGED_JAVA_FILES} || (echo "Problem in pre-commit. Try running: ./gradlew reformat" && /bin/false)
BRANCH=$(git rev-parse --abbrev-ref HEAD)
if [ "$BRANCH" = "master" ]; then
@@ -34,11 +36,14 @@ fi
# This is to handle non-.java files, since the above already handled .java files.
# May need to remove files that are allowed to have trailing whitespace or are
# not text files.
-CHANGED_FILES=`git diff --staged --name-only --diff-filter=ACM | grep -v '\.class$' | grep -v '\.gz$' | grep -v '\.jar$' | grep -v '\.pdf$' | grep -v '\.png$' | grep -v '\.xcf$'` || true
-if [ ! -z "$CHANGED_FILES" ]; then
+CHANGED_FILES=$(git diff --staged --name-only --diff-filter=ACM | grep -v '\.class$' | grep -v '\.gz$' | grep -v '\.jar$' | grep -v '\.pdf$' | grep -v '\.png$' | grep -v '\.xcf$') || true
+if [ -n "$CHANGED_FILES" ]; then
+ ## For debugging:
# echo "CHANGED_FILES: ${CHANGED_FILES}"
- FILES_WITH_TRAILING_SPACES=`grep -l -s '[[:blank:]]$' ${CHANGED_FILES} 2>&1` || true
- if [ ! -z "$FILES_WITH_TRAILING_SPACES" ]; then
+
+ # shellcheck disable=SC2086
+ FILES_WITH_TRAILING_SPACES=$(grep -l -s '[[:blank:]]$' ${CHANGED_FILES} 2>&1) || true
+ if [ -n "$FILES_WITH_TRAILING_SPACES" ]; then
echo "Some files have trailing whitespace: ${FILES_WITH_TRAILING_SPACES}" && exit 1
fi
fi
diff --git a/checker/bin-devel/test-daikon-part1.sh b/checker/bin-devel/test-daikon-part1.sh
index 671590df1a6..92991762130 100755
--- a/checker/bin-devel/test-daikon-part1.sh
+++ b/checker/bin-devel/test-daikon-part1.sh
@@ -19,7 +19,7 @@ git log | head -n 5
make compile
if [ "$TRAVIS" = "true" ] ; then
# Travis kills a job if it runs 10 minutes without output
- time make JAVACHECK_EXTRA_ARGS=-Afilenames -C java check-part1
+ time make JAVACHECK_EXTRA_ARGS=-Afilenames -C java typecheck-part1
else
- time make -C java check-part1
+ time make -C java typecheck-part1
fi
diff --git a/checker/bin-devel/test-daikon-part2.sh b/checker/bin-devel/test-daikon-part2.sh
index cb2de5bb6bf..e4313823320 100755
--- a/checker/bin-devel/test-daikon-part2.sh
+++ b/checker/bin-devel/test-daikon-part2.sh
@@ -19,7 +19,7 @@ git log | head -n 5
make compile
if [ "$TRAVIS" = "true" ] ; then
# Travis kills a job if it runs 10 minutes without output
- time make JAVACHECK_EXTRA_ARGS=-Afilenames -C java check-part2
+ time make JAVACHECK_EXTRA_ARGS=-Afilenames -C java typecheck-part2
else
- time make -C java check-part2
+ time make -C java typecheck-part2
fi
diff --git a/checker/bin-devel/test-misc.sh b/checker/bin-devel/test-misc.sh
index c5fd22fe78e..a93a57713dd 100755
--- a/checker/bin-devel/test-misc.sh
+++ b/checker/bin-devel/test-misc.sh
@@ -12,16 +12,17 @@ SCRIPTDIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
source "$SCRIPTDIR"/build.sh
-# Code style and formatting
-./gradlew checkBasicStyle checkFormat --console=plain --warning-mode=all --no-daemon
-
-# Run error-prone
-./gradlew runErrorProne --console=plain --warning-mode=all --no-daemon
+# Code style, formatting, and plugable type-checking
+./gradlew checkBasicStyle checkFormat typecheck --console=plain --warning-mode=all --no-daemon
# HTML legality
./gradlew htmlValidate --console=plain --warning-mode=all --no-daemon
# Javadoc documentation
+# Uncomment this line temporarily for refactorings that touch a lot of code that
+# you don't understand. Then, recomment it as soon as the pull request is merged.
+# SKIPJAVADOC=1
+if [ -z "$SKIPJAVADOC" ]; then
status=0
./gradlew javadoc --console=plain --warning-mode=all --no-daemon || status=1
./gradlew javadocPrivate --console=plain --warning-mode=all --no-daemon || status=1
@@ -30,6 +31,8 @@ status=0
(./gradlew javadocDoclintAll --console=plain --warning-mode=all --no-daemon > /tmp/warnings-jda.txt 2>&1) || true
/tmp/"$USER"/plume-scripts/ci-lint-diff /tmp/warnings-jda.txt || status=1
if [ $status -ne 0 ]; then exit $status; fi
+fi # end of "if [ -z $SKIPJAVADOC ]"
+
# User documentation
make -C docs/manual all
diff --git a/checker/jtreg/nullness/defaultsPersist/ReferenceInfoUtil.java b/checker/jtreg/nullness/defaultsPersist/ReferenceInfoUtil.java
index 1743208fbc7..9431e984ae7 100644
--- a/checker/jtreg/nullness/defaultsPersist/ReferenceInfoUtil.java
+++ b/checker/jtreg/nullness/defaultsPersist/ReferenceInfoUtil.java
@@ -15,7 +15,7 @@
import java.util.Arrays;
import java.util.List;
import org.checkerframework.javacutil.Pair;
-import org.checkerframework.javacutil.PluginUtil;
+import org.checkerframework.javacutil.SystemUtil;
public class ReferenceInfoUtil {
@@ -159,7 +159,7 @@ && areEquals(p1.type_index, p2.type_index)
public static String positionCompareStr(
TypeAnnotation.Position p1, TypeAnnotation.Position p2) {
- return PluginUtil.joinLines(
+ return SystemUtil.joinLines(
"type = " + p1.type + ", " + p2.type,
"offset = " + p1.offset + ", " + p2.offset,
"lvarOffset = " + p1.lvarOffset + ", " + p2.lvarOffset,
@@ -234,7 +234,7 @@ public ComparisonException(
}
public String toString() {
- return PluginUtil.joinLines(
+ return SystemUtil.joinLines(
super.toString(),
"\tExpected: "
+ expected.size()
diff --git a/checker/jtreg/nullness/inheritDeclAnnoPersist/Extends.java b/checker/jtreg/nullness/inheritDeclAnnoPersist/Extends.java
index f895a3027aa..20b905c97b5 100644
--- a/checker/jtreg/nullness/inheritDeclAnnoPersist/Extends.java
+++ b/checker/jtreg/nullness/inheritDeclAnnoPersist/Extends.java
@@ -1,4 +1,4 @@
-import org.checkerframework.javacutil.PluginUtil;
+import org.checkerframework.javacutil.SystemUtil;
/*
* @test
@@ -37,7 +37,7 @@ public String m3() {
class TestWrapper {
public static String wrap(String... method) {
- return PluginUtil.joinLines(
- "class Test extends Super {", PluginUtil.joinLines(method), "}");
+ return SystemUtil.joinLines(
+ "class Test extends Super {", SystemUtil.joinLines(method), "}");
}
}
diff --git a/checker/jtreg/nullness/inheritDeclAnnoPersist/Implements.java b/checker/jtreg/nullness/inheritDeclAnnoPersist/Implements.java
index 247916f2b7e..55b5ce89697 100644
--- a/checker/jtreg/nullness/inheritDeclAnnoPersist/Implements.java
+++ b/checker/jtreg/nullness/inheritDeclAnnoPersist/Implements.java
@@ -1,4 +1,4 @@
-import org.checkerframework.javacutil.PluginUtil;
+import org.checkerframework.javacutil.SystemUtil;
/*
* @test
@@ -23,7 +23,7 @@ public String m1() {
class TestWrapper {
public static String wrap(String... method) {
- return PluginUtil.joinLines(
- "class Test extends AbstractClass {", PluginUtil.joinLines(method), "}");
+ return SystemUtil.joinLines(
+ "class Test extends AbstractClass {", SystemUtil.joinLines(method), "}");
}
}
diff --git a/checker/jtreg/nullness/inheritDeclAnnoPersist/ReferenceInfoUtil.java b/checker/jtreg/nullness/inheritDeclAnnoPersist/ReferenceInfoUtil.java
index 02c9c8256e0..e3d6172521a 100644
--- a/checker/jtreg/nullness/inheritDeclAnnoPersist/ReferenceInfoUtil.java
+++ b/checker/jtreg/nullness/inheritDeclAnnoPersist/ReferenceInfoUtil.java
@@ -12,7 +12,7 @@
import java.util.ArrayList;
import java.util.List;
import java.util.StringJoiner;
-import org.checkerframework.javacutil.PluginUtil;
+import org.checkerframework.javacutil.SystemUtil;
public class ReferenceInfoUtil {
@@ -123,7 +123,7 @@ public String toString() {
throw new RuntimeException(e);
}
}
- return PluginUtil.joinLines(
+ return SystemUtil.joinLines(
super.toString(),
"\tExpected: "
+ expected.size()
diff --git a/checker/jtreg/sortwarnings/ErrorOrders.out b/checker/jtreg/sortwarnings/ErrorOrders.out
index ceddf61d07b..87f467eac8e 100644
--- a/checker/jtreg/sortwarnings/ErrorOrders.out
+++ b/checker/jtreg/sortwarnings/ErrorOrders.out
@@ -26,46 +26,46 @@ ErrorOrders.java:24:47: compiler.err.proc.messager: [expression.unparsable.type.
ErrorOrders.java:24:55: compiler.err.proc.messager: [assignment.type.incompatible] incompatible types in assignment.
found : @LTLengthOf(value="p2") int
required: @LTLengthOf(value="[error for expression: This isn't an expression; error: Invalid 'This isn't an expression' because is an invalid expression]") int
-ErrorOrders.java:29:15: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:29:15: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p1 of test4.
found : @LowerBoundUnknown int
required: @GTENegativeOne int
-ErrorOrders.java:29:15: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:29:15: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p1 of test4.
found : @UpperBoundUnknown int
required: @UpperBoundBottom int
-ErrorOrders.java:29:24: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:29:24: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p2 of test4.
found : @LowerBoundUnknown int
required: @GTENegativeOne int
-ErrorOrders.java:29:24: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:29:24: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p2 of test4.
found : @UpperBoundUnknown int
required: @UpperBoundBottom int
-ErrorOrders.java:29:25: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:29:25: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p1 of test4.
found : @LowerBoundUnknown int
required: @GTENegativeOne int
-ErrorOrders.java:29:25: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:29:25: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p1 of test4.
found : @UpperBoundUnknown int
required: @UpperBoundBottom int
-ErrorOrders.java:29:29: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:29:29: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p2 of test4.
found : @LowerBoundUnknown int
required: @GTENegativeOne int
-ErrorOrders.java:29:29: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:29:29: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p2 of test4.
found : @UpperBoundUnknown int
required: @UpperBoundBottom int
-ErrorOrders.java:29:33: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:29:33: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p3 of test4.
found : @UnknownVal int @UnknownVal []
required: @UnknownVal int []
-ErrorOrders.java:29:37: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:29:37: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p4 of test4.
found : @SameLenUnknown int @SameLen("p4") []
required: @SameLenUnknown int @SameLenBottom []
-ErrorOrders.java:29:41: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:29:41: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p5 of test4.
found : @UnknownVal int
required: int
-ErrorOrders.java:29:46: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:29:46: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p3 of test4.
found : @UnknownVal int @UnknownVal []
required: @UnknownVal int []
-ErrorOrders.java:29:50: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:29:50: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p4 of test4.
found : @SameLenUnknown int @SameLen("p4") []
required: @SameLenUnknown int @SameLenBottom []
-ErrorOrders.java:29:54: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:29:54: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p5 of test4.
found : @UnknownVal int
required: int
ErrorOrders.java:33:47: compiler.err.proc.messager: [expression.unparsable.type.invalid] Expression invalid in dependent type annotation: [error for expression: This isn't an expression; error: Invalid 'This isn't an expression' because is an invalid expression]
@@ -95,46 +95,46 @@ ErrorOrders.java:56:47: compiler.err.proc.messager: [expression.unparsable.type.
ErrorOrders.java:56:55: compiler.err.proc.messager: [assignment.type.incompatible] incompatible types in assignment.
found : @LTLengthOf(value="p2") int
required: @LTLengthOf(value="[error for expression: This isn't an expression; error: Invalid 'This isn't an expression' because is an invalid expression]") int
-ErrorOrders.java:61:15: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:61:15: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p1 of test4.
found : @LowerBoundUnknown int
required: @GTENegativeOne int
-ErrorOrders.java:61:15: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:61:15: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p1 of test4.
found : @UpperBoundUnknown int
required: @UpperBoundBottom int
-ErrorOrders.java:61:24: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:61:24: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p2 of test4.
found : @LowerBoundUnknown int
required: @GTENegativeOne int
-ErrorOrders.java:61:24: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:61:24: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p2 of test4.
found : @UpperBoundUnknown int
required: @UpperBoundBottom int
-ErrorOrders.java:61:25: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:61:25: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p1 of test4.
found : @LowerBoundUnknown int
required: @GTENegativeOne int
-ErrorOrders.java:61:25: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:61:25: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p1 of test4.
found : @UpperBoundUnknown int
required: @UpperBoundBottom int
-ErrorOrders.java:61:29: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:61:29: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p2 of test4.
found : @LowerBoundUnknown int
required: @GTENegativeOne int
-ErrorOrders.java:61:29: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:61:29: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p2 of test4.
found : @UpperBoundUnknown int
required: @UpperBoundBottom int
-ErrorOrders.java:61:33: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:61:33: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p3 of test4.
found : @UnknownVal int @UnknownVal []
required: @UnknownVal int []
-ErrorOrders.java:61:37: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:61:37: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p4 of test4.
found : @SameLenUnknown int @SameLen("p4") []
required: @SameLenUnknown int @SameLenBottom []
-ErrorOrders.java:61:41: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:61:41: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p5 of test4.
found : @UnknownVal int
required: int
-ErrorOrders.java:61:46: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:61:46: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p3 of test4.
found : @UnknownVal int @UnknownVal []
required: @UnknownVal int []
-ErrorOrders.java:61:50: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:61:50: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p4 of test4.
found : @SameLenUnknown int @SameLen("p4") []
required: @SameLenUnknown int @SameLenBottom []
-ErrorOrders.java:61:54: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+ErrorOrders.java:61:54: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter p5 of test4.
found : @UnknownVal int
required: int
49 errors
diff --git a/checker/jtreg/stubs/issue2147/WithStub.out b/checker/jtreg/stubs/issue2147/WithStub.out
index f9e01800442..bb3dd68ac92 100644
--- a/checker/jtreg/stubs/issue2147/WithStub.out
+++ b/checker/jtreg/stubs/issue2147/WithStub.out
@@ -1,4 +1,4 @@
-EnumStubTest.java:16:31: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+EnumStubTest.java:16:31: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter sEnum of requireEnum.
found : @Tainted SampleEnum
required: @Untainted SampleEnum
1 error
diff --git a/checker/jtreg/stubs/issue2147/WithoutStub.out b/checker/jtreg/stubs/issue2147/WithoutStub.out
index d543064e481..2f01ee07da0 100644
--- a/checker/jtreg/stubs/issue2147/WithoutStub.out
+++ b/checker/jtreg/stubs/issue2147/WithoutStub.out
@@ -1,7 +1,7 @@
-EnumStubTest.java:15:31: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+EnumStubTest.java:15:31: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter sEnum of requireEnum.
found : @Tainted SampleEnum
required: @Untainted SampleEnum
-EnumStubTest.java:16:31: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+EnumStubTest.java:16:31: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter sEnum of requireEnum.
found : @Tainted SampleEnum
required: @Untainted SampleEnum
2 errors
diff --git a/checker/jtreg/tainting/NewClass.out b/checker/jtreg/tainting/NewClass.out
index b589c23b8ae..360dc13cf8f 100644
--- a/checker/jtreg/tainting/NewClass.out
+++ b/checker/jtreg/tainting/NewClass.out
@@ -1,4 +1,4 @@
-NewClass.java:18:49: compiler.err.proc.messager: [argument.type.incompatible] incompatible types in argument.
+NewClass.java:18:49: compiler.err.proc.messager: [argument.type.incompatible] incompatible argument for parameter o of get.
found : @Tainted Object
required: @Untainted Object
1 error
diff --git a/checker/src/main/java/org/checkerframework/checker/formatter/FormatUtil.java b/checker/src/main/java/org/checkerframework/checker/formatter/FormatUtil.java
index 0205c852ef6..2185c4fa90a 100644
--- a/checker/src/main/java/org/checkerframework/checker/formatter/FormatUtil.java
+++ b/checker/src/main/java/org/checkerframework/checker/formatter/FormatUtil.java
@@ -10,22 +10,48 @@
import java.util.regex.Pattern;
import org.checkerframework.checker.formatter.qual.ConversionCategory;
import org.checkerframework.checker.formatter.qual.ReturnsFormat;
+import org.checkerframework.checker.regex.qual.Regex;
+import org.checkerframework.framework.qual.AnnotatedFor;
/** This class provides a collection of utilities to ease working with format strings. */
+@AnnotatedFor("nullness")
public class FormatUtil {
+
+ /**
+ * A representation of a format specifier, which is represented by "%..." in the format string.
+ * Indicates how to convert a value into a string.
+ */
private static class Conversion {
+ /** The index in the argument list. */
private final int index;
+ /** The conversion category. */
private final ConversionCategory cath;
+ /**
+ * Construct a new Conversion.
+ *
+ * @param index the index in the argument list
+ * @param c the conversion character
+ */
public Conversion(char c, int index) {
this.index = index;
this.cath = ConversionCategory.fromConversionChar(c);
}
+ /**
+ * Returns the index in the argument list.
+ *
+ * @return the index in the argument list
+ */
int index() {
return index;
}
+ /**
+ * Returns the conversion category.
+ *
+ * @return the conversion category
+ */
ConversionCategory category() {
return cath;
}
@@ -35,8 +61,14 @@ ConversionCategory category() {
* Returns if the format string is satisfiable, and if the format's parameters match the passed
* {@link ConversionCategory}s. Otherwise an {@link Error} is thrown.
*
- *
TODO introduce more such functions, see RegexUtil for examples
+ * @param format a format string
+ * @param cc an array of conversion categories
+ * @return the {@code format} argument
+ * @throws IllegalFormatException if the format string is incompatible with the conversion
+ * categories
*/
+ // TODO introduce more such functions, see RegexUtil for examples
+ @SuppressWarnings("nullness:argument.type.incompatible") // https://tinyurl.com/cfissue/3449
@ReturnsFormat
public static String asFormat(String format, ConversionCategory... cc)
throws IllegalFormatException {
@@ -54,9 +86,19 @@ public static String asFormat(String format, ConversionCategory... cc)
return format;
}
- /** Throws an exception if the format is not syntactically valid. */
+ /**
+ * Throws an exception if the format is not syntactically valid.
+ *
+ * @param format a format string
+ * @throws IllegalFormatException if the format string is invalid
+ */
+ @SuppressWarnings("nullness:argument.type.incompatible") // https://tinyurl.com/cfissue/3449
public static void tryFormatSatisfiability(String format) throws IllegalFormatException {
- @SuppressWarnings("unused")
+ @SuppressWarnings({
+ "unused", // called for side effect, to see if it throws an exception
+ "nullness:argument.type.incompatible" // it's not documented, but String.format permits
+ // a null array, which it treats as matching any format string
+ })
String unused = String.format(format, (Object[]) null);
}
@@ -90,33 +132,69 @@ public static ConversionCategory[] formatParameterCategories(String format)
break;
}
maxindex = Math.max(maxindex, last);
+ Integer lastKey = last;
conv.put(
last,
ConversionCategory.intersect(
- conv.containsKey(last) ? conv.get(last) : ConversionCategory.UNUSED,
+ conv.containsKey(lastKey)
+ ? conv.get(lastKey)
+ : ConversionCategory.UNUSED,
c.category()));
}
ConversionCategory[] res = new ConversionCategory[maxindex + 1];
for (int i = 0; i <= maxindex; ++i) {
- res[i] = conv.containsKey(i) ? conv.get(i) : ConversionCategory.UNUSED;
+ Integer key = i; // autoboxing prevents recognizing that containsKey => get() != null
+ res[i] = conv.containsKey(key) ? conv.get(key) : ConversionCategory.UNUSED;
}
return res;
}
- // %[argument_index$][flags][width][.precision][t]conversion
- private static final String formatSpecifier =
+ /**
+ * A regex that matches a format specifier. Its syntax is specified in the See {@code
+ * Formatter} documentation.
+ *
+ *
+ *
+ * For dates and times, the [t] is required and precision must not be provided. For types other
+ * than dates and times, the [t] must not be provided.
+ */
+ private static final @Regex(6) String formatSpecifier =
"%(\\d+\\$)?([-#+ 0,(\\<]*)?(\\d+)?(\\.\\d+)?([tT])?([a-zA-Z%])";
+ /** The capturing group for the optional {@code t} character. */
+ private static final int formatSpecifierT = 5;
+ /**
+ * The capturing group for the last character in a format specifier, which is the conversion
+ * character unless the {@code t} character was given.
+ */
+ private static final int formatSpecifierConversion = 6;
- private static Pattern fsPattern = Pattern.compile(formatSpecifier);
+ /**
+ * A Pattern that matches a format specifier.
+ *
+ * @see #formatSpecifier
+ */
+ private static @Regex(6) Pattern fsPattern = Pattern.compile(formatSpecifier);
+ /**
+ * Return the index, in the argument list, of the value that will be formatted by the matched
+ * format specifier.
+ *
+ * @param m a matcher that matches a format specifier
+ * @return the index of the argument to format
+ */
private static int indexFromFormat(Matcher m) {
int index;
String s = m.group(1);
if (s != null) { // explicit index
index = Integer.parseInt(s.substring(0, s.length() - 1));
} else {
- if (m.group(2) != null && m.group(2).contains(String.valueOf('<'))) {
+ String group2 = m.group(2); // not @Deterministic, so extract into local var
+ if (group2 != null && group2.contains(String.valueOf('<'))) {
index = -1; // relative index
} else {
index = 0; // ordinary index
@@ -125,18 +203,49 @@ private static int indexFromFormat(Matcher m) {
return index;
}
- private static char conversionCharFromFormat(Matcher m) {
- String dt = m.group(5);
- if (dt == null) {
- return m.group(6).charAt(0);
+ /**
+ * Returns the conversion character from a format specifier..
+ *
+ * @param m a matcher that matches a format specifier
+ * @return the conversion character from the format specifier
+ */
+ @SuppressWarnings(
+ "nullness:dereference.of.nullable") // group formatSpecifierConversion always exists
+ private static char conversionCharFromFormat(@Regex(6) Matcher m) {
+ String tGroup = m.group(formatSpecifierT);
+ if (tGroup != null) {
+ return tGroup.charAt(0); // This is the letter "t" or "T".
} else {
- return dt.charAt(0);
+ return m.group(formatSpecifierConversion).charAt(0);
}
}
+ /**
+ * Return the conversion character that is in the given format specifier.
+ *
+ * @param formatSpecifier a format
+ * specifier
+ * @return the conversion character that is in the given format specifier
+ * @deprecated This method is public only for testing. Use {@link
+ * #conversionCharFromFormat(Matcher)}.
+ */
+ @Deprecated // used only for testing. Use conversionCharFromFormat(Matcher).
+ public static char conversionCharFromFormat(String formatSpecifier) {
+ Matcher m = fsPattern.matcher(formatSpecifier);
+ assert m.find();
+ return conversionCharFromFormat(m);
+ }
+
+ /**
+ * Parse the given format string, return information about its format specifiers.
+ *
+ * @param format a format string
+ * @return the list of Conversions from the format specifiers in the format string
+ */
private static Conversion[] parse(String format) {
ArrayList cs = new ArrayList<>();
- Matcher m = fsPattern.matcher(format);
+ @Regex(7) Matcher m = fsPattern.matcher(format);
while (m.find()) {
char c = conversionCharFromFormat(m);
switch (c) {
@@ -194,7 +303,9 @@ public static class IllegalFormatConversionCategoryException
public IllegalFormatConversionCategoryException(
ConversionCategory expected, ConversionCategory found) {
super(
- expected.chars.length() == 0 ? '-' : expected.chars.charAt(0),
+ expected.chars == null || expected.chars.length() == 0
+ ? '-'
+ : expected.chars.charAt(0),
found.types == null ? Object.class : found.types[0]);
this.expected = expected;
this.found = found;
diff --git a/checker/src/main/java/org/checkerframework/checker/formatter/FormatterTreeUtil.java b/checker/src/main/java/org/checkerframework/checker/formatter/FormatterTreeUtil.java
index fe6b1da3084..5bd7937deb8 100644
--- a/checker/src/main/java/org/checkerframework/checker/formatter/FormatterTreeUtil.java
+++ b/checker/src/main/java/org/checkerframework/checker/formatter/FormatterTreeUtil.java
@@ -351,6 +351,8 @@ public Boolean visitNull(NullType t, Class p) {
}
}
+ // The failure() method is required so that FormatterTransfer, which has no access to the
+ // FormatterChecker, can report errors.
/**
* Reports an error.
*
diff --git a/checker/src/main/java/org/checkerframework/checker/formatter/FormatterVisitor.java b/checker/src/main/java/org/checkerframework/checker/formatter/FormatterVisitor.java
index 47d31c067b5..01d6b478c4a 100644
--- a/checker/src/main/java/org/checkerframework/checker/formatter/FormatterVisitor.java
+++ b/checker/src/main/java/org/checkerframework/checker/formatter/FormatterVisitor.java
@@ -9,6 +9,7 @@
import java.util.List;
import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.element.ExecutableElement;
+import javax.lang.model.element.Name;
import javax.lang.model.element.VariableElement;
import javax.lang.model.type.TypeMirror;
import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey;
@@ -88,9 +89,14 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void p) {
default:
if (!fc.isValidParameter(formatCat, paramType)) {
// II.3
+ ExecutableElement method =
+ TreeUtils.elementFromUse(node);
+ Name methodName = method.getSimpleName();
tu.failure(
param,
"argument.type.incompatible",
+ "", // parameter name is not useful
+ methodName,
paramType,
formatCat);
}
@@ -122,10 +128,15 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void p) {
}
/**
- * Returns true if fc is within a method m annotated as {@code @FormatMethod}, and fc's
+ * Returns true if {@code fc} is within a method m annotated as {@code @FormatMethod}, and fc's
* arguments are m's formal parameters. In other words, fc forwards m's arguments to another
* format method.
+ *
+ * @param fc an invocation of a format method
+ * @return true if {@code fc} is a call to a format method that forwards its containing methods'
+ * arguments
*/
+ @SuppressWarnings("interning:not.interned") // comparisons of Name objects
private boolean isWrappedFormatCall(FormatCall fc) {
MethodTree enclosingMethod = TreeUtils.enclosingMethod(atypeFactory.getPath(fc.node));
@@ -171,8 +182,9 @@ protected void commonAssignmentCheck(
AnnotatedTypeMirror varType,
AnnotatedTypeMirror valueType,
Tree valueTree,
- @CompilerMessageKey String errorKey) {
- super.commonAssignmentCheck(varType, valueType, valueTree, errorKey);
+ @CompilerMessageKey String errorKey,
+ Object... extraArgs) {
+ super.commonAssignmentCheck(varType, valueType, valueTree, errorKey, extraArgs);
AnnotationMirror rhs = valueType.getAnnotationInHierarchy(atypeFactory.UNKNOWNFORMAT);
AnnotationMirror lhs = varType.getAnnotationInHierarchy(atypeFactory.UNKNOWNFORMAT);
diff --git a/checker/src/main/java/org/checkerframework/checker/formatter/qual/ConversionCategory.java b/checker/src/main/java/org/checkerframework/checker/formatter/qual/ConversionCategory.java
index 5c0871a6e02..e64c5f3a801 100644
--- a/checker/src/main/java/org/checkerframework/checker/formatter/qual/ConversionCategory.java
+++ b/checker/src/main/java/org/checkerframework/checker/formatter/qual/ConversionCategory.java
@@ -7,7 +7,9 @@
import java.util.Date;
import java.util.HashSet;
import java.util.Set;
+import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.dataflow.qual.Pure;
+import org.checkerframework.framework.qual.AnnotatedFor;
/**
* Elements of this enumeration are used in a {@link Format Format} annotation to indicate the valid
@@ -28,6 +30,7 @@
* @see Format
* @checker_framework.manual #formatter-checker Format String Checker
*/
+@AnnotatedFor("nullness")
public enum ConversionCategory {
/** Use if the parameter can be of any type. Applicable for conversions b, B, h, H, s, S. */
GENERAL(null /* everything */, "bBhHsS"),
@@ -108,29 +111,29 @@ public enum ConversionCategory {
UNUSED(null /* everything */, null);
/** Create a new conversion category. */
- ConversionCategory(Class>[] types, String chars) {
+ ConversionCategory(Class> @Nullable [] types, @Nullable String chars) {
this.types = types;
this.chars = chars;
}
/** The format types. */
@SuppressWarnings("ImmutableEnumChecker") // TODO: clean this up!
- public final Class>[] types;
+ public final Class> @Nullable [] types;
/** The format characters. */
- public final String chars;
+ public final @Nullable String chars;
/**
- * Use this function to get the category associated with a conversion character. For example:
+ * Converts a conversion character to a category. For example:
*
- *
+ * @param c a conversion character
+ * @return the category for the given conversion character
*/
+ @SuppressWarnings("nullness:dereference.of.nullable") // `chars` field is non-null for these
public static ConversionCategory fromConversionChar(char c) {
for (ConversionCategory v : new ConversionCategory[] {GENERAL, CHAR, INT, FLOAT, TIME}) {
if (v.chars.contains(String.valueOf(c))) {
@@ -177,14 +180,23 @@ public static ConversionCategory intersect(ConversionCategory a, ConversionCateg
return a;
}
- Set> as = arrayToSet(a.types);
- Set> bs = arrayToSet(b.types);
+ @SuppressWarnings(
+ "nullness:argument.type.incompatible") // `types` field is null only for UNUSED and
+ // GENERAL
+ Set> as = arrayToSet(a.types);
+ @SuppressWarnings(
+ "nullness:argument.type.incompatible") // `types` field is null only for UNUSED and
+ // GENERAL
+ Set> bs = arrayToSet(b.types);
as.retainAll(bs); // intersection
for (ConversionCategory v :
new ConversionCategory[] {
CHAR, INT, FLOAT, TIME, CHAR_AND_INT, INT_AND_TIME, NULL
}) {
- Set> vs = arrayToSet(v.types);
+ @SuppressWarnings(
+ "nullness:argument.type.incompatible") // `types` field is null only for UNUSED
+ // and GENERAL
+ Set> vs = arrayToSet(v.types);
if (vs.equals(as)) {
return v;
}
@@ -221,14 +233,23 @@ public static ConversionCategory union(ConversionCategory a, ConversionCategory
return INT;
}
- Set> as = arrayToSet(a.types);
- Set> bs = arrayToSet(b.types);
+ @SuppressWarnings(
+ "nullness:argument.type.incompatible") // `types` field is null only for UNUSED and
+ // GENERAL
+ Set> as = arrayToSet(a.types);
+ @SuppressWarnings(
+ "nullness:argument.type.incompatible") // `types` field is null only for UNUSED and
+ // GENERAL
+ Set> bs = arrayToSet(b.types);
as.addAll(bs); // union
for (ConversionCategory v :
new ConversionCategory[] {
NULL, CHAR_AND_INT, INT_AND_TIME, CHAR, INT, FLOAT, TIME
}) {
- Set> vs = arrayToSet(v.types);
+ @SuppressWarnings(
+ "nullness:argument.type.incompatible") // `types` field is null only for UNUSED
+ // and GENERAL
+ Set> vs = arrayToSet(v.types);
if (vs.equals(as)) {
return v;
}
@@ -266,20 +287,25 @@ private String className(Class> cls) {
}
/** Returns a pretty printed {@link ConversionCategory}. */
+ @SuppressWarnings(
+ "nullness:iterating.over.nullable") // `types` field is null only for UNUSED and
+ // GENERAL
@Pure
@Override
public String toString() {
StringBuilder sb = new StringBuilder(this.name());
- sb.append(" conversion category (one of: ");
- boolean first = true;
- for (Class extends Object> cls : this.types) {
- if (!first) {
- sb.append(", ");
+ if (this != UNUSED && this != GENERAL) {
+ sb.append(" conversion category (one of: ");
+ boolean first = true;
+ for (Class> cls : this.types) {
+ if (!first) {
+ sb.append(", ");
+ }
+ sb.append(className(cls));
+ first = false;
}
- sb.append(className(cls));
- first = false;
+ sb.append(")");
}
- sb.append(")");
return sb.toString();
}
}
diff --git a/checker/src/main/java/org/checkerframework/checker/guieffect/GuiEffectVisitor.java b/checker/src/main/java/org/checkerframework/checker/guieffect/GuiEffectVisitor.java
index 0da2b746852..3e1feb0e793 100644
--- a/checker/src/main/java/org/checkerframework/checker/guieffect/GuiEffectVisitor.java
+++ b/checker/src/main/java/org/checkerframework/checker/guieffect/GuiEffectVisitor.java
@@ -18,7 +18,9 @@
import java.util.Set;
import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.element.ExecutableElement;
+import javax.lang.model.element.Name;
import javax.lang.model.element.TypeElement;
+import javax.lang.model.element.VariableElement;
import javax.lang.model.type.DeclaredType;
import org.checkerframework.checker.guieffect.qual.AlwaysSafe;
import org.checkerframework.checker.guieffect.qual.PolyUI;
@@ -210,6 +212,7 @@ public boolean isValidUse(
}
@Override
+ @SuppressWarnings("interning:not.interned") // comparing AST nodes
public Void visitLambdaExpression(LambdaExpressionTree node, Void p) {
Void v = super.visitLambdaExpression(node, p);
// If this is a lambda inferred to be @UI, scan up the path and re-check any assignments
@@ -435,6 +438,7 @@ public Void visitMethod(MethodTree node, Void p) {
}
@Override
+ @SuppressWarnings("interning:not.interned") // comparing AST nodes
public Void visitNewClass(NewClassTree node, Void p) {
Void v = super.visitNewClass(node, p);
// If this is an anonymous inner class inferred to be @UI, scan up the path and re-check any
@@ -453,11 +457,13 @@ public Void visitNewClass(NewClassTree node, Void p) {
/**
* This method is called to traverse the path back up from any anonymous inner class or lambda
- * which has been inferred to be UI affecting and re-run {@link #commonAssignmentCheck(Tree,
- * ExpressionTree, String)} as needed on places where the class declaration or lambda expression
- * are being assigned to a variable, passed as a parameter or returned from a method. This is
- * necessary because the normal visitor traversal only checks assignments on the way down the
- * AST, before inference has had a chance to run.
+ * which has been inferred to be UI affecting and re-run {@code commonAssignmentCheck} as needed
+ * on places where the class declaration or lambda expression are being assigned to a variable,
+ * passed as a parameter or returned from a method. This is necessary because the normal visitor
+ * traversal only checks assignments on the way down the AST, before inference has had a chance
+ * to run.
+ *
+ * @param path the path to traverse up from a UI-affecting class
*/
private void scanUp(TreePath path) {
Tree tree = path.getLeaf();
@@ -483,6 +489,9 @@ private void scanUp(TreePath path) {
List extends ExpressionTree> args = invocationTree.getArguments();
ParameterizedExecutableType mType = atypeFactory.methodFromUse(invocationTree);
AnnotatedExecutableType invokedMethod = mType.executableType;
+ ExecutableElement method = invokedMethod.getElement();
+ Name methodName = method.getSimpleName();
+ List extends VariableElement> methodParams = method.getParameters();
List argsTypes =
AnnotatedTypes.expandVarArgs(
atypeFactory, invokedMethod, invocationTree.getArguments());
@@ -493,7 +502,9 @@ private void scanUp(TreePath path) {
argsTypes.get(i),
atypeFactory.getAnnotatedType(args.get(i)),
args.get(i),
- "argument.type.incompatible");
+ "argument.type.incompatible",
+ methodParams.get(i),
+ methodName);
}
}
break;
diff --git a/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatUtil.java b/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatUtil.java
index 05d80036c81..5e537931178 100644
--- a/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatUtil.java
+++ b/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatUtil.java
@@ -14,12 +14,19 @@
import org.checkerframework.checker.i18nformatter.qual.I18nChecksFormat;
import org.checkerframework.checker.i18nformatter.qual.I18nConversionCategory;
import org.checkerframework.checker.i18nformatter.qual.I18nValidFormat;
+import org.checkerframework.checker.interning.qual.InternedDistinct;
+import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
+import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.nullness.qual.RequiresNonNull;
+import org.checkerframework.framework.qual.AnnotatedFor;
/**
* This class provides a collection of utilities to ease working with i18n format strings.
*
* @checker_framework.manual #i18n-formatter-checker Internationalization Format String Checker
*/
+@AnnotatedFor("nullness")
public class I18nFormatUtil {
/**
@@ -27,6 +34,9 @@ public class I18nFormatUtil {
*
* @param format the format string to parse
*/
+ @SuppressWarnings(
+ "nullness:argument.type.incompatible") // It's not documented, but passing null as the
+ // argument array is supported.
public static void tryFormatSatisfiability(String format) throws IllegalFormatException {
MessageFormat.format(format, (Object[]) null);
}
@@ -47,19 +57,22 @@ public static I18nConversionCategory[] formatParameterCategories(String format)
for (I18nConversion c : cs) {
int index = c.index;
+ Integer indexKey = index;
conv.put(
- index,
+ indexKey,
I18nConversionCategory.intersect(
c.category,
- conv.containsKey(index)
- ? conv.get(index)
+ conv.containsKey(indexKey)
+ ? conv.get(indexKey)
: I18nConversionCategory.UNUSED));
maxIndex = Math.max(maxIndex, index);
}
I18nConversionCategory[] res = new I18nConversionCategory[maxIndex + 1];
for (int i = 0; i <= maxIndex; i++) {
- res[i] = conv.containsKey(i) ? conv.get(i) : I18nConversionCategory.UNUSED;
+ Integer indexKey = i;
+ res[i] =
+ conv.containsKey(indexKey) ? conv.get(indexKey) : I18nConversionCategory.UNUSED;
}
return res;
}
@@ -117,18 +130,22 @@ private static class MessageFormatParser {
public static int maxOffset;
- /** The locale to use for formatting numbers and dates. */
- private static Locale locale;
+ /** The locale to use for formatting numbers and dates. Is set in {@link #parse}. */
+ private static @MonotonicNonNull Locale locale;
- /** An array of formatters, which are used to format the arguments. */
- private static List categories;
+ /**
+ * An array of formatters, which are used to format the arguments. Is set in {@link #parse}.
+ */
+ private static @MonotonicNonNull List categories;
/**
* The argument numbers corresponding to each formatter. (The formatters are stored in the
* order they occur in the pattern, not in the order in which the arguments are specified.)
+ * Is set in {@link #parse}.
*/
- private static List argumentIndices;
+ private static @MonotonicNonNull List argumentIndices;
+ // I think this means the number of format specifiers in the format string.
/** The number of subformats. */
private static int numFormat;
@@ -161,6 +178,7 @@ private static class MessageFormatParser {
"", "short", "medium", "long", "full"
};
+ @EnsuresNonNull({"categories", "argumentIndices", "locale"})
public static I18nConversion[] parse(String pattern) {
MessageFormatParser.categories = new ArrayList<>();
MessageFormatParser.argumentIndices = new ArrayList<>();
@@ -174,8 +192,10 @@ public static I18nConversion[] parse(String pattern) {
return ret;
}
+ @SuppressWarnings("nullness:dereference.of.nullable") // complex rules for segments[i]
+ @RequiresNonNull({"argumentIndices", "categories", "locale"})
private static void applyPattern(String pattern) {
- StringBuilder[] segments = new StringBuilder[4];
+ @Nullable StringBuilder[] segments = new StringBuilder[4];
// Allocate only segments[SEG_RAW] here. The rest are
// allocated on demand.
segments[SEG_RAW] = new StringBuilder();
@@ -262,7 +282,8 @@ private static void applyPattern(String pattern) {
}
/** Side-effects {@code categories} field, adding to it an I18nConversionCategory. */
- private static void makeFormat(int offsetNumber, StringBuilder[] textSegments) {
+ @RequiresNonNull({"argumentIndices", "categories", "locale"})
+ private static void makeFormat(int offsetNumber, @Nullable StringBuilder[] textSegments) {
String[] segments = new String[textSegments.length];
for (int i = 0; i < textSegments.length; i++) {
StringBuilder oneseg = textSegments[i];
@@ -372,7 +393,8 @@ private static final int findKeyword(String s, String[] list) {
}
// Try trimmed lowercase.
- String ls = s.trim().toLowerCase(Locale.ROOT);
+ @SuppressWarnings("interning:assignment.type.incompatible") // test if value changed
+ @InternedDistinct String ls = s.trim().toLowerCase(Locale.ROOT);
if (ls != s) { // Don't loop if the string trim().toLowerCase returned the same object.
for (int i = 0; i < list.length; ++i) {
if (ls.equals(list[i])) {
diff --git a/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterTreeUtil.java b/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterTreeUtil.java
index 38d156f455c..f11bbcdf073 100644
--- a/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterTreeUtil.java
+++ b/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterTreeUtil.java
@@ -236,14 +236,19 @@ public I18nFormatCall createFormatForCall(
/**
* Represents a format method invocation in the syntax tree.
*
- *
An I18nFormatCall instance can only be instantiated by createFormatForCall method
+ *
An I18nFormatCall instance can only be instantiated by the createFormatForCall method.
*/
public class I18nFormatCall {
- private final ExpressionTree tree;
+ /** The AST node for the call. */
+ private final MethodInvocationTree tree;
+ /** The format string argument. */
private ExpressionTree formatArg;
+ /** The type factory. */
private final AnnotatedTypeFactory atypeFactory;
+ /** The arguments to the format string. */
private List extends ExpressionTree> args;
+ /** Extra description for error messages. */
private String invalidMessage;
private AnnotatedTypeMirror formatAnno;
@@ -261,6 +266,15 @@ public I18nFormatCall(
initialCheck(theargs, method, node, methodAnno);
}
+ /**
+ * Returns the AST node for the call.
+ *
+ * @return the AST node for the call
+ */
+ public MethodInvocationTree getTree() {
+ return tree;
+ }
+
@Override
public String toString() {
return this.tree.toString();
@@ -420,7 +434,7 @@ public InvocationType visitNull(NullType t, Class p) {
}
ExpressionTree loc;
- loc = ((MethodInvocationTree) tree).getMethodSelect();
+ loc = tree.getMethodSelect();
if (type != InvocationType.VARARG && !args.isEmpty()) {
loc = args.get(0);
}
diff --git a/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterVisitor.java b/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterVisitor.java
index 125cfb266b8..6ab4583691a 100644
--- a/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterVisitor.java
+++ b/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterVisitor.java
@@ -3,6 +3,8 @@
import com.sun.source.tree.MethodInvocationTree;
import com.sun.source.tree.Tree;
import javax.lang.model.element.AnnotationMirror;
+import javax.lang.model.element.ExecutableElement;
+import javax.lang.model.element.Name;
import javax.lang.model.type.TypeMirror;
import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey;
import org.checkerframework.checker.formatter.FormatterTreeUtil.InvocationType;
@@ -16,6 +18,7 @@
import org.checkerframework.dataflow.cfg.node.MethodInvocationNode;
import org.checkerframework.framework.type.AnnotatedTypeMirror;
import org.checkerframework.javacutil.AnnotationUtils;
+import org.checkerframework.javacutil.TreeUtils;
/**
* Whenever a method with {@link I18nFormatFor} annotation is invoked, it will perform the format
@@ -47,8 +50,6 @@ private void checkInvocationFormatFor(I18nFormatCall fc) {
I18nFormatterTreeUtil tu = atypeFactory.treeUtil;
Result type = fc.getFormatType();
- Result invc;
- I18nConversionCategory[] formatCats;
switch (type.value()) {
case I18NINVALID:
tu.failure(type, "i18nformat.string.invalid", fc.getInvalidError());
@@ -60,8 +61,8 @@ private void checkInvocationFormatFor(I18nFormatCall fc) {
}
break;
case I18NFORMAT:
- invc = fc.getInvocationType();
- formatCats = fc.getFormatCategories();
+ Result invc = fc.getInvocationType();
+ I18nConversionCategory[] formatCats = fc.getFormatCategories();
switch (invc.value()) {
case VARARG:
Result[] paramTypes = fc.getParamTypes();
@@ -89,9 +90,14 @@ private void checkInvocationFormatFor(I18nFormatCall fc) {
break;
default:
if (!fc.isValidParameter(formatCat, paramType)) {
+ ExecutableElement method =
+ TreeUtils.elementFromUse(fc.getTree());
+ Name methodName = method.getSimpleName();
tu.failure(
param,
"argument.type.incompatible",
+ "", // parameter name is not useful
+ methodName,
paramType,
formatCat);
}
@@ -122,7 +128,8 @@ protected void commonAssignmentCheck(
AnnotatedTypeMirror varType,
AnnotatedTypeMirror valueType,
Tree valueTree,
- @CompilerMessageKey String errorKey) {
+ @CompilerMessageKey String errorKey,
+ Object... extraArgs) {
AnnotationMirror rhs = valueType.getAnnotationInHierarchy(atypeFactory.I18NUNKNOWNFORMAT);
AnnotationMirror lhs = varType.getAnnotationInHierarchy(atypeFactory.I18NUNKNOWNFORMAT);
@@ -163,6 +170,6 @@ protected void commonAssignmentCheck(
// issued for a given line of code will take precedence over the
// assignment.type.incompatible
// issued by super.commonAssignmentCheck.
- super.commonAssignmentCheck(varType, valueType, valueTree, errorKey);
+ super.commonAssignmentCheck(varType, valueType, valueTree, errorKey, extraArgs);
}
}
diff --git a/checker/src/main/java/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java b/checker/src/main/java/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java
index d1d816917c9..6b697978c33 100644
--- a/checker/src/main/java/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java
+++ b/checker/src/main/java/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java
@@ -4,25 +4,23 @@
import java.util.Date;
import java.util.HashSet;
import java.util.Set;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.framework.qual.AnnotatedFor;
/**
* Elements of this enumeration are used in a {@link I18nFormat} annotation to indicate the valid
* types that may be passed as a format parameter. For example:
*
- *
- *
* The annotation indicates that the format string requires any object as the first parameter
* ({@link I18nConversionCategory#GENERAL}) and a number as the second parameter ({@link
* I18nConversionCategory#NUMBER}).
*
* @checker_framework.manual #i18n-formatter-checker Internationalization Format String Checker
*/
+@AnnotatedFor("nullness")
public enum I18nConversionCategory {
/**
@@ -54,12 +52,12 @@ public enum I18nConversionCategory {
NUMBER(new Class>[] {Number.class}, new String[] {"number", "choice"});
@SuppressWarnings("ImmutableEnumChecker") // TODO: clean this up!
- public final Class extends Object>[] types;
+ public final Class> @Nullable [] types;
@SuppressWarnings("ImmutableEnumChecker") // TODO: clean this up!
- public final String[] strings;
+ public final String @Nullable [] strings;
- I18nConversionCategory(Class extends Object>[] types, String[] strings) {
+ I18nConversionCategory(Class> @Nullable [] types, String @Nullable [] strings) {
this.types = types;
this.strings = strings;
}
@@ -76,6 +74,8 @@ public enum I18nConversionCategory {
*
* @return the I18nConversionCategory associated with the given string
*/
+ @SuppressWarnings(
+ "nullness:iterating.over.nullable") // in namedCategories, `strings` field is non-null
public static I18nConversionCategory stringToI18nConversionCategory(String string) {
string = string.toLowerCase();
for (I18nConversionCategory v : namedCategories) {
@@ -127,11 +127,20 @@ public static I18nConversionCategory intersect(
return a;
}
- Set> as = arrayToSet(a.types);
- Set> bs = arrayToSet(b.types);
+ @SuppressWarnings(
+ "nullness:argument.type.incompatible") // types field is only null in UNUSED and
+ // GENERAL
+ Set> as = arrayToSet(a.types);
+ @SuppressWarnings(
+ "nullness:argument.type.incompatible") // types field is only null in UNUSED and
+ // GENERAL
+ Set> bs = arrayToSet(b.types);
as.retainAll(bs); // intersection
for (I18nConversionCategory v : new I18nConversionCategory[] {DATE, NUMBER}) {
- Set> vs = arrayToSet(v.types);
+ @SuppressWarnings(
+ "nullness:argument.type.incompatible") // in those values, `types` field is
+ // non-null
+ Set> vs = arrayToSet(v.types);
if (vs.equals(as)) {
return v;
}
@@ -168,7 +177,7 @@ public String toString() {
} else {
sb.append(" conversion category (one of: ");
boolean first = true;
- for (Class extends Object> cls : this.types) {
+ for (Class> cls : this.types) {
if (!first) {
sb.append(", ");
}
diff --git a/checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanVisitor.java b/checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanVisitor.java
index 0d608e56895..a6fd12c3283 100644
--- a/checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanVisitor.java
+++ b/checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanVisitor.java
@@ -24,7 +24,10 @@ public LessThanVisitor(BaseTypeChecker checker) {
@Override
protected void commonAssignmentCheck(
- Tree varTree, ExpressionTree valueTree, @CompilerMessageKey String errorKey) {
+ Tree varTree,
+ ExpressionTree valueTree,
+ @CompilerMessageKey String errorKey,
+ Object... extraArgs) {
// check that when an assignment to a variable declared as @HasSubsequence(a, from, to)
// occurs, from <= to.
@@ -53,7 +56,7 @@ protected void commonAssignmentCheck(
}
}
- super.commonAssignmentCheck(varTree, valueTree, errorKey);
+ super.commonAssignmentCheck(varTree, valueTree, errorKey, extraArgs);
}
@Override
@@ -61,7 +64,8 @@ protected void commonAssignmentCheck(
AnnotatedTypeMirror varType,
AnnotatedTypeMirror valueType,
Tree valueTree,
- @CompilerMessageKey String errorKey) {
+ @CompilerMessageKey String errorKey,
+ Object... extraArgs) {
// If value is less than all expressions in the annotation in varType,
// using the Value Checker, then skip the common assignment check.
// Also skip the check if the only expression is "a + 1" and the valueTree
@@ -98,7 +102,7 @@ protected void commonAssignmentCheck(
return;
}
}
- super.commonAssignmentCheck(varType, valueType, valueTree, errorKey);
+ super.commonAssignmentCheck(varType, valueType, valueTree, errorKey, extraArgs);
}
@Override
diff --git a/checker/src/main/java/org/checkerframework/checker/index/lowerbound/LowerBoundVisitor.java b/checker/src/main/java/org/checkerframework/checker/index/lowerbound/LowerBoundVisitor.java
index df3e84591d0..3cecd0ad5f6 100644
--- a/checker/src/main/java/org/checkerframework/checker/index/lowerbound/LowerBoundVisitor.java
+++ b/checker/src/main/java/org/checkerframework/checker/index/lowerbound/LowerBoundVisitor.java
@@ -62,7 +62,10 @@ public Void visitNewArray(NewArrayTree tree, Void type) {
@Override
protected void commonAssignmentCheck(
- Tree varTree, ExpressionTree valueTree, @CompilerMessageKey String errorKey) {
+ Tree varTree,
+ ExpressionTree valueTree,
+ @CompilerMessageKey String errorKey,
+ Object... extraArgs) {
// check that when an assignment to a variable declared as @HasSubsequence(a, from, to)
// occurs, from is non-negative.
@@ -88,6 +91,6 @@ protected void commonAssignmentCheck(
}
}
- super.commonAssignmentCheck(varTree, valueTree, errorKey);
+ super.commonAssignmentCheck(varTree, valueTree, errorKey, extraArgs);
}
}
diff --git a/checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenVisitor.java b/checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenVisitor.java
index 613c17fd584..fda48689c13 100644
--- a/checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenVisitor.java
+++ b/checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenVisitor.java
@@ -33,7 +33,8 @@ protected void commonAssignmentCheck(
AnnotatedTypeMirror varType,
AnnotatedTypeMirror valueType,
Tree valueTree,
- @CompilerMessageKey String errorKey) {
+ @CompilerMessageKey String errorKey,
+ Object... extraArgs) {
if (IndexUtil.isSequenceType(valueType.getUnderlyingType())
&& TreeUtils.isExpressionTree(valueTree)
// if both annotations are @PolySameLen, there is nothing to do
@@ -57,6 +58,6 @@ protected void commonAssignmentCheck(
valueType.replaceAnnotation(newSameLen);
}
}
- super.commonAssignmentCheck(varType, valueType, valueTree, errorKey);
+ super.commonAssignmentCheck(varType, valueType, valueTree, errorKey, extraArgs);
}
}
diff --git a/checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundVisitor.java b/checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundVisitor.java
index 35b0d8e8126..95141c62b43 100644
--- a/checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundVisitor.java
+++ b/checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundVisitor.java
@@ -190,7 +190,10 @@ private void visitAccess(ExpressionTree indexTree, ExpressionTree arrTree) {
@Override
protected void commonAssignmentCheck(
- Tree varTree, ExpressionTree valueTree, @CompilerMessageKey String errorKey) {
+ Tree varTree,
+ ExpressionTree valueTree,
+ @CompilerMessageKey String errorKey,
+ Object... extraArgs) {
// check that when an assignment to a variable b declared as @HasSubsequence(a, from, to)
// occurs, to <= a.length, i.e. to is @LTEqLengthOf(a).
@@ -237,14 +240,15 @@ protected void commonAssignmentCheck(
}
}
- super.commonAssignmentCheck(varTree, valueTree, errorKey);
+ super.commonAssignmentCheck(varTree, valueTree, errorKey, extraArgs);
}
@Override
protected void commonAssignmentCheck(
AnnotatedTypeMirror varType,
ExpressionTree valueTree,
- @CompilerMessageKey String errorKey) {
+ @CompilerMessageKey String errorKey,
+ Object... extraArgs) {
AnnotatedTypeMirror valueType = atypeFactory.getAnnotatedType(valueTree);
commonAssignmentCheckStartDiagnostic(varType, valueType, valueTree);
if (!relaxedCommonAssignment(varType, valueTree)) {
@@ -253,7 +257,7 @@ protected void commonAssignmentCheck(
varType,
valueType,
valueTree);
- super.commonAssignmentCheck(varType, valueTree, errorKey);
+ super.commonAssignmentCheck(varType, valueTree, errorKey, extraArgs);
} else if (checker.hasOption("showchecks")) {
commonAssignmentCheckEndDiagnostic(
true, "relaxedCommonAssignment", varType, valueType, valueTree);
diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationAnnotatedTypeFactory.java
index 76fcda52282..964d3320d68 100644
--- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationAnnotatedTypeFactory.java
+++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationAnnotatedTypeFactory.java
@@ -3,6 +3,7 @@
import com.sun.source.tree.ClassTree;
import com.sun.source.tree.ExpressionTree;
import com.sun.source.tree.LiteralTree;
+import com.sun.source.tree.MemberSelectTree;
import com.sun.source.tree.MethodTree;
import com.sun.source.tree.NewClassTree;
import com.sun.source.tree.Tree;
@@ -427,12 +428,17 @@ public AnnotatedDeclaredType getSelfType(Tree tree) {
}
/**
- * In the first enclosing class, find the top-level member that contains tree. TODO: should we
- * look whether these elements are enclosed within another class that is itself under
- * construction.
+ * In the first enclosing class, find the top-level member that contains {@code path}.
+ *
+ *
TODO: should we look whether these elements are enclosed within another class that is
+ * itself under construction.
*
*
Are there any other type of top level objects?
+ *
+ * @param path the path whose leaf is the target
+ * @return a top-level member containing the leaf of {@code path}
*/
+ @SuppressWarnings("interning:not.interned") // AST node comparison
private Tree findTopLevelClassMemberForTree(TreePath path) {
ClassTree enclosingClass = TreeUtils.enclosingClass(path);
if (enclosingClass != null) {
@@ -737,6 +743,15 @@ public Void visitLiteral(LiteralTree tree, AnnotatedTypeMirror type) {
}
return super.visitLiteral(tree, type);
}
+
+ @Override
+ public Void visitMemberSelect(
+ MemberSelectTree node, AnnotatedTypeMirror annotatedTypeMirror) {
+ if (TreeUtils.isArrayLengthAccess(node)) {
+ annotatedTypeMirror.replaceAnnotation(INITIALIZED);
+ }
+ return super.visitMemberSelect(node, annotatedTypeMirror);
+ }
}
/**
diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.java
index b539d07bb12..d60ac81e296 100644
--- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.java
+++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.java
@@ -13,7 +13,6 @@
import javax.lang.model.type.TypeKind;
import javax.lang.model.type.TypeMirror;
import javax.lang.model.util.ElementFilter;
-import org.checkerframework.dataflow.analysis.ConditionalTransferResult;
import org.checkerframework.dataflow.analysis.FlowExpressions;
import org.checkerframework.dataflow.analysis.FlowExpressions.FieldAccess;
import org.checkerframework.dataflow.analysis.FlowExpressions.Receiver;
@@ -86,9 +85,11 @@ protected boolean isNotFullyInitializedReceiver(MethodTree methodTree) {
/**
* Returns the fields that can safely be considered initialized after the method call {@code
* node}.
+ *
+ * @param node a method call
+ * @return the fields that are initialized after the method call
*/
- protected List initializedFieldsAfterCall(
- MethodInvocationNode node, ConditionalTransferResult transferResult) {
+ protected List initializedFieldsAfterCall(MethodInvocationNode node) {
List result = new ArrayList<>();
MethodInvocationTree tree = node.getTree();
ExecutableElement method = TreeUtils.elementFromUse(tree);
@@ -194,9 +195,7 @@ public TransferResult visitFieldAccess(FieldAccessNode n, TransferInput visitMethodInvocation(
MethodInvocationNode n, TransferInput in) {
TransferResult result = super.visitMethodInvocation(n, in);
- assert result instanceof ConditionalTransferResult;
- List newlyInitializedFields =
- initializedFieldsAfterCall(n, (ConditionalTransferResult) result);
+ List newlyInitializedFields = initializedFieldsAfterCall(n);
if (!newlyInitializedFields.isEmpty()) {
for (VariableElement f : newlyInitializedFields) {
result.getThenStore().addInitializedField(f);
diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java
index 44c370f48fd..fcc5e084794 100644
--- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java
+++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java
@@ -110,7 +110,10 @@ protected void checkThisOrSuperConstructorCall(
@Override
protected void commonAssignmentCheck(
- Tree varTree, ExpressionTree valueExp, @CompilerMessageKey String errorKey) {
+ Tree varTree,
+ ExpressionTree valueExp,
+ @CompilerMessageKey String errorKey,
+ Object... extraArgs) {
// field write of the form x.f = y
if (TreeUtils.isFieldAccess(varTree)) {
// cast is safe: a field access can only be an IdentifierTree or
@@ -141,7 +144,7 @@ protected void commonAssignmentCheck(
}
}
}
- super.commonAssignmentCheck(varTree, valueExp, errorKey);
+ super.commonAssignmentCheck(varTree, valueExp, errorKey, extraArgs);
}
@Override
diff --git a/checker/src/main/java/org/checkerframework/checker/interning/InterningAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/interning/InterningAnnotatedTypeFactory.java
index ffd7f193972..cb2ba0e93be 100644
--- a/checker/src/main/java/org/checkerframework/checker/interning/InterningAnnotatedTypeFactory.java
+++ b/checker/src/main/java/org/checkerframework/checker/interning/InterningAnnotatedTypeFactory.java
@@ -2,6 +2,7 @@
import com.sun.source.tree.BinaryTree;
import com.sun.source.tree.CompoundAssignmentTree;
+import com.sun.source.tree.IdentifierTree;
import com.sun.source.tree.Tree;
import com.sun.source.tree.TypeCastTree;
import com.sun.tools.javac.code.Symbol.MethodSymbol;
@@ -12,8 +13,10 @@
import javax.lang.model.type.DeclaredType;
import javax.lang.model.type.TypeKind;
import javax.lang.model.type.TypeMirror;
+import org.checkerframework.checker.interning.qual.FindDistinct;
import org.checkerframework.checker.interning.qual.InternMethod;
import org.checkerframework.checker.interning.qual.Interned;
+import org.checkerframework.checker.interning.qual.InternedDistinct;
import org.checkerframework.checker.interning.qual.PolyInterned;
import org.checkerframework.checker.interning.qual.UnknownInterned;
import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
@@ -47,11 +50,14 @@
*
is a use of a class declared to be @Interned
*
*
- * This factory extends {@link BaseAnnotatedTypeFactory} and inherits its functionality, including:
- * flow-sensitive qualifier inference, qualifier polymorphism (of {@link PolyInterned}), implicit
- * annotations via {@link org.checkerframework.framework.qual.DefaultFor} on {@link Interned} (to
- * handle cases 1, 2, 4), and user-specified defaults via {@link DefaultQualifier}. Case 5 is
- * handled by the stub library.
+ * This type factory adds {@link InternedDistinct} to formal parameters that have a {@link
+ * FindDistinct} declaration annotation.
+ *
+ *
This factory extends {@link BaseAnnotatedTypeFactory} and inherits its functionality,
+ * including: flow-sensitive qualifier inference, qualifier polymorphism (of {@link PolyInterned}),
+ * implicit annotations via {@link org.checkerframework.framework.qual.DefaultFor} on {@link
+ * Interned} (to handle cases 1, 2, 4), and user-specified defaults via {@link DefaultQualifier}.
+ * Case 5 is handled by the stub library.
*/
public class InterningAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
@@ -59,6 +65,9 @@ public class InterningAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
final AnnotationMirror TOP = AnnotationBuilder.fromClass(elements, UnknownInterned.class);
/** The {@link Interned} annotation. */
final AnnotationMirror INTERNED = AnnotationBuilder.fromClass(elements, Interned.class);
+ /** The {@link InternedDistinct} annotation. */
+ final AnnotationMirror INTERNED_DISTINCT =
+ AnnotationBuilder.fromClass(elements, InternedDistinct.class);
/**
* Creates a new {@link InterningAnnotatedTypeFactory} that operates on a particular AST.
@@ -185,6 +194,15 @@ public Void visitTypeCast(TypeCastTree node, AnnotatedTypeMirror type) {
}
return super.visitTypeCast(node, type);
}
+
+ @Override
+ public Void visitIdentifier(IdentifierTree node, AnnotatedTypeMirror type) {
+ Element e = TreeUtils.elementFromTree(node);
+ if (atypeFactory.getDeclAnnotation(e, FindDistinct.class) != null) {
+ type.replaceAnnotation(INTERNED_DISTINCT);
+ }
+ return super.visitIdentifier(node, type);
+ }
}
/** Adds @Interned to enum types. */
diff --git a/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java b/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java
index eb6285e2001..c939ed7e5b0 100644
--- a/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java
+++ b/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java
@@ -24,12 +24,15 @@
import javax.lang.model.element.Element;
import javax.lang.model.element.ElementKind;
import javax.lang.model.element.ExecutableElement;
+import javax.lang.model.element.Name;
import javax.lang.model.element.TypeElement;
import javax.lang.model.type.DeclaredType;
import javax.lang.model.type.TypeKind;
import javax.lang.model.type.TypeMirror;
import javax.lang.model.util.ElementFilter;
import javax.tools.Diagnostic.Kind;
+import org.checkerframework.checker.interning.qual.CompareToMethod;
+import org.checkerframework.checker.interning.qual.EqualsMethod;
import org.checkerframework.checker.interning.qual.InternMethod;
import org.checkerframework.checker.interning.qual.Interned;
import org.checkerframework.checker.interning.qual.InternedDistinct;
@@ -175,25 +178,20 @@ public Void visitBinary(BinaryTree node, Void p) {
return super.visitBinary(node, p);
}
- Element leftElt = null;
- Element rightElt = null;
- if (left instanceof AnnotatedTypeMirror.AnnotatedDeclaredType) {
- leftElt = ((DeclaredType) left.getUnderlyingType()).asElement();
- }
- if (right instanceof AnnotatedTypeMirror.AnnotatedDeclaredType) {
- rightElt = ((DeclaredType) right.getUnderlyingType()).asElement();
- }
-
- // TODO: CODE REVIEW
- // TODO: WOULD IT BE CLEARER TO USE A METHOD usesReferenceEquality(AnnotatedTypeMirror type)
- // TODO: RATHER THAN leftElt.getAnnotation(UsesObjectEquals.class) != null)
- // if neither @Interned or @UsesObjectEquals, report error
+ Element leftElt = TypesUtils.getTypeElement(left.getUnderlyingType());
+ // If neither @Interned or @UsesObjectEquals, report error.
if (!(left.hasEffectiveAnnotation(INTERNED)
- || (leftElt != null && leftElt.getAnnotation(UsesObjectEquals.class) != null))) {
+ || (leftElt != null
+ && atypeFactory.getDeclAnnotation(leftElt, UsesObjectEquals.class)
+ != null))) {
checker.reportError(leftOp, "not.interned", left);
}
+
+ Element rightElt = TypesUtils.getTypeElement(right.getUnderlyingType());
if (!(right.hasEffectiveAnnotation(INTERNED)
- || (rightElt != null && rightElt.getAnnotation(UsesObjectEquals.class) != null))) {
+ || (rightElt != null
+ && atypeFactory.getDeclAnnotation(rightElt, UsesObjectEquals.class)
+ != null))) {
checker.reportError(rightOp, "not.interned", right);
}
return super.visitBinary(node, p);
@@ -219,13 +217,44 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void p) {
return super.visitMethodInvocation(node, p);
}
+ // Ensure that method annotations are not written on methods they don't apply to.
+ @Override
+ public Void visitMethod(MethodTree node, Void p) {
+ ExecutableElement methElt = TreeUtils.elementFromDeclaration(node);
+ boolean hasCompareToMethodAnno =
+ atypeFactory.getDeclAnnotation(methElt, CompareToMethod.class) != null;
+ boolean hasEqualsMethodAnno =
+ atypeFactory.getDeclAnnotation(methElt, EqualsMethod.class) != null;
+ boolean hasInternMethodAnno =
+ atypeFactory.getDeclAnnotation(methElt, InternMethod.class) != null;
+ int params = methElt.getParameters().size();
+ if (hasCompareToMethodAnno && !(params == 1 || params == 2)) {
+ checker.reportError(
+ node,
+ "invalid.method.annotation",
+ "@CompareToMethod",
+ "1 or 2",
+ methElt,
+ params);
+ } else if (hasEqualsMethodAnno && !(params == 1 || params == 2)) {
+ checker.reportError(
+ node, "invalid.method.annotation", "@EqualsMethod", "1 or 2", methElt, params);
+ } else if (hasInternMethodAnno && !(params == 0)) {
+ checker.reportError(
+ node, "invalid.method.annotation", "@InternMethod", "0", methElt, params);
+ }
+
+ return super.visitMethod(node, p);
+ }
+
/**
* Method to implement the @UsesObjectEquals functionality. If a class is annotated
* with @UsesObjectEquals, it must:
*
*
- *
not override .equals(Object)
- *
be a subclass of Object or another class annotated with @UsesObjectEquals
+ *
not override .equals(Object) and be a subclass of a class annotated
+ * with @UsesObjectEquals, or
+ *
override equals(Object) with body "this == arg"
*
*
* If a class is not annotated with @UsesObjectEquals, it must:
@@ -246,20 +275,25 @@ public void processClassTree(ClassTree classTree) {
// If @UsesObjectEquals is present, check to make sure the class does not override equals
// and its supertype is Object or is annotated with @UsesObjectEquals.
if (annotation != null) {
- // Check methods to ensure no .equals
- if (overridesEquals(classTree)) {
- checker.reportError(classTree, "overrides.equals");
- }
- TypeMirror superClass = elt.getSuperclass();
- if (superClass != null
- // The super class of an interface is "none" rather than null.
- && superClass.getKind() == TypeKind.DECLARED) {
- TypeElement superClassElement = TypesUtils.getTypeElement(superClass);
- if (superClassElement != null
- && !ElementUtils.isObject(superClassElement)
- && atypeFactory.getDeclAnnotation(superClassElement, UsesObjectEquals.class)
- == null) {
- checker.reportError(classTree, "superclass.notannotated");
+ MethodTree equalsMethod = equalsImplementation(classTree);
+ if (equalsMethod != null) {
+ if (!isReferenceEqualityImplementation(equalsMethod)) {
+ checker.reportError(classTree, "overrides.equals");
+ }
+ } else {
+ // Does not override equals()
+ TypeMirror superClass = elt.getSuperclass();
+ if (superClass != null
+ // The super class of an interface is "none" rather than null.
+ && superClass.getKind() == TypeKind.DECLARED) {
+ TypeElement superClassElement = TypesUtils.getTypeElement(superClass);
+ if (superClassElement != null
+ && !ElementUtils.isObject(superClassElement)
+ && atypeFactory.getDeclAnnotation(
+ superClassElement, UsesObjectEquals.class)
+ == null) {
+ checker.reportError(classTree, "superclass.notannotated");
+ }
}
}
}
@@ -267,6 +301,41 @@ public void processClassTree(ClassTree classTree) {
super.processClassTree(classTree);
}
+ /**
+ * Returns true if the given equals() method implements reference equality.
+ *
+ * @param equalsMethod an overriding implementation of Object.equals()
+ * @return true if the given equals() method implements reference equality
+ */
+ private boolean isReferenceEqualityImplementation(MethodTree equalsMethod) {
+ BlockTree body = equalsMethod.getBody();
+ List extends StatementTree> bodyStatements = body.getStatements();
+ if (bodyStatements.size() == 1) {
+ StatementTree bodyStatement = bodyStatements.get(0);
+ if (bodyStatement.getKind() == Tree.Kind.RETURN) {
+ ExpressionTree returnExpr =
+ TreeUtils.withoutParens(((ReturnTree) bodyStatement).getExpression());
+ if (returnExpr.getKind() == Tree.Kind.EQUAL_TO) {
+ BinaryTree bt = (BinaryTree) returnExpr;
+ ExpressionTree lhsTree = bt.getLeftOperand();
+ ExpressionTree rhsTree = bt.getRightOperand();
+ if (lhsTree.getKind() == Tree.Kind.IDENTIFIER
+ && rhsTree.getKind() == Tree.Kind.IDENTIFIER) {
+ Name leftName = ((IdentifierTree) lhsTree).getName();
+ Name rightName = ((IdentifierTree) rhsTree).getName();
+ Name paramName = equalsMethod.getParameters().get(0).getName();
+ if ((leftName.contentEquals("this") && rightName.equals(paramName))
+ || (leftName.equals(paramName)
+ && rightName.contentEquals("this"))) {
+ return true;
+ }
+ }
+ }
+ }
+ }
+ return false;
+ }
+
@Override
protected void checkConstructorResult(
AnnotatedExecutableType constructorType, ExecutableElement constructorElement) {
@@ -340,19 +409,24 @@ private boolean checkCreationOfInternedObject(
// Helper methods
// **********************************************************************
- /** Returns true if a class overrides Object.equals. */
- private boolean overridesEquals(ClassTree node) {
+ /**
+ * Returns the method that overrides Object.equals, or null.
+ *
+ * @param node a class
+ * @return the class's implementation of equals, or null
+ */
+ private MethodTree equalsImplementation(ClassTree node) {
List extends Tree> members = node.getMembers();
for (Tree member : members) {
if (member instanceof MethodTree) {
MethodTree mTree = (MethodTree) member;
ExecutableElement enclosing = TreeUtils.elementFromDeclaration(mTree);
if (overrides(enclosing, Object.class, "equals")) {
- return true;
+ return mTree;
}
}
}
- return false;
+ return null;
}
/**
@@ -408,42 +482,51 @@ private boolean suppressInsideComparison(final BinaryTree node) {
return false;
}
- // If we're not directly in an if statement in a method (ignoring
- // parens and blocks), terminate.
- if (!Heuristics.matchParents(getCurrentPath(), Tree.Kind.IF, Tree.Kind.METHOD)) {
- return false;
- }
-
- // Ensure the if statement is the first statement in the method
-
- TreePath parentPath = getCurrentPath().getParentPath();
-
- // Retrieve the enclosing if statement tree and method tree
- Tree tree, ifStatementTree = null;
- MethodTree methodTree = null;
- while ((tree = parentPath.getLeaf()) != null) {
- if (tree.getKind() == Tree.Kind.IF) {
- ifStatementTree = tree;
- } else if (tree.getKind() == Tree.Kind.METHOD) {
- methodTree = (MethodTree) tree;
- break;
+ TreePath path = getCurrentPath();
+ TreePath parentPath = path.getParentPath();
+ Tree parent = parentPath.getLeaf();
+
+ // Ensure the == is in a return or in an if, and that enclosing statement is the first
+ // statement in the method.
+ if (parent.getKind() == Tree.Kind.RETURN) {
+ // ensure the return statement is the first statement in the method
+ if (parentPath.getParentPath().getParentPath().getLeaf().getKind()
+ != Tree.Kind.METHOD) {
+ return false;
}
- parentPath = parentPath.getParentPath();
- }
-
- // The call to Heuristics.matchParents already ensured there is an enclosing if statement
- assert ifStatementTree != null;
- // The call to Heuristics.matchParents already ensured there is an enclosing method
- assert methodTree != null;
-
- StatementTree stmnt = methodTree.getBody().getStatements().get(0);
- // The call to Heuristics.matchParents already ensured the enclosing method has at least one
- // statement (an if statement) in the body
- assert stmnt != null;
-
- if (stmnt != ifStatementTree) {
- return false; // The if statement is not the first statement in the method.
+ // maybe set some variables??
+ } else if (Heuristics.matchParents(getCurrentPath(), Tree.Kind.IF, Tree.Kind.METHOD)) {
+ // Ensure the if statement is the first statement in the method
+
+ // Retrieve the enclosing if statement tree and method tree
+ Tree ifStatementTree = null;
+ MethodTree methodTree = null;
+ // Set ifStatementTree and methodTree
+ {
+ TreePath ppath = parentPath;
+ Tree tree;
+ while ((tree = ppath.getLeaf()) != null) {
+ if (tree.getKind() == Tree.Kind.IF) {
+ ifStatementTree = tree;
+ } else if (tree.getKind() == Tree.Kind.METHOD) {
+ methodTree = (MethodTree) tree;
+ break;
+ }
+ ppath = ppath.getParentPath();
+ }
+ }
+ assert ifStatementTree != null;
+ assert methodTree != null;
+ StatementTree firstStmnt = methodTree.getBody().getStatements().get(0);
+ assert firstStmnt != null;
+ @SuppressWarnings("interning:not.interned") // comparing AST nodes
+ boolean notSameNode = firstStmnt != ifStatementTree;
+ if (notSameNode) {
+ return false; // The if statement is not the first statement in the method.
+ }
+ } else {
+ return false;
}
ExecutableElement enclosingMethod =
@@ -479,9 +562,16 @@ public Boolean visitReturn(ReturnTree tree, Void p) {
}
};
+ boolean hasCompareToMethodAnno =
+ atypeFactory.getDeclAnnotation(enclosingMethod, CompareToMethod.class) != null;
+ boolean hasEqualsMethodAnno =
+ atypeFactory.getDeclAnnotation(enclosingMethod, EqualsMethod.class) != null;
+ int params = enclosingMethod.getParameters().size();
+
// Determine whether or not the "then" statement of the if has a single
// "return 0" statement (for the Comparator.compare heuristic).
- if (overrides(enclosingMethod, Comparator.class, "compare")) {
+ if (overrides(enclosingMethod, Comparator.class, "compare")
+ || (hasCompareToMethodAnno && params == 2)) {
final boolean returnsZero =
new Heuristics.Within(new Heuristics.OfKind(Tree.Kind.IF, matcherIfReturnsZero))
.match(getCurrentPath());
@@ -490,20 +580,27 @@ public Boolean visitReturn(ReturnTree tree, Void p) {
return false;
}
- assert enclosingMethod.getParameters().size() == 2;
+ assert params == 2;
Element p1 = enclosingMethod.getParameters().get(0);
Element p2 = enclosingMethod.getParameters().get(1);
return (p1.equals(lhs) && p2.equals(rhs)) || (p1.equals(rhs) && p2.equals(lhs));
- } else if (overrides(enclosingMethod, Object.class, "equals")) {
- assert enclosingMethod.getParameters().size() == 1;
+ } else if (overrides(enclosingMethod, Object.class, "equals")
+ || (hasEqualsMethodAnno && params == 1)) {
+ assert params == 1;
Element param = enclosingMethod.getParameters().get(0);
Element thisElt = getThis(trees.getScope(getCurrentPath()));
assert thisElt != null;
return (thisElt.equals(lhs) && param.equals(rhs))
|| (thisElt.equals(rhs) && param.equals(lhs));
- } else if (overrides(enclosingMethod, Comparable.class, "compareTo")) {
+ } else if (hasEqualsMethodAnno && params == 2) {
+ Element p1 = enclosingMethod.getParameters().get(0);
+ Element p2 = enclosingMethod.getParameters().get(1);
+ return (p1.equals(lhs) && p2.equals(rhs)) || (p1.equals(rhs) && p2.equals(lhs));
+
+ } else if (overrides(enclosingMethod, Comparable.class, "compareTo")
+ || (hasCompareToMethodAnno && params == 1)) {
final boolean returnsZero =
new Heuristics.Within(new Heuristics.OfKind(Tree.Kind.IF, matcherIfReturnsZero))
@@ -513,13 +610,14 @@ public Boolean visitReturn(ReturnTree tree, Void p) {
return false;
}
- assert enclosingMethod.getParameters().size() == 1;
+ assert params == 1;
Element param = enclosingMethod.getParameters().get(0);
Element thisElt = getThis(trees.getScope(getCurrentPath()));
assert thisElt != null;
return (thisElt.equals(lhs) && param.equals(rhs))
|| (thisElt.equals(rhs) && param.equals(lhs));
}
+
return false;
}
@@ -723,7 +821,10 @@ public Boolean visitBinary(BinaryTree tree, Void p) {
return visit(leftTree, p);
} else {
// a == b || a.compareTo(b) == 0
- ExpressionTree leftTree = tree.getLeftOperand(); // looking for a==b
+ @SuppressWarnings(
+ "interning:assignment.type.incompatible" // AST node comparisons
+ )
+ @InternedDistinct ExpressionTree leftTree = tree.getLeftOperand(); // looking for a==b
ExpressionTree rightTree =
tree.getRightOperand(); // looking for a.compareTo(b) == 0
// or b.compareTo(a) == 0
diff --git a/checker/src/main/java/org/checkerframework/checker/interning/messages.properties b/checker/src/main/java/org/checkerframework/checker/interning/messages.properties
index 72399842895..435cb6541ea 100644
--- a/checker/src/main/java/org/checkerframework/checker/interning/messages.properties
+++ b/checker/src/main/java/org/checkerframework/checker/interning/messages.properties
@@ -5,3 +5,4 @@ overrides.equals=annotated with @UsesObjectEquals but overrides .equals(Object)
superclass.notannotated=superclass must be annotated with @UsesObjectEquals
superclass.annotated=subclasses must also be annotated with @UsesObjectEquals
interned.object.creation=Cannot statically verify that a new object of an @Interned class is @Interned
+invalid.method.annotation=%s applies to a method with %s formal parameters; %s has %d
diff --git a/checker/src/main/java/org/checkerframework/checker/interning/qual/CompareToMethod.java b/checker/src/main/java/org/checkerframework/checker/interning/qual/CompareToMethod.java
new file mode 100644
index 00000000000..8fc5212de46
--- /dev/null
+++ b/checker/src/main/java/org/checkerframework/checker/interning/qual/CompareToMethod.java
@@ -0,0 +1,21 @@
+package org.checkerframework.checker.interning.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.InheritedAnnotation;
+
+/**
+ * Method declaration annotation that indicates a method has a specification like {@code
+ * compareTo()} or {@code compare()}. The Interning Checker permits use of {@code if (this == arg) {
+ * return 0; }} or {@code if (arg1 == arg2) { return 0; }} within the body.
+ *
+ * @checker_framework.manual #interning-checker Interning Checker
+ */
+@Documented
+@Target(ElementType.METHOD)
+@Retention(RetentionPolicy.RUNTIME)
+@InheritedAnnotation
+public @interface CompareToMethod {}
diff --git a/checker/src/main/java/org/checkerframework/checker/interning/qual/EqualsMethod.java b/checker/src/main/java/org/checkerframework/checker/interning/qual/EqualsMethod.java
new file mode 100644
index 00000000000..727024e2759
--- /dev/null
+++ b/checker/src/main/java/org/checkerframework/checker/interning/qual/EqualsMethod.java
@@ -0,0 +1,21 @@
+package org.checkerframework.checker.interning.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.InheritedAnnotation;
+
+/**
+ * Method declaration annotation that indicates a method has a specification like {@code equals()}.
+ * The Interning Checker permits use of {@code this == arg} within the body. Can also be applied to
+ * a static two-argument method, in which case {@code arg1 == arg2} is permitted within the body.
+ *
+ * @checker_framework.manual #interning-checker Interning Checker
+ */
+@Documented
+@Target(ElementType.METHOD)
+@Retention(RetentionPolicy.RUNTIME)
+@InheritedAnnotation
+public @interface EqualsMethod {}
diff --git a/checker/src/main/java/org/checkerframework/checker/interning/qual/FindDistinct.java b/checker/src/main/java/org/checkerframework/checker/interning/qual/FindDistinct.java
new file mode 100644
index 00000000000..9797d7c2363
--- /dev/null
+++ b/checker/src/main/java/org/checkerframework/checker/interning/qual/FindDistinct.java
@@ -0,0 +1,24 @@
+package org.checkerframework.checker.interning.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * This formal parameter annotation indicates that the method searches for the given value, using
+ * reference equality ({@code ==}).
+ *
+ *
Within the method, the formal parameter is treated as {@code @}{@link InternedDistinct}: it
+ * should be compared with {@code ==} rather than with {@code equals()}. However, any value may be
+ * passed to the method, and the Interning Checker does not verify that use of {@code ==} within the
+ * method is logically correct.
+ *
+ * @see org.checkerframework.checker.interning.InterningChecker
+ * @checker_framework.manual #interning-checker Interning Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.PARAMETER})
+public @interface FindDistinct {}
diff --git a/checker/src/main/java/org/checkerframework/checker/interning/qual/InternMethod.java b/checker/src/main/java/org/checkerframework/checker/interning/qual/InternMethod.java
index 7385ba20cf0..9157a728860 100644
--- a/checker/src/main/java/org/checkerframework/checker/interning/qual/InternMethod.java
+++ b/checker/src/main/java/org/checkerframework/checker/interning/qual/InternMethod.java
@@ -2,10 +2,10 @@
import java.lang.annotation.Documented;
import java.lang.annotation.ElementType;
-import java.lang.annotation.Inherited;
import java.lang.annotation.Retention;
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.InheritedAnnotation;
/**
* Method declaration annotation used to indicate that this method may be invoked on an uninterned
@@ -16,5 +16,5 @@
@Documented
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
-@Inherited
+@InheritedAnnotation
public @interface InternMethod {}
diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java b/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java
index 40f4e27dbdb..f109f81e135 100644
--- a/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java
+++ b/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java
@@ -343,7 +343,8 @@ protected void commonAssignmentCheck(
AnnotatedTypeMirror varType,
AnnotatedTypeMirror valueType,
Tree valueTree,
- @CompilerMessageKey String errorKey) {
+ @CompilerMessageKey String errorKey,
+ Object... extraArgs) {
Kind valueTreeKind = valueTree.getKind();
@@ -430,7 +431,7 @@ protected void commonAssignmentCheck(
}
}
- super.commonAssignmentCheck(varType, valueType, valueTree, errorKey);
+ super.commonAssignmentCheck(varType, valueType, valueTree, errorKey, extraArgs);
}
@Override
@@ -1087,6 +1088,7 @@ private boolean isTreeSymbolEffectivelyFinalOrUnmodifiable(Tree tree) {
}
@Override
+ @SuppressWarnings("interning:not.interned") // AST node comparison
public Void visitIdentifier(IdentifierTree tree, Void p) {
// If the identifier is a field accessed via an implicit this,
// then check the lock of this. (All other field accessed are checked in visitMemberSelect.
diff --git a/checker/src/main/java/org/checkerframework/checker/lock/qual/GuardedBy.java b/checker/src/main/java/org/checkerframework/checker/lock/qual/GuardedBy.java
index 31a8fc3330c..5e7b74902c0 100644
--- a/checker/src/main/java/org/checkerframework/checker/lock/qual/GuardedBy.java
+++ b/checker/src/main/java/org/checkerframework/checker/lock/qual/GuardedBy.java
@@ -11,6 +11,7 @@
import org.checkerframework.framework.qual.SubtypeOf;
import org.checkerframework.framework.qual.TypeKind;
import org.checkerframework.framework.qual.TypeUseLocation;
+import org.checkerframework.framework.qual.UpperBoundFor;
/**
* Indicates that a thread may dereference the value referred to by the annotated variable only if
@@ -52,7 +53,19 @@
TypeKind.LONG,
TypeKind.SHORT
},
- types = {java.lang.String.class, Void.class})
+ types = {String.class, Void.class})
+@UpperBoundFor(
+ typeKinds = {
+ TypeKind.BOOLEAN,
+ TypeKind.BYTE,
+ TypeKind.CHAR,
+ TypeKind.DOUBLE,
+ TypeKind.FLOAT,
+ TypeKind.INT,
+ TypeKind.LONG,
+ TypeKind.SHORT
+ },
+ types = String.class)
public @interface GuardedBy {
/**
* The Java value expressions that need to be held.
diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java
index b1f91db5088..e4e056e64eb 100644
--- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java
+++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java
@@ -45,6 +45,8 @@
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType;
+import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedNoType;
+import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedPrimitiveType;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedWildcardType;
import org.checkerframework.framework.type.QualifierHierarchy;
import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator;
@@ -356,14 +358,30 @@ public AnnotatedTypeMirror getMethodReturnType(MethodTree m, ReturnTree r) {
}
@Override
- protected TypeAnnotator createTypeAnnotator() {
+ protected DefaultForTypeAnnotator createDefaultForTypeAnnotator() {
DefaultForTypeAnnotator defaultForTypeAnnotator = new DefaultForTypeAnnotator(this);
- defaultForTypeAnnotator.addAtmClass(AnnotatedTypeMirror.AnnotatedNoType.class, NONNULL);
- defaultForTypeAnnotator.addAtmClass(
- AnnotatedTypeMirror.AnnotatedPrimitiveType.class, NONNULL);
+ defaultForTypeAnnotator.addAtmClass(AnnotatedNoType.class, NONNULL);
+ defaultForTypeAnnotator.addAtmClass(AnnotatedPrimitiveType.class, NONNULL);
+ return defaultForTypeAnnotator;
+ }
+
+ @Override
+ protected void addAnnotationsFromDefaultForType(
+ @Nullable Element element, AnnotatedTypeMirror type) {
+ if (element != null
+ && element.getKind() == ElementKind.LOCAL_VARIABLE
+ && type.getKind().isPrimitive()) {
+ // Always apply the DefaultQualifierForUse for primitives.
+ super.addAnnotationsFromDefaultForType(null, type);
+ } else {
+ super.addAnnotationsFromDefaultForType(element, type);
+ }
+ }
+
+ @Override
+ protected TypeAnnotator createTypeAnnotator() {
return new ListTypeAnnotator(
new PropagationTypeAnnotator(this),
- defaultForTypeAnnotator,
new NullnessTypeAnnotator(this),
new CommitmentTypeAnnotator(this));
}
diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessUtil.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessUtil.java
index 1eee7405a79..127a55e80bc 100644
--- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessUtil.java
+++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessUtil.java
@@ -3,6 +3,7 @@
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.framework.qual.AnnotatedFor;
/**
* Utility class for the Nullness Checker.
@@ -15,17 +16,15 @@
*
*
Please note that using this class introduces a runtime dependency. This means that you need to
- * distribute (or link to) the Checker Framework, along with your binaries.
- *
- *
To eliminate this dependency, you can simply copy this class into your own project.
+ *
Runtime Dependency: If you use this class, you must distribute (or link to) {@code
+ * checker-qual.jar}, along with your binaries. Or, you can can copy this class into your own
+ * project.
*/
@SuppressWarnings({
"nullness", // Nullness utilities are trusted regarding nullness.
"cast" // Casts look redundant if Nullness Checker is not run.
})
+@AnnotatedFor("nullness")
public final class NullnessUtil {
private NullnessUtil() {
@@ -63,7 +62,8 @@ private NullnessUtil() {
* is {@code null}. If the exception is ever thrown, then that indicates that the programmer
* misused the method by using it in a circumstance where its argument can be null.
*
- * @param ref a reference of @Nullable type
+ * @param the type of the reference
+ * @param ref a reference of @Nullable type, that is non-null at run time
* @return the argument, casted to have the type qualifier @NonNull
*/
public static @EnsuresNonNull("#1") @NonNull T castNonNull(
@@ -72,16 +72,36 @@ private NullnessUtil() {
return (@NonNull T) ref;
}
+ /**
+ * Suppress warnings from the Nullness Checker, with a custom error message. See {@link
+ * #castNonNull(Object)} for documentation.
+ *
+ * @see #castNonNull(Object)
+ * @param the type of the reference
+ * @param ref a reference of @Nullable type, that is non-null at run time
+ * @param message text to include if this method is misused
+ * @return the argument, casted to have the type qualifier @NonNull
+ */
+ public static @EnsuresNonNull("#1") @NonNull T castNonNull(
+ @Nullable T ref, String message) {
+ assert ref != null : "Misuse of castNonNull: called with a null argument: " + message;
+ return (@NonNull T) ref;
+ }
+
/**
* Like castNonNull, but whereas that method only checks and casts the reference itself, this
* traverses all levels of the argument array. The array is recursively checked to ensure that
* all elements at every array level are non-null.
*
+ * @param the component type of the array
+ * @param arr an array all of whose elements, and their elements recursively, are non-null at
+ * run time
+ * @return the argument, casted to have the type qualifier @NonNull at all levels
* @see #castNonNull(Object)
*/
public static @EnsuresNonNull("#1")
@NonNull T @NonNull [] castNonNullDeep(T @Nullable [] arr) {
- return (@NonNull T[]) castNonNullArray(arr);
+ return (@NonNull T[]) castNonNullArray(arr, null);
}
/**
@@ -89,11 +109,32 @@ private NullnessUtil() {
* traverses all levels of the argument array. The array is recursively checked to ensure that
* all elements at every array level are non-null.
*
+ * @param the component type of the array
+ * @param arr an array all of whose elements, and their elements recursively, are non-null at
+ * run time
+ * @param message text to include if this method is misused
+ * @return the argument, casted to have the type qualifier @NonNull at all levels
+ * @see #castNonNull(Object)
+ */
+ public static @EnsuresNonNull("#1")
+ @NonNull T @NonNull [] castNonNullDeep(T @Nullable [] arr, String message) {
+ return (@NonNull T[]) castNonNullArray(arr, message);
+ }
+
+ /**
+ * Like castNonNull, but whereas that method only checks and casts the reference itself, this
+ * traverses all levels of the argument array. The array is recursively checked to ensure that
+ * all elements at every array level are non-null.
+ *
+ * @param the component type of the component type of the array
+ * @param arr an array all of whose elements, and their elements recursively, are non-null at
+ * run time
+ * @return the argument, casted to have the type qualifier @NonNull at all levels
* @see #castNonNull(Object)
*/
public static @EnsuresNonNull("#1")
@NonNull T @NonNull [][] castNonNullDeep(T @Nullable [] @Nullable [] arr) {
- return (@NonNull T[][]) castNonNullArray(arr);
+ return (@NonNull T[][]) castNonNullArray(arr, null);
}
/**
@@ -101,11 +142,32 @@ private NullnessUtil() {
* traverses all levels of the argument array. The array is recursively checked to ensure that
* all elements at every array level are non-null.
*
+ * @param the component type of the component type of the array
+ * @param arr an array all of whose elements, and their elements recursively, are non-null at
+ * run time
+ * @param message text to include if this method is misused
+ * @return the argument, casted to have the type qualifier @NonNull at all levels
+ * @see #castNonNull(Object)
+ */
+ public static @EnsuresNonNull("#1")
+ @NonNull T @NonNull [][] castNonNullDeep(T @Nullable [] @Nullable [] arr, String message) {
+ return (@NonNull T[][]) castNonNullArray(arr, message);
+ }
+
+ /**
+ * Like castNonNull, but whereas that method only checks and casts the reference itself, this
+ * traverses all levels of the argument array. The array is recursively checked to ensure that
+ * all elements at every array level are non-null.
+ *
+ * @param the component type (three levels in) of the array
+ * @param arr an array all of whose elements, and their elements recursively, are non-null at
+ * run time
+ * @return the argument, casted to have the type qualifier @NonNull at all levels
* @see #castNonNull(Object)
*/
public static @EnsuresNonNull("#1")
@NonNull T @NonNull [][][] castNonNullDeep(T @Nullable [] @Nullable [] @Nullable [] arr) {
- return (@NonNull T[][][]) castNonNullArray(arr);
+ return (@NonNull T[][][]) castNonNullArray(arr, null);
}
/**
@@ -113,12 +175,52 @@ private NullnessUtil() {
* traverses all levels of the argument array. The array is recursively checked to ensure that
* all elements at every array level are non-null.
*
+ * @param the component type (three levels in) of the array
+ * @param arr an array all of whose elements, and their elements recursively, are non-null at
+ * run time
+ * @param message text to include if this method is misused
+ * @return the argument, casted to have the type qualifier @NonNull at all levels
+ * @see #castNonNull(Object)
+ */
+ public static @EnsuresNonNull("#1")
+ @NonNull T @NonNull [][][] castNonNullDeep(
+ T @Nullable [] @Nullable [] @Nullable [] arr, String message) {
+ return (@NonNull T[][][]) castNonNullArray(arr, message);
+ }
+
+ /**
+ * Like castNonNull, but whereas that method only checks and casts the reference itself, this
+ * traverses all levels of the argument array. The array is recursively checked to ensure that
+ * all elements at every array level are non-null.
+ *
+ * @param the component type of the array
+ * @param arr an array all of whose elements, and their elements recursively, are non-null at
+ * run time
+ * @return the argument, casted to have the type qualifier @NonNull at all levels
* @see #castNonNull(Object)
*/
public static @EnsuresNonNull("#1")
@NonNull T @NonNull [][][][] castNonNullDeep(
T @Nullable [] @Nullable [] @Nullable [] @Nullable [] arr) {
- return (@NonNull T[][][][]) castNonNullArray(arr);
+ return (@NonNull T[][][][]) castNonNullArray(arr, null);
+ }
+
+ /**
+ * Like castNonNull, but whereas that method only checks and casts the reference itself, this
+ * traverses all levels of the argument array. The array is recursively checked to ensure that
+ * all elements at every array level are non-null.
+ *
+ * @param the component type (four levels in) of the array
+ * @param arr an array all of whose elements, and their elements recursively, are non-null at
+ * run time
+ * @param message text to include if this method is misused
+ * @return the argument, casted to have the type qualifier @NonNull at all levels
+ * @see #castNonNull(Object)
+ */
+ public static @EnsuresNonNull("#1")
+ @NonNull T @NonNull [][][][] castNonNullDeep(
+ T @Nullable [] @Nullable [] @Nullable [] @Nullable [] arr, String message) {
+ return (@NonNull T[][][][]) castNonNullArray(arr, message);
}
/**
@@ -126,26 +228,73 @@ private NullnessUtil() {
* traverses all levels of the argument array. The array is recursively checked to ensure that
* all elements at every array level are non-null.
*
+ * @param the component type (four levels in) of the array
+ * @param arr an array all of whose elements, and their elements recursively, are non-null at
+ * run time
+ * @return the argument, casted to have the type qualifier @NonNull at all levels
* @see #castNonNull(Object)
*/
public static @EnsuresNonNull("#1")
@NonNull T @NonNull [][][][][] castNonNullDeep(
T @Nullable [] @Nullable [] @Nullable [] @Nullable [] @Nullable [] arr) {
- return (@NonNull T[][][][][]) castNonNullArray(arr);
+ return (@NonNull T[][][][][]) castNonNullArray(arr, null);
}
+ /**
+ * Like castNonNull, but whereas that method only checks and casts the reference itself, this
+ * traverses all levels of the argument array. The array is recursively checked to ensure that
+ * all elements at every array level are non-null.
+ *
+ * @param the component type (five levels in) of the array
+ * @param arr an array all of whose elements, and their elements recursively, are non-null at
+ * run time
+ * @param message text to include if this method is misused
+ * @return the argument, casted to have the type qualifier @NonNull at all levels
+ * @see #castNonNull(Object)
+ */
+ public static @EnsuresNonNull("#1")
+ @NonNull T @NonNull [][][][][] castNonNullDeep(
+ T @Nullable [] @Nullable [] @Nullable [] @Nullable [] @Nullable [] arr,
+ String message) {
+ return (@NonNull T[][][][][]) castNonNullArray(arr, message);
+ }
+
+ /**
+ * The implementation of castNonNullDeep.
+ *
+ * @param the component type (five levels in) of the array
+ * @param arr an array all of whose elements, and their elements recursively, are non-null at
+ * run time
+ * @param message text to include if there is a non-null value, or null to use uncustomized
+ * message
+ * @return the argument, casted to have the type qualifier @NonNull at all levels
+ */
private static @NonNull T @NonNull [] castNonNullArray(
- T @Nullable [] arr) {
- assert arr != null : "Misuse of castNonNullArray: called with a null array argument";
+ T @Nullable [] arr, @Nullable String message) {
+ assert arr != null
+ : "Misuse of castNonNullArray: called with a null array argument"
+ + ((message == null) ? "" : (": " + message));
for (int i = 0; i < arr.length; ++i) {
- assert arr[i] != null : "Misuse of castNonNull: called with a null array element";
- checkIfArray(arr[i]);
+ assert arr[i] != null
+ : "Misuse of castNonNull: called with a null array element"
+ + ((message == null) ? "" : (": " + message));
+ checkIfArray(arr[i], message);
}
return (@NonNull T[]) arr;
}
- private static void checkIfArray(@NonNull Object ref) {
- assert ref != null : "Misuse of checkIfArray: called with a null argument";
+ /**
+ * If the argument is an array, requires it to be non-null at all levels.
+ *
+ * @param ref a value; if an array, all of its elements, and their elements recursively, are
+ * non-null at run time
+ * @param message text to include if there is a non-null value, or null to use uncustomized
+ * message
+ */
+ private static void checkIfArray(@NonNull Object ref, @Nullable String message) {
+ assert ref != null
+ : "Misuse of checkIfArray: called with a null argument"
+ + ((message == null) ? "" : (": " + message));
Class> comp = ref.getClass().getComponentType();
if (comp != null) {
// comp is non-null for arrays, otherwise null.
@@ -153,7 +302,7 @@ private static void checkIfArray(@NonNull Object ref) {
// Nothing to do for arrays of primitive type: primitives are
// never null.
} else {
- castNonNullArray((Object[]) ref);
+ castNonNullArray((Object[]) ref, message);
}
}
}
diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java
index e72a5392f39..91ed8d9cfff 100644
--- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java
+++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java
@@ -41,7 +41,11 @@
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.common.basetype.BaseTypeValidator;
+import org.checkerframework.common.basetype.BaseTypeVisitor;
+import org.checkerframework.common.basetype.TypeValidator;
import org.checkerframework.framework.flow.CFCFGBuilder;
+import org.checkerframework.framework.type.AnnotatedTypeFactory;
import org.checkerframework.framework.type.AnnotatedTypeMirror;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType;
@@ -175,7 +179,10 @@ private boolean containsSameByName(
@Override
protected void commonAssignmentCheck(
- Tree varTree, ExpressionTree valueExp, @CompilerMessageKey String errorKey) {
+ Tree varTree,
+ ExpressionTree valueExp,
+ @CompilerMessageKey String errorKey,
+ Object... extraArgs) {
// allow MonotonicNonNull to be initialized to null at declaration
if (varTree.getKind() == Tree.Kind.VARIABLE) {
@@ -187,20 +194,21 @@ protected void commonAssignmentCheck(
return;
}
}
- super.commonAssignmentCheck(varTree, valueExp, errorKey);
+ super.commonAssignmentCheck(varTree, valueExp, errorKey, extraArgs);
}
@Override
protected void commonAssignmentCheck(
AnnotatedTypeMirror varType,
ExpressionTree valueExp,
- @CompilerMessageKey String errorKey) {
+ @CompilerMessageKey String errorKey,
+ Object... extraArgs) {
// Use the valueExp as the context because data flow will have a value for that tree.
// It might not have a value for the var tree. This is sound because
// if data flow has determined @PolyNull is @Nullable at the RHS, then
// it is also @Nullable for the LHS.
atypeFactory.replacePolyQualifier(varType, valueExp);
- super.commonAssignmentCheck(varType, valueExp, errorKey);
+ super.commonAssignmentCheck(varType, valueExp, errorKey, extraArgs);
}
@Override
@@ -208,7 +216,8 @@ protected void commonAssignmentCheck(
AnnotatedTypeMirror varType,
AnnotatedTypeMirror valueType,
Tree valueTree,
- @CompilerMessageKey String errorKey) {
+ @CompilerMessageKey String errorKey,
+ Object... extraArgs) {
if (TypesUtils.isPrimitive(varType.getUnderlyingType())
&& !TypesUtils.isPrimitive(valueType.getUnderlyingType())) {
boolean succeed = checkForNullability(valueType, valueTree, UNBOXING_OF_NULLABLE);
@@ -217,7 +226,7 @@ protected void commonAssignmentCheck(
return;
}
}
- super.commonAssignmentCheck(varType, valueType, valueTree, errorKey);
+ super.commonAssignmentCheck(varType, valueType, valueTree, errorKey, extraArgs);
}
/** Case 1: Check for null dereferencing. */
@@ -289,6 +298,13 @@ private static boolean isNewArrayAllZeroDims(NewArrayTree node) {
return isAllZeros;
}
+ /**
+ * Return true if the given node is "new X[]", in the context "toArray(new X[])".
+ *
+ * @param node a node to test
+ * @return true if the node is a new array within acall to toArray()
+ */
+ @SuppressWarnings("interning:not.interned") // comparisons of Name objects
private boolean isNewArrayInToArray(NewArrayTree node) {
if (node.getDimensions().size() != 1) {
return false;
@@ -636,4 +652,39 @@ public Void visitAnnotation(AnnotationTree node, Void p) {
// All annotation arguments are non-null and initialized, so no need to check them.
return null;
}
+
+ @Override
+ protected TypeValidator createTypeValidator() {
+ return new NullnessValidator(checker, this, atypeFactory);
+ }
+
+ /**
+ * Check that primitive types are annotated with {@code @NonNull} even if they are the type of a
+ * local variable.
+ */
+ private static class NullnessValidator extends BaseTypeValidator {
+
+ /**
+ * Create NullnessValidator.
+ *
+ * @param checker checker
+ * @param visitor visitor
+ * @param atypeFactory factory
+ */
+ public NullnessValidator(
+ BaseTypeChecker checker,
+ BaseTypeVisitor> visitor,
+ AnnotatedTypeFactory atypeFactory) {
+ super(checker, visitor, atypeFactory);
+ }
+
+ @Override
+ protected boolean shouldCheckTopLevelDeclaredOrPrimitiveType(
+ AnnotatedTypeMirror type, Tree tree) {
+ if (type.getKind().isPrimitive()) {
+ return true;
+ }
+ return super.shouldCheckTopLevelDeclaredOrPrimitiveType(type, tree);
+ }
+ }
}
diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/Opt.java b/checker/src/main/java/org/checkerframework/checker/nullness/Opt.java
index 149b9f4f9eb..36a93442c0c 100644
--- a/checker/src/main/java/org/checkerframework/checker/nullness/Opt.java
+++ b/checker/src/main/java/org/checkerframework/checker/nullness/Opt.java
@@ -8,6 +8,7 @@
import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.framework.qual.AnnotatedFor;
/**
* Utility class for the Nullness Checker, providing every method in {@link java.util.Optional}, but
@@ -21,15 +22,13 @@
*
*
Please note that using this class introduces a runtime dependency. This means that you need to
- * distribute (or link to) {@code checker-qual.jar}, along with your binaries.
- *
- *
To eliminate this dependency, you can simply copy this class into your own project.
+ *
Runtime Dependency: If you use this class, you must distribute (or link to) {@code
+ * checker-qual.jar}, along with your binaries. Or, you can can copy this class into your own
+ * project.
*
* @see java.util.Optional
*/
+@AnnotatedFor("nullness")
public final class Opt {
/** The Opt class cannot be instantiated. */
@@ -40,6 +39,7 @@ private Opt() {
/**
* If primary is non-null, returns it, otherwise throws NoSuchElementException.
*
+ * @param the type of the argument
* @param primary a non-null value to return
* @return {@code primary} if it is non-null
* @throws NoSuchElementException if primary is null
diff --git a/checker/src/main/java/org/checkerframework/checker/regex/RegexUtil.java b/checker/src/main/java/org/checkerframework/checker/regex/RegexUtil.java
index 2269bfa4b9b..157f2cf520b 100644
--- a/checker/src/main/java/org/checkerframework/checker/regex/RegexUtil.java
+++ b/checker/src/main/java/org/checkerframework/checker/regex/RegexUtil.java
@@ -10,6 +10,7 @@
import org.checkerframework.checker.regex.qual.Regex;
import org.checkerframework.dataflow.qual.Pure;
import org.checkerframework.dataflow.qual.SideEffectFree;
+import org.checkerframework.framework.qual.AnnotatedFor;
import org.checkerframework.framework.qual.EnsuresQualifierIf;
/**
@@ -20,13 +21,12 @@
* href="https://checkerframework.org/manual/#regexutil-methods">Testing whether a string is a
* regular expression in the Checker Framework manual.
*
- *
Runtime Dependency: Using this class introduces a runtime dependency on the
- * checker-qual package. To eliminate this dependency, you can simply copy this class into your own
+ *
Runtime Dependency: If you use this class, you must distribute (or link to) {@code
+ * checker-qual.jar}, along with your binaries. Or, you can can copy this class into your own
* project.
*/
-// The Purity Checker cannot show for most methods in this class that
-// they are pure, even though they are.
-@SuppressWarnings("all:purity")
+@SuppressWarnings("allcheckers:purity")
+@AnnotatedFor("nullness")
public final class RegexUtil {
/** This class is a collection of methods; it does not represent anything. */
diff --git a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessAnnotatedTypeFactory.java
index e3f5d8daff5..c2f947267cd 100644
--- a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessAnnotatedTypeFactory.java
+++ b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessAnnotatedTypeFactory.java
@@ -6,10 +6,14 @@
import java.lang.annotation.Annotation;
import java.util.Set;
import javax.lang.model.element.AnnotationMirror;
+import javax.lang.model.element.Element;
+import javax.lang.model.type.PrimitiveType;
import javax.lang.model.type.TypeKind;
import javax.lang.model.type.TypeMirror;
+import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.checker.signedness.qual.Signed;
import org.checkerframework.checker.signedness.qual.SignedPositive;
+import org.checkerframework.checker.signedness.qual.SignednessBottom;
import org.checkerframework.checker.signedness.qual.SignednessGlb;
import org.checkerframework.checker.signedness.qual.UnknownSignedness;
import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
@@ -20,14 +24,20 @@
import org.checkerframework.common.value.qual.IntRangeFromNonNegative;
import org.checkerframework.common.value.qual.IntRangeFromPositive;
import org.checkerframework.common.value.util.Range;
-import org.checkerframework.framework.qual.TypeUseLocation;
import org.checkerframework.framework.type.AnnotatedTypeFactory;
import org.checkerframework.framework.type.AnnotatedTypeMirror;
+import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType;
+import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedPrimitiveType;
+import org.checkerframework.framework.type.DefaultTypeHierarchy;
+import org.checkerframework.framework.type.QualifierHierarchy;
+import org.checkerframework.framework.type.TypeHierarchy;
import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator;
import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator;
import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
-import org.checkerframework.framework.util.defaults.QualifierDefaults;
import org.checkerframework.javacutil.AnnotationBuilder;
+import org.checkerframework.javacutil.AnnotationUtils;
+import org.checkerframework.javacutil.BugInCF;
+import org.checkerframework.javacutil.TypesUtils;
/**
* The type factory for the Signedness Checker.
@@ -36,14 +46,17 @@
*/
public class SignednessAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
- /** The @SignednessGlb annotation. */
- private final AnnotationMirror SIGNEDNESS_GLB =
- AnnotationBuilder.fromClass(elements, SignednessGlb.class);
- /** The @Signed annotation. */
- private final AnnotationMirror SIGNED = AnnotationBuilder.fromClass(elements, Signed.class);
/** The @UnknownSignedness annotation. */
private final AnnotationMirror UNKNOWN_SIGNEDNESS =
AnnotationBuilder.fromClass(elements, UnknownSignedness.class);
+ /** The @Signed annotation. */
+ private final AnnotationMirror SIGNED = AnnotationBuilder.fromClass(elements, Signed.class);
+ /** The @SignednessGlb annotation. */
+ private final AnnotationMirror SIGNEDNESS_GLB =
+ AnnotationBuilder.fromClass(elements, SignednessGlb.class);
+ /** The @SignednessBottom annotation. */
+ private final AnnotationMirror SIGNEDNESS_BOTTOM =
+ AnnotationBuilder.fromClass(elements, SignednessBottom.class);
/** The @NonNegative annotation of the Index Checker, as represented by the Value Checker. */
private final AnnotationMirror INT_RANGE_FROM_NON_NEGATIVE =
@@ -73,12 +86,6 @@ protected Set> createSupportedTypeQualifiers() {
@Override
protected void addComputedTypeAnnotations(
Tree tree, AnnotatedTypeMirror type, boolean iUseFlow) {
- // Prevent @ImplicitFor from applying to local variables of type byte, short, int, and long,
- // but adding the top type to them, which permits flow-sensitive type refinement.
- // (When it is possible to default types based on their TypeKinds,
- // this whole method will no longer be needed.)
- addUnknownSignednessToSomeLocals(tree, type);
-
if (!computingAnnotatedTypeMirrorOfLHS) {
addSignednessGlbAnnotation(tree, type);
}
@@ -162,25 +169,6 @@ private void addSignednessGlbAnnotation(Tree tree, AnnotatedTypeMirror type) {
}
}
- /**
- * If the tree is a local variable and the type is byte, short, int, or long, then add the
- * UnknownSignedness annotation so that dataflow can refine it.
- */
- private void addUnknownSignednessToSomeLocals(Tree tree, AnnotatedTypeMirror type) {
- switch (type.getKind()) {
- case BYTE:
- case SHORT:
- case INT:
- case LONG:
- QualifierDefaults defaults = new QualifierDefaults(elements, this);
- defaults.addCheckedCodeDefault(UNKNOWN_SIGNEDNESS, TypeUseLocation.LOCAL_VARIABLE);
- defaults.annotate(tree, type);
- break;
- default:
- // Nothing for other cases.
- }
- }
-
@Override
protected TreeAnnotator createTreeAnnotator() {
return new ListTreeAnnotator(
@@ -188,10 +176,14 @@ protected TreeAnnotator createTreeAnnotator() {
}
/**
- * This TreeAnnotator ensures that boolean expressions are not given Unsigned or Signed
- * annotations by {@link PropagationTreeAnnotator}, that shift results take on the type of their
- * left operand, and that the types of identifiers are refined based on the results of the Value
- * Checker.
+ * This TreeAnnotator ensures that:
+ *
+ *
+ *
boolean expressions are not given Unsigned or Signed annotations by {@link
+ * PropagationTreeAnnotator},
+ *
shift results take on the type of their left operand,
+ *
the types of identifiers are refined based on the results of the Value Checker.
+ *
*/
private class SignednessTreeAnnotator extends TreeAnnotator {
@@ -235,4 +227,153 @@ public Void visitCompoundAssignment(CompoundAssignmentTree tree, AnnotatedTypeMi
return null;
}
}
+
+ @Override
+ protected void addAnnotationsFromDefaultForType(
+ @Nullable Element element, AnnotatedTypeMirror type) {
+ if (TypesUtils.isFloating(type.getUnderlyingType())
+ || TypesUtils.isBoxedFloating(type.getUnderlyingType())
+ || type.getKind() == TypeKind.CHAR
+ || TypesUtils.isDeclaredOfName(type.getUnderlyingType(), "java.lang.Character")) {
+ // Floats are always signed and chars are always unsigned.
+ super.addAnnotationsFromDefaultForType(null, type);
+ } else {
+ super.addAnnotationsFromDefaultForType(element, type);
+ }
+ }
+
+ @Override
+ protected TypeHierarchy createTypeHierarchy() {
+ return new SignednessTypeHierarchy(
+ checker,
+ getQualifierHierarchy(),
+ checker.getBooleanOption("ignoreRawTypeArguments", true),
+ checker.hasOption("invariantArrays"));
+ }
+
+ /**
+ * The type hierarchy for the signedness type system. If A is narrower (fewer bits) than B, then
+ * A with any qualifier is a subtype of @SignedPositive B.
+ */
+ protected class SignednessTypeHierarchy extends DefaultTypeHierarchy {
+
+ /**
+ * Create a new SignednessTypeHierarchy.
+ *
+ * @param checker the checker
+ * @param qualifierHierarchy the qualifier hierarchy
+ * @param ignoreRawTypes from -AignoreRawTypes
+ * @param invariantArrayComponents from -AinvariantArrays
+ */
+ public SignednessTypeHierarchy(
+ BaseTypeChecker checker,
+ QualifierHierarchy qualifierHierarchy,
+ boolean ignoreRawTypes,
+ boolean invariantArrayComponents) {
+ super(checker, qualifierHierarchy, ignoreRawTypes, invariantArrayComponents);
+ }
+
+ @Override
+ public Boolean visitPrimitive_Primitive(
+ AnnotatedPrimitiveType subtype, AnnotatedPrimitiveType supertype, Void p) {
+
+ boolean superResult = super.visitPrimitive_Primitive(subtype, supertype, p);
+ if (superResult) {
+ return true;
+ }
+
+ PrimitiveType subPrimitive = subtype.getUnderlyingType();
+ PrimitiveType superPrimitive = supertype.getUnderlyingType();
+ if (isNarrowerIntegral(subPrimitive, superPrimitive)) {
+ AnnotationMirror superAnno = supertype.getAnnotationInHierarchy(UNKNOWN_SIGNEDNESS);
+ if (!AnnotationUtils.areSameByName(superAnno, SIGNEDNESS_BOTTOM)) {
+ return true;
+ }
+ }
+
+ return false;
+ }
+
+ @Override
+ public Boolean visitPrimitive_Declared(
+ AnnotatedPrimitiveType subtype, AnnotatedDeclaredType supertype, Void p) {
+ boolean superBoxed = TypesUtils.isBoxedPrimitive(supertype.getUnderlyingType());
+ if (superBoxed) {
+ return visitPrimitive_Primitive(subtype, getUnboxedType(supertype), p);
+ }
+ return super.visitPrimitive_Declared(subtype, supertype, p);
+ }
+
+ @Override
+ public Boolean visitDeclared_Declared(
+ AnnotatedDeclaredType subtype, AnnotatedDeclaredType supertype, Void p) {
+ boolean subBoxed = TypesUtils.isBoxedPrimitive(subtype.getUnderlyingType());
+ if (subBoxed) {
+ boolean superBoxed = TypesUtils.isBoxedPrimitive(supertype.getUnderlyingType());
+ if (superBoxed) {
+ return visitPrimitive_Primitive(
+ getUnboxedType(subtype), getUnboxedType(supertype), p);
+ }
+ }
+ return super.visitDeclared_Declared(subtype, supertype, p);
+ }
+
+ @Override
+ public Boolean visitDeclared_Primitive(
+ AnnotatedDeclaredType subtype, AnnotatedPrimitiveType supertype, Void p) {
+ boolean subBoxed = TypesUtils.isBoxedPrimitive(subtype.getUnderlyingType());
+ if (subBoxed) {
+ return visitPrimitive_Primitive(getUnboxedType(subtype), supertype, p);
+ }
+ return super.visitDeclared_Primitive(subtype, supertype, p);
+ }
+
+ /**
+ * Returns true if both types are integral and the first type is strictly narrower
+ * (represented by fewer bits) than the second type.
+ *
+ * @param a a primitive type
+ * @param b a primitive type
+ * @return true if {@code a} is represented by fewer bits than {@code b}
+ */
+ private boolean isNarrowerIntegral(PrimitiveType a, PrimitiveType b) {
+ int aBits = numIntegralBits(a);
+ if (aBits == -1) {
+ return false;
+ }
+ int bBits = numIntegralBits(b);
+ if (bBits == -1) {
+ return false;
+ }
+ return aBits < bBits;
+ }
+
+ /**
+ * Returns the number of bits in the representation of an integral primitive type. Returns
+ * -1 if the type is not an integral primitive type.
+ *
+ * @param p a primitive type
+ * @return the number of bits in its representation, or -1 if not integral
+ */
+ private int numIntegralBits(PrimitiveType p) {
+ switch (p.getKind()) {
+ case BYTE:
+ return 8;
+ case SHORT:
+ return 16;
+ case CHAR:
+ return 16;
+ case INT:
+ return 32;
+ case LONG:
+ return 64;
+ case BOOLEAN:
+ case DOUBLE:
+ case FLOAT:
+ return -1;
+ default:
+ throw new BugInCF("Unexpected primitive type " + p);
+ }
+ }
+ }
}
diff --git a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessUtil.java b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessUtil.java
index 6a846d2f4c1..948ab11dcbd 100644
--- a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessUtil.java
+++ b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessUtil.java
@@ -6,6 +6,7 @@
import java.nio.ByteBuffer;
import java.nio.IntBuffer;
import org.checkerframework.checker.signedness.qual.Unsigned;
+import org.checkerframework.framework.qual.AnnotatedFor;
/**
* Provides static utility methods for unsigned values. Most of these re-implement functionality
@@ -15,6 +16,7 @@
*
* @checker_framework.manual #signedness-utilities Utility routines for manipulating unsigned values
*/
+@AnnotatedFor("nullness")
public final class SignednessUtil {
private SignednessUtil() {
diff --git a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessUtilExtra.java b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessUtilExtra.java
index 464e37c50ae..6b38b1d5202 100644
--- a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessUtilExtra.java
+++ b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessUtilExtra.java
@@ -3,6 +3,7 @@
import java.awt.Dimension;
import java.awt.image.BufferedImage;
import org.checkerframework.checker.signedness.qual.Unsigned;
+import org.checkerframework.framework.qual.AnnotatedFor;
/**
* Provides more static utility methods for unsigned values. These methods use Java packages not
@@ -10,7 +11,9 @@
*
* @checker_framework.manual #signedness-utilities Utility routines for manipulating unsigned values
*/
+@AnnotatedFor("nullness")
public class SignednessUtilExtra {
+ /** Do not instantiate this class. */
private SignednessUtilExtra() {
throw new Error("Do not instantiate");
}
diff --git a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java
index d2b3687d6d8..cef73f24b05 100644
--- a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java
+++ b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java
@@ -10,6 +10,7 @@
import com.sun.source.tree.Tree.Kind;
import com.sun.source.tree.TypeCastTree;
import javax.lang.model.type.TypeKind;
+import org.checkerframework.checker.interning.qual.InternedDistinct;
import org.checkerframework.checker.signedness.qual.PolySigned;
import org.checkerframework.checker.signedness.qual.Signed;
import org.checkerframework.checker.signedness.qual.Unsigned;
@@ -212,7 +213,8 @@ private boolean isMaskedShiftEitherSignedness(BinaryTree shiftExpr) {
// enclosing immediately contains shiftExpr or a parenthesized version of shiftExpr
Tree enclosing = enclosingPair.first;
// enclosingChild is a child of enclosing: shiftExpr or a parenthesized version of it.
- Tree enclosingChild = enclosingPair.second;
+ @SuppressWarnings("interning:assignment.type.incompatible") // comparing AST nodes
+ @InternedDistinct Tree enclosingChild = enclosingPair.second;
if (!isMask(enclosing)) {
return false;
diff --git a/checker/src/main/java/org/checkerframework/checker/signedness/qual/Signed.java b/checker/src/main/java/org/checkerframework/checker/signedness/qual/Signed.java
index 3af02116d87..377e79391ac 100644
--- a/checker/src/main/java/org/checkerframework/checker/signedness/qual/Signed.java
+++ b/checker/src/main/java/org/checkerframework/checker/signedness/qual/Signed.java
@@ -8,6 +8,7 @@
import org.checkerframework.framework.qual.DefaultFor;
import org.checkerframework.framework.qual.SubtypeOf;
import org.checkerframework.framework.qual.TypeKind;
+import org.checkerframework.framework.qual.UpperBoundFor;
/**
* The value is to be interpreted as signed. That is, if the most significant bit in the bitwise
@@ -26,18 +27,17 @@
TypeKind.LONG,
TypeKind.SHORT,
TypeKind.FLOAT,
- TypeKind.DOUBLE,
- TypeKind.CHAR
- }
-
- // This is commented out until implicitly signed boxed types are implemented
- // correctly.
-
- /*,
+ TypeKind.DOUBLE
+ },
types = {
java.lang.Byte.class,
- java.lang.Short.class,
java.lang.Integer.class,
- java.lang.Long.class
- }*/ )
+ java.lang.Long.class,
+ java.lang.Short.class,
+ java.lang.Float.class,
+ java.lang.Double.class
+ })
+@UpperBoundFor(
+ typeKinds = {TypeKind.FLOAT, TypeKind.DOUBLE},
+ types = {java.lang.Float.class, java.lang.Double.class})
public @interface Signed {}
diff --git a/checker/src/main/java/org/checkerframework/checker/signedness/qual/Unsigned.java b/checker/src/main/java/org/checkerframework/checker/signedness/qual/Unsigned.java
index be27a217a1a..3b8029b6996 100644
--- a/checker/src/main/java/org/checkerframework/checker/signedness/qual/Unsigned.java
+++ b/checker/src/main/java/org/checkerframework/checker/signedness/qual/Unsigned.java
@@ -5,7 +5,10 @@
import java.lang.annotation.Retention;
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.DefaultFor;
import org.checkerframework.framework.qual.SubtypeOf;
+import org.checkerframework.framework.qual.TypeKind;
+import org.checkerframework.framework.qual.UpperBoundFor;
/**
* The value is to be interpreted as unsigned. That is, if the most significant bit in the bitwise
@@ -18,4 +21,10 @@
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf({UnknownSignedness.class})
+@DefaultFor(
+ typeKinds = {TypeKind.CHAR},
+ types = {java.lang.Character.class})
+@UpperBoundFor(
+ typeKinds = {TypeKind.CHAR},
+ types = {java.lang.Character.class})
public @interface Unsigned {}
diff --git a/checker/src/main/java/org/checkerframework/checker/units/UnitsTools.java b/checker/src/main/java/org/checkerframework/checker/units/UnitsTools.java
index 2559f5cf923..56f128df42c 100644
--- a/checker/src/main/java/org/checkerframework/checker/units/UnitsTools.java
+++ b/checker/src/main/java/org/checkerframework/checker/units/UnitsTools.java
@@ -21,10 +21,13 @@
import org.checkerframework.checker.units.qual.mol;
import org.checkerframework.checker.units.qual.radians;
import org.checkerframework.checker.units.qual.s;
+import org.checkerframework.framework.qual.AnnotatedFor;
+
+// TODO: add fromTo methods for all useful unit combinations.
/** Utility methods to generate annotated types and to convert between them. */
@SuppressWarnings({"units", "checkstyle:constantname"})
-// TODO: add fromTo methods for all useful unit combinations.
+@AnnotatedFor("nullness")
public class UnitsTools {
// Acceleration
public static final @mPERs2 int mPERs2 = 1;
diff --git a/checker/src/test/java/tests/FormatterUnitTest.java b/checker/src/test/java/tests/FormatterUnitTest.java
new file mode 100644
index 00000000000..f80ae1c895e
--- /dev/null
+++ b/checker/src/test/java/tests/FormatterUnitTest.java
@@ -0,0 +1,45 @@
+package tests;
+
+import org.checkerframework.checker.formatter.FormatUtil;
+import org.junit.Assert;
+import org.junit.Test;
+
+public class FormatterUnitTest {
+
+ @SuppressWarnings("deprecation") // calls methods that are used only for testing
+ @Test
+ public void testConversionCharFromFormat() {
+ Assert.assertEquals('s', FormatUtil.conversionCharFromFormat("%1$2s"));
+ Assert.assertEquals('s', FormatUtil.conversionCharFromFormat("%1$s"));
+ Assert.assertEquals('t', FormatUtil.conversionCharFromFormat("%1$tb"));
+ Assert.assertEquals('t', FormatUtil.conversionCharFromFormat("%1$te"));
+ Assert.assertEquals('t', FormatUtil.conversionCharFromFormat("%1$tm"));
+ Assert.assertEquals('t', FormatUtil.conversionCharFromFormat("%1$tY"));
+ Assert.assertEquals('f', FormatUtil.conversionCharFromFormat("%+10.4f"));
+ Assert.assertEquals('s', FormatUtil.conversionCharFromFormat("%2$2s"));
+ Assert.assertEquals('s', FormatUtil.conversionCharFromFormat("%2$s"));
+ Assert.assertEquals('f', FormatUtil.conversionCharFromFormat("%(,.2f"));
+ Assert.assertEquals('s', FormatUtil.conversionCharFromFormat("%3$2s"));
+ Assert.assertEquals('s', FormatUtil.conversionCharFromFormat("%3$s"));
+ Assert.assertEquals('s', FormatUtil.conversionCharFromFormat("%4$2s"));
+ Assert.assertEquals('s', FormatUtil.conversionCharFromFormat("%4$s"));
+ Assert.assertEquals('s', FormatUtil.conversionCharFromFormat("% {
@@ -29,6 +31,80 @@ public boolean equals(Object o) {
return false;
}
+ @EqualsMethod
+ @org.checkerframework.dataflow.qual.Pure
+ public boolean equals2(Object o) {
+ // Using == is OK if it's the first statement in the equals method
+ // and it compares "this" against the argument.
+ if (this == o) {
+ return true;
+ }
+ // Not the first statement in the method.
+ // :: error: (not.interned)
+ if (o == this) {
+ return true;
+ }
+ return false;
+ }
+
+ @org.checkerframework.dataflow.qual.Pure
+ public boolean equals3(Object o) {
+ // Not equals() or annotated as @EqualsMethod.
+ // :: error: (not.interned)
+ if (this == o) {
+ return true;
+ }
+ // Not the first statement in the method.
+ // :: error: (not.interned)
+ if (o == this) {
+ return true;
+ }
+ return false;
+ }
+
+ @EqualsMethod
+ @org.checkerframework.dataflow.qual.Pure
+ public static boolean equals4(Object thisOne, Object o) {
+ // Using == is OK if it's the first statement in the equals method
+ // and it compares "this" against the argument.
+ if (thisOne == o) {
+ return true;
+ }
+ // Not the first statement in the method.
+ // :: error: (not.interned)
+ if (o == thisOne) {
+ return true;
+ }
+ return false;
+ }
+
+ @org.checkerframework.dataflow.qual.Pure
+ public static boolean equals5(Object thisOne, Object o) {
+ // Not equals() or annotated as @EqualsMethod.
+ // :: error: (not.interned)
+ if (thisOne == o) {
+ return true;
+ }
+ // Not the first statement in the method.
+ // :: error: (not.interned)
+ if (o == thisOne) {
+ return true;
+ }
+ return false;
+ }
+
+ @EqualsMethod
+ // :: error: (invalid.method.annotation)
+ public boolean equals6() {
+ return true;
+ }
+
+ @EqualsMethod
+ // :: error: (invalid.method.annotation)
+ public boolean equals7(int a, int b, int c) {
+ return true;
+ }
+
@Override
@org.checkerframework.dataflow.qual.Pure
public int compareTo(HeuristicsTest o) {
@@ -46,6 +122,82 @@ public int compareTo(HeuristicsTest o) {
return 0;
}
+ @CompareToMethod
+ @org.checkerframework.dataflow.qual.Pure
+ public int compareTo2(HeuristicsTest o) {
+ // Using == is OK if it's the first statement in the equals method
+ // and it compares "this" against the argument.
+
+ if (o == this) {
+ return 0;
+ }
+ // Not the first statement in the method.
+ // :: error: (not.interned)
+ if (this == o) {
+ return 0;
+ }
+ return 0;
+ }
+
+ @org.checkerframework.dataflow.qual.Pure
+ public int compareTo3(HeuristicsTest o) {
+ // Not compareTo or annotated as @CompareToMethod
+ // :: error: (not.interned)
+ if (o == this) {
+ return 0;
+ }
+ // Not the first statement in the method.
+ // :: error: (not.interned)
+ if (this == o) {
+ return 0;
+ }
+ return 0;
+ }
+
+ @CompareToMethod
+ @org.checkerframework.dataflow.qual.Pure
+ public static int compareTo4(HeuristicsTest thisOne, HeuristicsTest o) {
+ // Using == is OK if it's the first statement in the equals method
+ // and it compares "this" against the argument.
+
+ if (o == thisOne) {
+ return 0;
+ }
+ // Not the first statement in the method.
+ // :: error: (not.interned)
+ if (thisOne == o) {
+ return 0;
+ }
+ return 0;
+ }
+
+ @org.checkerframework.dataflow.qual.Pure
+ public static int compareTo5(HeuristicsTest thisOne, HeuristicsTest o) {
+ // Not compareTo or annotated as @CompareToMethod
+ // :: error: (not.interned)
+ if (o == thisOne) {
+ return 0;
+ }
+ // Not the first statement in the method.
+ // :: error: (not.interned)
+ if (thisOne == o) {
+ return 0;
+ }
+ return 0;
+ }
+
+ @EqualsMethod
+ // :: error: (invalid.method.annotation)
+ public boolean compareTo6() {
+ return true;
+ }
+
+ @EqualsMethod
+ // :: error: (invalid.method.annotation)
+ public boolean compareTo7(int a, int b, int c) {
+ return true;
+ }
+
public boolean optimizeEqualsClient(Object a, Object b, Object[] arr) {
// Using == is OK if it's the left-hand side of an || whose right-hand
// side is a call to equals with the same arguments.
diff --git a/checker/tests/interning/ThreadUsesObjectEquals.java b/checker/tests/interning/ThreadUsesObjectEquals.java
new file mode 100644
index 00000000000..e494d1fd364
--- /dev/null
+++ b/checker/tests/interning/ThreadUsesObjectEquals.java
@@ -0,0 +1,5 @@
+public class ThreadUsesObjectEquals {
+ boolean p(Thread a, Thread b) {
+ return a == b;
+ }
+}
diff --git a/checker/tests/interning/UsesObjectEqualsTest.java b/checker/tests/interning/UsesObjectEqualsTest.java
index 883c6ef0d3f..89cb2b297b6 100644
--- a/checker/tests/interning/UsesObjectEqualsTest.java
+++ b/checker/tests/interning/UsesObjectEqualsTest.java
@@ -20,6 +20,22 @@ public boolean equals(Object o) {
}
}
+ @UsesObjectEquals
+ class B3 extends A {
+ @Override
+ public boolean equals(Object o3) {
+ return this == o3;
+ }
+ }
+
+ @UsesObjectEquals
+ class B4 extends A {
+ @Override
+ public boolean equals(Object o4) {
+ return o4 == this;
+ }
+ }
+
// changed to inherited, no (superclass.annotated) warning
class C extends A {}
@@ -60,4 +76,19 @@ class ExtendsInner1 extends UsesObjectEqualsTest.A {}
class ExtendsInner2 extends UsesObjectEqualsTest.A {}
class MyList extends LinkedList {}
+
+ class DoesNotUseObjectEquals {
+ @Override
+ public boolean equals(Object o) {
+ return super.equals(o);
+ }
+ }
+
+ @UsesObjectEquals
+ class SubclassUsesObjectEquals extends DoesNotUseObjectEquals {
+ @Override
+ public boolean equals(Object o) {
+ return this == o;
+ }
+ }
}
diff --git a/checker/tests/lock/ChapterExamples.java b/checker/tests/lock/ChapterExamples.java
index 20305c020f8..cdd316541ff 100644
--- a/checker/tests/lock/ChapterExamples.java
+++ b/checker/tests/lock/ChapterExamples.java
@@ -442,7 +442,6 @@ void unboxing() {
@GuardedBy("lock") Integer b = 1;
int d;
synchronized (lock) {
- // :: error: (assignment.type.incompatible)
d = b;
// Expected, since b cannot be @GuardedBy("lock") since it is a boxed primitive.
@@ -464,7 +463,6 @@ void unboxing() {
c = new Integer(c.intValue() + b.intValue()); // The de-sugared version
}
- // :: error: (assignment.type.incompatible)
a = b;
b = c; // OK
}
diff --git a/checker/tests/lock/Strings.java b/checker/tests/lock/Strings.java
index 1f021ef5b14..568f4a8b51c 100644
--- a/checker/tests/lock/Strings.java
+++ b/checker/tests/lock/Strings.java
@@ -8,17 +8,14 @@
public class Strings {
final Object lock = new Object();
- // Tests that @GuardedBy({}) is @ImplicitFor(typeNames = { java.lang.String.class })
+ // These casts are safe because if the casted Object is a String, it must be @GuardedBy({})
void StringIsGBnothing(
@GuardedByUnknown Object o1,
@GuardedBy("lock") Object o2,
@GuardSatisfied Object o3,
@GuardedByBottom Object o4) {
- // :: error: (assignment.type.incompatible)
String s1 = (String) o1;
- // :: error: (assignment.type.incompatible)
String s2 = (String) o2;
- // :: error: (assignment.type.incompatible)
String s3 = (String) o3;
String s4 = (String) o4; // OK
}
diff --git a/checker/tests/nullness-safedefaultssourcecode/Issue3449.java b/checker/tests/nullness-safedefaultssourcecode/Issue3449.java
new file mode 100644
index 00000000000..417721ecb0a
--- /dev/null
+++ b/checker/tests/nullness-safedefaultssourcecode/Issue3449.java
@@ -0,0 +1,15 @@
+// Test case for https://tinyurl.com/cfissue/3449
+
+import org.checkerframework.framework.qual.AnnotatedFor;
+
+@AnnotatedFor("nullness")
+public class Issue3449 {
+
+ int length;
+ Object[] objs;
+
+ public Issue3449(Object... args) {
+ length = args.length;
+ objs = args;
+ }
+}
diff --git a/checker/tests/nullness/Issue3443.java b/checker/tests/nullness/Issue3443.java
new file mode 100644
index 00000000000..d70d281fb3e
--- /dev/null
+++ b/checker/tests/nullness/Issue3443.java
@@ -0,0 +1,19 @@
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+class Issue3443 {
+ static > Supplier3443 passThrough(T t) {
+ // :: error: (return.type.incompatible)
+ return t;
+ }
+
+ public static void main(String[] args) {
+ Supplier3443<@Nullable String> s1 = () -> null;
+ // TODO: passThrough(s1) should cause an error. #979.
+ Supplier3443 s2 = passThrough(s1);
+ s2.get().toString();
+ }
+}
+
+interface Supplier3443 {
+ T get();
+}
diff --git a/checker/tests/nullness/java8/Issue1098.java b/checker/tests/nullness/java8/Issue1098.java
index f37c81f7d71..aa63d5d92f2 100644
--- a/checker/tests/nullness/java8/Issue1098.java
+++ b/checker/tests/nullness/java8/Issue1098.java
@@ -10,7 +10,7 @@ void cls(Class p1, T p2) {}
void use() {
opt(Optional.empty(), null);
- // TODO: false positive, because type agrument inference does not account for @Covariant.
+ // TODO: false positive, because type argument inference does not account for @Covariant.
// See https://github.com/typetools/checker-framework/issues/979.
// :: error: (argument.type.incompatible)
cls(this.getClass(), null);
diff --git a/checker/tests/nullness/java8/Issue1098NoJdk.java b/checker/tests/nullness/java8/Issue1098NoJdk.java
index 54265353cdb..da7c3ee4f4d 100644
--- a/checker/tests/nullness/java8/Issue1098NoJdk.java
+++ b/checker/tests/nullness/java8/Issue1098NoJdk.java
@@ -12,7 +12,7 @@ class Issue1098NoJdk {
void cls2(Class p1, T p2) {}
void use2(MyObject ths) {
- // TODO: false positive, because type agrument inference does not account for @Covariant.
+ // TODO: false positive, because type argument inference does not account for @Covariant.
// See https://github.com/typetools/checker-framework/issues/979.
// :: error: (argument.type.incompatible)
cls2(ths.getMyClass(), null);
diff --git a/checker/tests/nullness/java8/Issue1633.java b/checker/tests/nullness/java8/Issue1633.java
index 14bf178aa36..48eb06f1e3e 100644
--- a/checker/tests/nullness/java8/Issue1633.java
+++ b/checker/tests/nullness/java8/Issue1633.java
@@ -53,7 +53,7 @@ void foo5(Optional1633 o, Supplier<@NonNull String> supplyNonNull) {
}
void foo6(Optional1633 o, Supplier<@NonNull String> supplyNonNull) {
- // :: error: (argument.type.incompatible) :: error: (assignment.type.incompatible)
+ // :: error: (assignment.type.incompatible)
@NonNull String str1 = o.orElseGetNullable(supplyNonNull);
}
diff --git a/checker/tests/signedness/Arrays.java b/checker/tests/signedness/Arrays.java
new file mode 100644
index 00000000000..c60c1966c6e
--- /dev/null
+++ b/checker/tests/signedness/Arrays.java
@@ -0,0 +1,5 @@
+public class Arrays {
+ void test() {
+ Object[] os = new Double[234];
+ }
+}
diff --git a/checker/tests/signedness/BoxedPrimitives.java b/checker/tests/signedness/BoxedPrimitives.java
new file mode 100644
index 00000000000..010d7d2c101
--- /dev/null
+++ b/checker/tests/signedness/BoxedPrimitives.java
@@ -0,0 +1,83 @@
+import java.util.LinkedList;
+import org.checkerframework.checker.signedness.qual.Signed;
+import org.checkerframework.checker.signedness.qual.Unsigned;
+
+public class BoxedPrimitives {
+
+ @Signed int si;
+ @Unsigned int ui;
+
+ @Signed Integer sbi;
+ @Unsigned Integer ubi;
+
+ void argSigned(@Signed int x) {
+ si = x;
+ sbi = x;
+ // :: error: (assignment.type.incompatible)
+ ui = x;
+ // :: error: (assignment.type.incompatible)
+ ubi = x;
+ }
+
+ void argUnsigned(@Unsigned int x) {
+ // :: error: (assignment.type.incompatible)
+ si = x;
+ // :: error: (assignment.type.incompatible)
+ sbi = x;
+ ui = x;
+ ubi = x;
+ }
+
+ void argSignedBoxed(@Signed Integer x) {
+ si = x;
+ sbi = x;
+ // :: error: (assignment.type.incompatible)
+ ui = x;
+ // :: error: (assignment.type.incompatible)
+ ubi = x;
+ }
+
+ void argUnsignedBoxed(@Unsigned Integer x) {
+ // :: error: (assignment.type.incompatible)
+ si = x;
+ // :: error: (assignment.type.incompatible)
+ sbi = x;
+ ui = x;
+ ubi = x;
+ }
+
+ void client() {
+ argSigned(si);
+ argSignedBoxed(si);
+ argSigned(sbi);
+ argSignedBoxed(sbi);
+ // :: error: (argument.type.incompatible)
+ argUnsigned(si);
+ // :: error: (argument.type.incompatible)
+ argUnsignedBoxed(si);
+ // :: error: (argument.type.incompatible)
+ argUnsigned(sbi);
+ // :: error: (argument.type.incompatible)
+ argUnsignedBoxed(sbi);
+ // :: error: (argument.type.incompatible)
+ argSigned(ui);
+ // :: error: (argument.type.incompatible)
+ argSignedBoxed(ui);
+ // :: error: (argument.type.incompatible)
+ argSigned(ubi);
+ // :: error: (argument.type.incompatible)
+ argSignedBoxed(ubi);
+ argUnsigned(ui);
+ argUnsignedBoxed(ui);
+ argUnsigned(ubi);
+ argUnsignedBoxed(ubi);
+ }
+
+ public LinkedList commands;
+
+ void forLoop() {
+ for (Integer ix : this.commands) {
+ argSigned(ix);
+ }
+ }
+}
diff --git a/checker/tests/signedness/CastedShifts.java b/checker/tests/signedness/CastedShifts.java
index 89dfd16db88..c849822e3bd 100644
--- a/checker/tests/signedness/CastedShifts.java
+++ b/checker/tests/signedness/CastedShifts.java
@@ -36,19 +36,15 @@ public void CastedIntShifts(@Unsigned int unsigned, @Signed int signed) {
byteRes = (@Signed byte) (signed >> 0);
// Cast to char.
- @UnknownSignedness char charRes;
+ char charRes;
// Shifting right by 23, the introduced bits are cast away
charRes = (@Unsigned char) (unsigned >>> 23);
charRes = (@Unsigned char) (unsigned >> 23);
- charRes = (@Signed char) (signed >>> 23);
- charRes = (@Signed char) (signed >> 23);
// Shifting right by 24, the introduced bits are still cast away.
charRes = (@Unsigned char) (unsigned >>> 24);
charRes = (@Unsigned char) (unsigned >> 24);
- charRes = (@Signed char) (signed >>> 24);
- charRes = (@Signed char) (signed >> 24);
// Shifting right by 25, now the MSB matters.
charRes = (@Unsigned char) (unsigned >>> 25);
@@ -56,15 +52,9 @@ public void CastedIntShifts(@Unsigned int unsigned, @Signed int signed) {
// :: error: (shift.signed)
charRes = (@Unsigned char) (unsigned >> 25);
- // :: error: (shift.unsigned)
- charRes = (@Signed char) (signed >>> 25);
- charRes = (@Signed char) (signed >> 25);
-
// Shifting right by zero should behave as assignment
charRes = (@Unsigned char) (unsigned >>> 0);
charRes = (@Unsigned char) (unsigned >> 0);
- charRes = (@Signed char) (signed >>> 0);
- charRes = (@Signed char) (signed >> 0);
// Cast to short.
@UnknownSignedness short shortRes;
@@ -235,19 +225,15 @@ public void CastedLongShifts(@Unsigned long unsigned, @Signed long signed) {
byteRes = (@Signed byte) (signed >> 0);
// Cast to char.
- @UnknownSignedness char charRes;
+ char charRes;
// Shifting right by 55, the introduced bits are cast away
charRes = (@Unsigned char) (unsigned >>> 55);
charRes = (@Unsigned char) (unsigned >> 55);
- charRes = (@Signed char) (signed >>> 55);
- charRes = (@Signed char) (signed >> 55);
// Shifting right by 56, the introduced bits are still cast away.
charRes = (@Unsigned char) (unsigned >>> 56);
charRes = (@Unsigned char) (unsigned >> 56);
- charRes = (@Signed char) (signed >>> 56);
- charRes = (@Signed char) (signed >> 56);
// Shifting right by 57, now the MSB matters.
charRes = (@Unsigned char) (unsigned >>> 57);
@@ -255,15 +241,9 @@ public void CastedLongShifts(@Unsigned long unsigned, @Signed long signed) {
// :: error: (shift.signed)
charRes = (@Unsigned char) (unsigned >> 57);
- // :: error: (shift.unsigned)
- charRes = (@Signed char) (signed >>> 57);
- charRes = (@Signed char) (signed >> 57);
-
// Shifting right by zero should behave as assignment
charRes = (@Unsigned char) (unsigned >>> 0);
charRes = (@Unsigned char) (unsigned >> 0);
- charRes = (@Signed char) (signed >>> 0);
- charRes = (@Signed char) (signed >> 0);
// Cast to short.
@UnknownSignedness short shortRes;
diff --git a/checker/tests/signedness/CompoundAssignments.java b/checker/tests/signedness/CompoundAssignmentsSignedness.java
similarity index 99%
rename from checker/tests/signedness/CompoundAssignments.java
rename to checker/tests/signedness/CompoundAssignmentsSignedness.java
index ebbc8074967..62dccb004a1 100644
--- a/checker/tests/signedness/CompoundAssignments.java
+++ b/checker/tests/signedness/CompoundAssignmentsSignedness.java
@@ -1,6 +1,6 @@
import org.checkerframework.checker.signedness.qual.*;
-public class CompoundAssignments {
+public class CompoundAssignmentsSignedness {
public void DivModTest(
@Unsigned int unsigned,
diff --git a/checker/tests/signedness/DefaultsSignedness.java b/checker/tests/signedness/DefaultsSignedness.java
index 518ac2465ce..c91d9cb4ddb 100644
--- a/checker/tests/signedness/DefaultsSignedness.java
+++ b/checker/tests/signedness/DefaultsSignedness.java
@@ -112,31 +112,14 @@ public void SignedTest(
// Test floats
@Signed float sinFloat;
- @SignednessGlb float conFloat;
sinFloat = testFloat;
- // :: error: (assignment.type.incompatible)
- conFloat = testFloat;
-
// Test doubles
@Signed double sinDouble;
- @SignednessGlb double conDouble;
sinDouble = testDouble;
- // :: error: (assignment.type.incompatible)
- conDouble = testDouble;
-
- // Test chars
- @Signed char sinChar;
- @SignednessGlb char conChar;
-
- sinChar = testChar;
-
- // :: error: (assignment.type.incompatible)
- conChar = testChar;
-
/*
// Test boxed bytes
@Signed Byte sinBoxedByte;
diff --git a/checker/tests/signedness/Issue2483.java b/checker/tests/signedness/Issue2483.java
new file mode 100644
index 00000000000..9217ca9c1ae
--- /dev/null
+++ b/checker/tests/signedness/Issue2483.java
@@ -0,0 +1,8 @@
+import org.checkerframework.checker.signedness.qual.*;
+
+class Issue2483 {
+ void foo(String a, byte[] b) {
+ @Unsigned int len = a.length();
+ @Unsigned int len2 = b.length;
+ }
+}
diff --git a/checker/tests/signedness/LocalVarDefaults.java b/checker/tests/signedness/LocalVarDefaults.java
new file mode 100644
index 00000000000..e80bd610046
--- /dev/null
+++ b/checker/tests/signedness/LocalVarDefaults.java
@@ -0,0 +1,29 @@
+import org.checkerframework.checker.signedness.qual.Signed;
+import org.checkerframework.checker.signedness.qual.Unsigned;
+
+public class LocalVarDefaults {
+
+ void methodInt(@Unsigned int unsignedInt, @Signed int signedInt) {
+ int local = unsignedInt;
+ int local2 = signedInt;
+ }
+
+ // :: error: (type.invalid.annotations.on.use)
+ void methodDouble(@Unsigned double unsigned, @Signed double signed) {
+ // :: error: (assignment.type.incompatible)
+ double local = unsigned;
+ double local2 = signed;
+ }
+
+ void methodInteger(@Unsigned Integer unsignedInt, @Signed Integer signedInt) {
+ Integer local = unsignedInt;
+ Integer local2 = signedInt;
+ }
+
+ // :: error: (type.invalid.annotations.on.use)
+ void methodDoubleWrapper(@Unsigned Double unsigned, @Signed Double signed) {
+ // :: error: (assignment.type.incompatible)
+ Double local = unsigned;
+ Double local2 = signed;
+ }
+}
diff --git a/checker/tests/signedness/PrimitiveCasts.java b/checker/tests/signedness/PrimitiveCasts.java
new file mode 100644
index 00000000000..895b04e19a4
--- /dev/null
+++ b/checker/tests/signedness/PrimitiveCasts.java
@@ -0,0 +1,32 @@
+import org.checkerframework.checker.signedness.qual.Unsigned;
+
+public class PrimitiveCasts {
+
+ void shortToChar1(short s) {
+ // :: warning: (cast.unsafe)
+ char c = (char) s;
+ }
+
+ // These are Java errors.
+ // void shortToChar2(short s) {
+ // char c = s;
+ // }
+ // char shortToChar3(short s) {
+ // return s;
+ // }
+
+ void intToDouble1(@Unsigned int ui) {
+ // :: warning: (cast.unsafe)
+ double d = (double) ui;
+ }
+
+ void intToDouble2(@Unsigned int ui) {
+ // :: error: (assignment.type.incompatible)
+ double d = ui;
+ }
+
+ double intToDouble3(@Unsigned int ui) {
+ // :: error: (return.type.incompatible)
+ return ui;
+ }
+}
diff --git a/checker/tests/signedness/SignednessAssignments.java b/checker/tests/signedness/SignednessAssignments.java
new file mode 100644
index 00000000000..668893710d9
--- /dev/null
+++ b/checker/tests/signedness/SignednessAssignments.java
@@ -0,0 +1,121 @@
+import org.checkerframework.checker.signedness.qual.Signed;
+import org.checkerframework.checker.signedness.qual.SignedPositive;
+import org.checkerframework.checker.signedness.qual.Unsigned;
+
+public class SignednessAssignments {
+
+ @Signed byte sb;
+ @Unsigned byte ub;
+ @Signed Byte sB;
+ @Unsigned Byte uB;
+
+ @Unsigned char uc;
+ @Unsigned Character uC;
+
+ @Signed short ss;
+ @Unsigned short us;
+ @Signed Short sS;
+ @Unsigned Short uS;
+
+ @Signed int si;
+ @Unsigned int ui;
+ @Signed Integer sI;
+ @Unsigned Integer uI;
+
+ @Signed long sl;
+ @Unsigned long ul;
+ @Signed Long sL;
+ @Unsigned Long uL;
+
+ void assignmentsByte() {
+ @Signed byte i1 = sb;
+ @Unsigned byte i2 = ub;
+ @Signed byte i3 = sB;
+ @Unsigned byte i4 = uB;
+
+ @Signed Byte i91 = sb;
+ @Unsigned Byte i92 = ub;
+ @Signed Byte i93 = sB;
+ @Unsigned Byte i94 = uB;
+ }
+
+ void assignmentsShort() {
+ @SignedPositive short i1 = sb;
+ @SignedPositive short i2 = ub;
+ @SignedPositive short i3 = sB;
+ @SignedPositive short i4 = uB;
+
+ @Signed short i9 = ss;
+ @Unsigned short i10 = us;
+ @Signed short i11 = sS;
+ @Unsigned short i12 = uS;
+
+ @Signed Short i91 = ss;
+ @Unsigned Short i92 = us;
+ @Signed Short i93 = sS;
+ @Unsigned Short i94 = uS;
+ }
+
+ void assignmentsChar() {
+ // These are commented out because they are Java errors.
+ // @Unsigned char i2 = ub;
+ // @Unsigned char i4 = uB;
+ // @Unsigned char i10 = us;
+ // @Unsigned char i12 = uS;
+ }
+
+ void assignmentsInt() {
+ @SignedPositive int i1 = sb;
+ @SignedPositive int i2 = ub;
+ @SignedPositive int i3 = sB;
+ @SignedPositive int i4 = uB;
+
+ @SignedPositive int i6 = uc;
+ @SignedPositive int i8 = uC;
+
+ @SignedPositive int i9 = ss;
+ @SignedPositive int i10 = us;
+ @SignedPositive int i11 = sS;
+ @SignedPositive int i12 = uS;
+
+ @Signed int i13 = si;
+ @Unsigned int i14 = ui;
+ @Signed int i15 = sI;
+ @Unsigned int i16 = uI;
+
+ @Signed Integer i91 = si;
+ @Unsigned Integer i92 = ui;
+ @Signed Integer i93 = sI;
+ @Unsigned Integer i94 = uI;
+ }
+
+ void assignmentsLong() {
+ @SignedPositive long i1 = sb;
+ @SignedPositive long i2 = ub;
+ @SignedPositive long i3 = sB;
+ @SignedPositive long i4 = uB;
+
+ @SignedPositive long i6 = uc;
+ @SignedPositive long i8 = uC;
+
+ @SignedPositive long i9 = ss;
+ @SignedPositive long i10 = us;
+ @SignedPositive long i11 = sS;
+ @SignedPositive long i12 = uS;
+
+ @SignedPositive long i13 = si;
+ @SignedPositive long i14 = ui;
+ @SignedPositive long i15 = sI;
+ @SignedPositive long i16 = uI;
+
+ @Signed long i17 = sl;
+ @Unsigned long i18 = ul;
+ @Signed long i19 = sL;
+ @Unsigned long i20 = uL;
+
+ @Signed Long i91 = sl;
+ @Unsigned Long i92 = ul;
+ @Signed Long i93 = sL;
+ @Unsigned Long i94 = uL;
+ }
+}
diff --git a/checker/tests/signedness/ValueIntegration.java b/checker/tests/signedness/ValueIntegration.java
index 83a194ba8f8..ae4ecc860d7 100644
--- a/checker/tests/signedness/ValueIntegration.java
+++ b/checker/tests/signedness/ValueIntegration.java
@@ -53,6 +53,8 @@ public void ByteValRules(
ptest = bmixed;
}
+ // Character and char are always @Unsigned, never @Signed.
+ /*
public void CharValRules(
@IntVal({0, 127}) char c,
@IntVal({128, 255}) char upure,
@@ -69,35 +71,36 @@ public void CharValRules(
ptest = c;
stest = upure;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
gtest = upure;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
ptest = upure;
stest = umixed;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
gtest = umixed;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
ptest = umixed;
stest = spure;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
gtest = spure;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
ptest = spure;
stest = smixed;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
gtest = smixed;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
ptest = smixed;
stest = bmixed;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
gtest = bmixed;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
ptest = bmixed;
}
+ */
public void ShortValRules(
@IntVal({0, 32767}) short c,
@@ -279,6 +282,8 @@ public void ByteRangeRules(
ptest = bmixed;
}
+ // Character and char are always @Unsigned, never @Signed.
+ /*
public void CharRangeRules(
@IntRange(from = 0, to = 127) char c,
@NonNegative char nnc,
@@ -305,35 +310,36 @@ public void CharRangeRules(
ptest = pc;
stest = upure;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
gtest = upure;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
ptest = upure;
stest = umixed;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
gtest = umixed;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
ptest = umixed;
stest = spure;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
gtest = spure;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
ptest = spure;
stest = smixed;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
gtest = smixed;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
ptest = smixed;
stest = bmixed;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
gtest = bmixed;
- // :: error: (assignment.type.incompatible)
+ // XX error: (assignment.type.incompatible)
ptest = bmixed;
}
+ */
public void ShortRangeRules(
@IntRange(from = 0, to = 32767) short c,
diff --git a/checker/tests/tainting/HasQualParamDefaults.java b/checker/tests/tainting/HasQualParamDefaults.java
index e568139cac5..fa2cb03983f 100644
--- a/checker/tests/tainting/HasQualParamDefaults.java
+++ b/checker/tests/tainting/HasQualParamDefaults.java
@@ -44,6 +44,31 @@ public Buffer append(@PolyTainted String s) {
someString = s;
return s;
}
+
+ void initializeLocalTainted(@Tainted Buffer b) {
+ Buffer local = b;
+ @Tainted Buffer copy1 = local;
+ // :: error: (assignment.type.incompatible)
+ @Untainted Buffer copy2 = local;
+ }
+
+ void initializeLocalUntainted(@Untainted Buffer b) {
+ Buffer local = b;
+ @Untainted Buffer copy1 = local;
+ // :: error: (assignment.type.incompatible)
+ @Tainted Buffer copy2 = local;
+ }
+
+ void initializeLocalPolyTainted(@PolyTainted Buffer b) {
+ Buffer local = b;
+ @PolyTainted Buffer copy = local;
+ }
+
+ void noInitializer(@Untainted Buffer b) {
+ Buffer local;
+ // :: error: (assignment.type.incompatible)
+ local = b;
+ }
}
class Use {
@@ -83,4 +108,49 @@ void creation() {
@PolyTainted Buffer b3 = new @PolyTainted Buffer();
}
}
+
+ // For classes with @HasQualifierParameter, different defaulting rules are applied on that type
+ // inside the class body and outside the class body, so local variables need to be tested
+ // outside the class as well.
+ class LocalVars {
+ void initializeLocalTainted(@Tainted Buffer b) {
+ Buffer local = b;
+ @Tainted Buffer copy1 = local;
+ // :: error: (assignment.type.incompatible)
+ @Untainted Buffer copy2 = local;
+ }
+
+ void initializeLocalUntainted(@Untainted Buffer b) {
+ Buffer local = b;
+ @Untainted Buffer copy1 = local;
+ // :: error: (assignment.type.incompatible)
+ @Tainted Buffer copy2 = local;
+ }
+
+ void initializeLocalPolyTainted(@PolyTainted Buffer b) {
+ Buffer local = b;
+ @PolyTainted Buffer copy = local;
+ }
+
+ void noInitializer(@Untainted Buffer b) {
+ Buffer local;
+ // :: error: (assignment.type.incompatible)
+ local = b;
+ }
+
+ // These next two cases test circular dependencies. Calculating the type of a local variable
+ // looks at the type of initializer, but if the type of the initializer depends on the type
+ // of the variable, then infinite recursion could occur.
+
+ void testTypeVariableInference() {
+ GenericWithQualParam set = new GenericWithQualParam<>();
+ }
+
+ void testVariableInOwnInitializer() {
+ Buffer b = (b = null);
+ }
+ }
+
+ @HasQualifierParameter(Tainted.class)
+ static class GenericWithQualParam {}
}
diff --git a/checker/tests/tainting/InitializerDataflow.java b/checker/tests/tainting/InitializerDataflow.java
new file mode 100644
index 00000000000..73d1f484e98
--- /dev/null
+++ b/checker/tests/tainting/InitializerDataflow.java
@@ -0,0 +1,23 @@
+import org.checkerframework.checker.tainting.qual.PolyTainted;
+import org.checkerframework.checker.tainting.qual.Tainted;
+import org.checkerframework.checker.tainting.qual.Untainted;
+import org.checkerframework.framework.qual.HasQualifierParameter;
+
+public class InitializerDataflow {
+ @HasQualifierParameter(Tainted.class)
+ static class Buffer {}
+
+ @PolyTainted Buffer id(@PolyTainted String s) {
+ return null;
+ }
+
+ void methodBuffer(@Untainted String s) {
+ Buffer b1 = id(s);
+
+ String local = s;
+ Buffer b2 = id(local);
+
+ @Untainted String local2 = s;
+ Buffer b3 = id(local2);
+ }
+}
diff --git a/dataflow/build.gradle b/dataflow/build.gradle
index b8d6545b63c..4d54727f3fa 100644
--- a/dataflow/build.gradle
+++ b/dataflow/build.gradle
@@ -48,7 +48,7 @@ task liveVariableTest(dependsOn: compileTestJava, group: 'Verification') {
if (!JavaVersion.current().java9Compatible) {
jvmArgs += "-Xbootclasspath/p:${configurations.javacJar.asPath}"
}
- classpath = sourceSets.test.compileClasspath
+ classpath = sourceSets.test.runtimeClasspath
classpath += sourceSets.test.output
main = 'livevar.LiveVariable'
}
@@ -59,3 +59,22 @@ task liveVariableTest(dependsOn: compileTestJava, group: 'Verification') {
}
}
}
+
+task issue3447Test(dependsOn: compileTestJava, group: 'Verification') {
+ description 'Test issue 3447 test case for backward analysis.'
+ inputs.file('tests/issue3447/Test.java')
+ delete('tests/issue3447/Out.txt')
+ delete('tests/issue3447/Test.class')
+ doLast {
+ javaexec {
+ workingDir = 'tests/issue3447'
+ if (!JavaVersion.current().java9Compatible) {
+ jvmArgs += "-Xbootclasspath/p:${configurations.javacJar.asPath}"
+ }
+ classpath = sourceSets.test.runtimeClasspath
+ classpath += sourceSets.test.output
+
+ main = 'livevar.LiveVariable'
+ }
+ }
+}
diff --git a/dataflow/manual/Makefile b/dataflow/manual/Makefile
index 5177f8006dc..149fe75b639 100644
--- a/dataflow/manual/Makefile
+++ b/dataflow/manual/Makefile
@@ -1,4 +1,4 @@
-dataflow.pdf: dataflow.tex content.tex
+dataflow.pdf: dataflow.tex content.tex examples
pdflatex dataflow
pdflatex dataflow
diff --git a/dataflow/manual/content.tex b/dataflow/manual/content.tex
index 68fbb53b732..e743f9939b4 100644
--- a/dataflow/manual/content.tex
+++ b/dataflow/manual/content.tex
@@ -8,33 +8,17 @@ \section{Introduction}
\href{https://github.com/uber/NullAway}{NullAway}, and other contexts.
The primary purpose of the Dataflow Framework is to estimate values:
-that is, to determine that, on a particular line of source code, what
-values a variable might contain. This can also determine that a variable
-has a more precise type than its declared type. This enables
-flow-sensitive type checking in the Checker Framework, which
-reduces the burden of annotating a program. The Dataflow Framework was
-designed with several goals in mind. First, to encourage other uses
-of the framework, it is written as a separate package that can be
-built and used with no dependence on the Checker Framework. Second,
-the framework is currently intended to support analysis but not
-transformation, so it provides information that can be used by a type
-checker or an IDE, but it does not support optimization. Third, the
-framework aims to minimize the burden on developers who build on top
-of it. In particular, the hierarchy of analysis classes is designed
-to reduce the effort required to implement a new flow-sensitive type
-checker in the Checker Framework. The
-\href{https://docs.google.com/document/d/1oYzbOrrS4ZEEx4wQgIHbijNzcI5CiQAq_-1NrOS8JME/edit?usp=sharing}{Dataflow User's Guide}
-gives an introduction to customizing dataflow to add checker specific
-enhancements.
+for each line of source code, it determines what
+values each variable might contain.
The Dataflow Framework's result (\autoref{sec:analysis_result_class})
is an abstract value for each expression (an estimate of the
expression's run-time value) and a store at each program point. A
-store maps variables and other distinguished expressions to abstract
-values. As a pre-pass, the Dataflow Framework transforming an input
+store maps variables and other expressions to abstract
+values. As a pre-pass, the Dataflow Framework transforms an input
AST into a control flow graph (\autoref{sec:cfg}) consisting of basic
-blocks made up of nodes representing single operations. To produce
-its output, the Checker Framework performs iterative data flow
+blocks made up of nodes representing single operations. An analysis
+performs iterative data flow
analysis over the control flow graph. The effect of a single node on
the dataflow store is represented by a transfer function, which takes
an input store and a node and produces an output store. Once the
@@ -42,10 +26,25 @@ \section{Introduction}
code.
In the Checker Framework, the abstract values to be computed are
-annotated types. An individual checkers can customize its analysis by
+annotated types. An individual checker can customize its analysis by
extending the abstract value class and by overriding the behavior of
the transfer function for particular node types.
+The Dataflow Framework was
+designed with several goals in mind. First, to encourage use
+beyond the Checker Framework, it is written as a separate package that can be
+built and used with no dependence on the Checker Framework. Second,
+the framework supports analysis but not
+transformation, so it provides information that can be used by a type
+checker or an IDE, but it does not support optimization. Third, the
+framework aims to minimize the burden on developers who build on top
+of it. In particular, the hierarchy of analysis classes is designed
+to reduce the effort required to implement a new flow-sensitive type
+checker in the Checker Framework. The
+\href{https://docs.google.com/document/d/1oYzbOrrS4ZEEx4wQgIHbijNzcI5CiQAq_-1NrOS8JME/edit?usp=sharing}{Dataflow User's Guide}
+gives an introduction to customizing dataflow to add checker-specific
+enhancements.
+
\begin{workinprogress}
Paragraphs colored in gray with a gray bar on the left side (just
like this one) contain questions, additional comments or indicate
@@ -62,9 +61,10 @@ \subsection{Projects}
% TODO: Update
The source code of the combined Checker Framework and Dataflow
-Framework is divided into five projects: \code{javacutil},
-\code{dataflow}, \code{stubparser}, \code{framework}, and \code{checker},
-which can be built into distinct jar files.
+Framework is divided into multiple projects: \code{javacutil},
+\code{dataflow}, \code{framework}, and \code{checker},
+which can be built into distinct jar files. \code{checker.jar} is a fat
+jar that contains all of these, plus the Stub Parser.
\code{javacutil} provides convenient interfaces to routines in
Oracle's javac library. There are utility classes for interacting
@@ -84,18 +84,13 @@ \subsection{Projects}
control flow graphs and the base classes required for flow analysis.
These classes are described in detail in \autoref{sec:node_classes}.
-\code{stubparser} contains the stub-file parsing project.
-
\code{framework} contains the framework aspects of the Checker
Framework, including the derived classes for flow analysis of
annotated types which are described later in this document.
\code{checker} contains the type system-specific checkers.
-The \code{dataflow} project depends on \code{javacutil}, the
-\code{framework} project depends on both \code{dataflow} and
-\code{javacutil}, \code{stubparser} has no dependencies, and
-\code{checker} depends on \code{framework} and \code{stubparser}.
+The \code{dataflow} project depends only on \code{javacutil}.
\subsection{Classes}
@@ -111,12 +106,14 @@ \subsection{Classes}
\subsubsection{Nodes}
\label{sec:node_classes}
-Dataflow doesn't actually work on trees; it works on Nodes. Nodes
-simplify writing a dataflow analysis by separating the dataflow
-analysis from the original source code.
+Dataflow doesn't actually work on trees; it works on Nodes.
A Node class represents an individual operation of a program,
including arithmetic operations, logical operations, method calls,
-variable references, array accesses, etc. \autoref{tab:nodes} lists
+variable references, array accesses, etc.
+Nodes
+simplify writing a dataflow analysis by separating the dataflow
+analysis from the original source code.
+\autoref{tab:nodes} on page~\pageref{tab:nodes} lists
the Node types.
\begin{verbatim}
@@ -130,9 +127,8 @@ \subsubsection{Nodes}
\subsubsection{Blocks}
\label{sec:block_classes}
-Nodes are grouped into basic blocks using a hierarchy of Block
-classes. The hierarchy is composed of five interfaces, two abstract
-classes, and four concrete classes.
+The Block
+classes represent basic blocks.
\begin{verbatim}
package org.checkerframework.dataflow.cfg.block;
@@ -415,7 +411,7 @@ \subsubsubsection{TransferFunction}
\end{verbatim}
The Regex Checker's transfer function overrides visitMethodInvocation
-to special case isRegex and asRegex methods.
+to special-case the \code{isRegex} and \code{asRegex} methods.
\begin{verbatim}
package org.checkerframework.checker.regex;
@@ -533,37 +529,31 @@ \subsubsection{AnnotatedTypeFactory}
\end{verbatim}
-\begin{workinprogress}
-We should investigate whether we can optimize CFG generation for
-aggregate and compound checkers.
-\end{workinprogress}
-
-
\section{The Control-Flow Graph}
\label{sec:cfg}
-%In this section, we describe the control-flow graph (CFG), and the
-%translation from the Java abstract syntax tree (AST) to the CFG.
-
-This section describes the control-flow graph (CFG), which is used to
-represent a single method or field initialization, and the translation
-from the abstract syntax tree (AST) to the CFG\@. (The Dataflow
-Framework described here is designed to perform an intra-procedural
+A control-flow graph (CFG) represents a single method or field
+initialization. (The Dataflow Framework performs an intra-procedural
analysis. This analysis is modular and every method is considered in
-isolation.) We start with a simple example, then give a more formal
+isolation.)
+This section also describes the translation from the abstract syntax tree
+(AST) to the CFG\@.
+We start with a simple example, then give a more formal
definition of the CFG and its properties, and finally describe the
translation from the AST to the CFG.
-As is standard, a control-flow graph in the framework is a set of
+As is standard, a control-flow graph is a set of
basic blocks that are linked by control-flow edges. Possibly less
standard, every basic block consists of a sequence of so-called nodes,
-which correspond to a minimal Java operation or expression.
+each of which represents a minimal Java operation or expression.
-\flow{Simple}{A simple Java code snippet to introduce the CFG.}
+\flow{CFGSimple}{.33}{1.1}{A simple Java code snippet to introduce the CFG.
+In CFG visualizations, special basic blocks are shown as ovals;
+conditional basic blocks are polygons with eight sides; and regular and exception
+basic blocks are rectangles.}
-Consider the method \code{test} of \autoref{lst:CFGSimple} whose
-control-flow graph is shown in \autoref{fig:CFGSimple}. The if
+Consider the method \code{test} of \autoref{fig:CFGSimple}. The if
conditional got translated to a \emph{conditional basic block}
(octagon) with two successors. There are also two special basic blocks
(ovals) to denote the entry and exit point of the method.
@@ -610,29 +600,24 @@ \subsection{Formal Definition of the Control-Flow Graph}
point of the method and thus is the only basic block
without predecessors.
\item Exit block. This basic block denotes the (normal)
- exit of a method, and it does not have successors.
+ exit of a method, and it has no successors.
\item Exceptional exit block, which indicates exceptional
termination of the method. As an exit block, this block
- does not have successors.
+ has no successors.
\end{itemize}
Every method has exactly one entry block, zero or one exit blocks,
- and zero or one exceptional exit blocks. However, there is
- either an exit block or an exceptional exit block.
- \begin{workinprogress}
- Is this an exclusive or? Or can a method have both a regular
- exit block and an exceptional exit block? I think the latter
- is true.
- \end{workinprogress}
+ and zero or one exceptional exit blocks. There is always
+ either an exit block, an exceptional exit block, or both.
\item \textbf{Exception basic block.} An \emph{exception basic
block} contains exactly one node that \emph{might} throw an
exception at runtime (e.g., a method call). There are zero
- or one non-exceptional successors, and one or more
- exceptional successors (see \autoref{def:edges}). But in all
- cases there is at least one successor (regular or
- exceptional), and only a basic block containing a
+ or one non-exceptional successors (only a basic block containing a
\code{throw} statement does not have a non-exceptional
- successor.
+ successor). There are one or more
+ exceptional successors (see \autoref{def:edges}). In all
+ cases there is at least one successor (regular or
+ exceptional).
\item \textbf{Conditional basic block.} A \emph{conditional
basic block} does not contain any nodes and is used as a
@@ -653,23 +638,18 @@ \subsection{Formal Definition of the Control-Flow Graph}
The Java implementation of the four block types above is described in
\autoref{sec:block_classes}.
-In the visualizations used in this document (e.g., in
-\autoref{fig:CFGSimple}), special basic blocks are shown as ovals,
-conditional basic blocks are polygons with eight sides, and any other
-basic block appears as a rectangle.
-
\begin{definition}[Control-Flow Graph Edges]
\label{def:edges}
The basic blocks of a control-flow graph are connected by directed
\emph{edges}. If $b_1$ and $b_2$ are connected by a directed edge
-$(b_1,b_2)$, we call $b_1$ the predecessor of $b_2$, and we call $b_2$
-the successor of $b_1$. In a control-flow graph, there are three
+$(b_1,b_2)$, we call $b_1$ a predecessor of $b_2$, and we call $b_2$
+a successor of $b_1$. In a control-flow graph, there are three
types of edges:
\begin{enumerate}
\item \textbf{Exceptional edges}. An \emph{exceptional edge}
connects an exception basic block with its exceptional
successors, and it is labeled by the most general exception that
- might cause execution to take this edge during runtime. Note
+ might cause execution to take this edge during run time. Note
that the outgoing exceptional edges of a basic block do not need
to have mutually exclusive labels; the semantics is that the
control flow follows the most specific edge. For instance, if
@@ -707,7 +687,7 @@ \subsection{Formal Definition of the Control-Flow Graph}
A \emph{node} is a minimal Java operation or expression. It is
minimal in the sense that it cannot be decomposed further into
subparts between which control flow occurs. Examples for such
- nodes include integer literals, an addition node (that performs
+ nodes include integer literals, an addition node (which performs
the mathematical addition of two nodes) or a method call. Control
flow such as \code{if} and \code{break} are not represented as
nodes. The full list of nodes is given in \autoref{tab:nodes} and
@@ -865,7 +845,7 @@ \subsection{Formal Definition of the Control-Flow Graph}
\label{tab:nodes}
\end{longtable}
-\autoref{tab:nodesWithException} shows all node types which can possibly throw
+\autoref{tab:nodesWithException} shows all node types that can possibly throw
an exception and the exception type to be thrown.
Java class name of nodes are simplified as with \autoref{tab:nodes}.
All exception types in \autoref{tab:nodesWithException} are in package \code{java.lang}.
@@ -876,14 +856,10 @@ \subsection{Formal Definition of the Control-Flow Graph}
it's not recommended to catch it due to a critical situation which is not
to able to execute JVM and handle in an application.
- \begin{longtable}{lp{0.6\linewidth}l}
- \midrule
- \multicolumn{2}{c}{\autoref{tab:nodesWithException}: All node types could throw Exception and types to be thrown.} \\ \\
- \textbf{Node type} & \textbf{Exception type} \\ \midrule \endfirsthead
-
- \textbf{Node type} & \textbf{Exception type} \\ \midrule \endhead
- \hline \multicolumn{2}{|c|}{{Continued on next page}} \\ \hline \endfoot
- \endlastfoot
+\begin{table}
+ \begin{tabular}{ll}
+ \hline
+ \textbf{Node type} & \textbf{Exception type} \\ \hline
\code{ArrayAccess} & \code{NullPointerException}, \code{ArrayIndexOutOfBoundsException} \\
\code{FieldAccess} & \code{NullPointerException} \\
@@ -895,11 +871,12 @@ \subsection{Formal Definition of the Control-Flow Graph}
\code{TypeCast} & \code{ClassCastException} \\
\code{Throw} & Type of \code{e} when \code{throw e} \\
\code{AssertionError} & \code{AssertionError} \\
- \midrule
+ \hline
+ \end{tabular}
- \caption{All node types could throw Exception and types to be thrown.}
+ \caption{All node types that could throw Exception, and the types to be thrown.}
\label{tab:nodesWithException}
- \end{longtable}
+\end{table}
\begin{workinprogress}
ThisLiteral shouldn't be considered a literal value node, because a use of
@@ -951,15 +928,15 @@ \subsubsection{Program Structure}
\label{sec:prog-structure}
Java programs are structured using high-level programming constructs
-such as different variants of loops, if-then-else constructs,
+such as loops, if-then-else constructs,
try-catch-finally blocks or switch statements. During the translation
from the AST to the CFG some of this program structure is lost and all
non-sequential control flow is represented by two low-level
constructs: conditional basic blocks and control-flow edges between
basic blocks. For instance, a \code{while} loop is translated into its
condition followed by a conditional basic block that models the two
-possible outcomes of the condition: either, the control flow follows
-the `true' branch and continues with the loops body, or goes to the
+possible outcomes of the condition: either the control flow follows
+the `true' branch and continues with the loop's body, or control goes to the
`false' successor and executes the first statement after the loop.
@@ -970,35 +947,35 @@ \subsubsection{Assignment}
be evaluated even if the left-hand side of the assignment causes an
exception. This semantics is faithfully represented in the CFG
produced by the translation. An example of a field assignment
-exhibiting this behavior is shown in \autoref{lst:CFGFieldAssignment}.
+exhibiting this behavior is shown in \autoref{fig:CFGFieldAssignment}.
-\flow{FieldAssignment}{Control flow for a field assignment is not strictly
+\flow{CFGFieldAssignment}{.33}{1}{Control flow for a field assignment is not strictly
left-to-right (cf.\ \jlsref{15.26.1}),
which is properly handled by the translation.}
\subsubsection{Postfix/Prefix Increment/Decrement}
\label{sec:postpre-incdec}
-Both of postfix and prefix increment or decrement have a side effect to
-update the variable or field. To represent this side effect, Dataflow
-Framework create an artificial assignment node like \code{n = n + 1}
+Postfix and prefix increment and decrement have a side effect to
+update the variable or field. To represent this side effect, the Dataflow
+Framework creates an artificial assignment node like \code{n = n + 1}
for \code{++n} or \code{n++}. This artificial assignment node is stored
in \code{unaryAssignNodeLookup} of \code{ControlFlowGraph}. The assignment
node is also stored in \code{treeLookup} for prefix increment or decrement
so that the result of it is after the assignment. However, the node before
the assignment is stored in \code{treeLookup} for postfix increment or decrement
because the result of it should be before the assignment. For further information
-about node-tree mapping, see \autoref{sec:conversions} also.
+about node-tree mapping, see \autoref{sec:conversions}.
\subsubsection{Conditional stores}
\label{sec:cond-stores}
The Dataflow Framework extracts information from control-flow splits
-that occur in if, for, while, and switch statements. In order to have
+that occur in \code{if}, \code{for}, \code{while}, and \code{switch} statements. In order to have
the information available at the split, we eagerly produce two stores
contained in a \code{ConditionalTransferResult} after certain
boolean-valued expressions. The stores are called the \emph{then} and
\emph{else} stores. So, for example, after the expression \code{x ==
- null}, two different stores will be created. The Nullness Checkers
+ null}, two different stores will be created. The Nullness Checker
would produce a then store that maps \code{x} to @Nullable and an else
store that maps \code{x} to @NonNull.
@@ -1023,7 +1000,7 @@ \subsubsection{Branches}
successor.
Consider the control flow graph generated for the simple if statement
-in \autoref{lst:CFGIfStatement}. The conditional expression \code{b1}
+in \autoref{fig:CFGIfStatement}. The conditional expression \code{b1}
immediately precedes the \code{ConditionalBlock}, represented by the
octagonal node. The \code{ConditionalBlock} is followed by both a
then and an else successor block, after which control flow merges back
@@ -1036,7 +1013,7 @@ \subsubsection{Branches}
More precise rules are used to preserve dataflow information for
short-circuiting expressions, as described in \autoref{sec:cond-exp}.
-\flow{IfStatement}{Example of an if statement translated into a
+\flow{CFGIfStatement}{.33}{1.25}{Example of an if statement translated into a
\code{ConditionalBlock}.}
\subsubsection{Conditional Expressions}
@@ -1051,7 +1028,7 @@ \subsubsection{Conditional Expressions}
additional dataflow information.
An example program using conditional or is shown in
-\autoref{lst:CFGConditionalOr}. Note that the CFG correctly
+\autoref{fig:CFGConditionalOr}. Note that the CFG correctly
represents short-circuiting. The expression \code{b2 || b3} is only
executed if \code{b1} is false and \code{b3} is only evaluated if
\code{b1} and \code{b2} are false.
@@ -1075,7 +1052,7 @@ \subsubsection{Conditional Expressions}
along those edges need to be kept in the else store of the block
containing \code{b1 || (b2 || b3)}.
-\flow{ConditionalOr}{Example of a conditional or expression
+\flow{CFGConditionalOr}{.33}{1.33}{Example of a conditional or expression
(\code{||}) with short-circuiting and more precise flow rules.}
@@ -1086,12 +1063,7 @@ \subsubsection{Implicit \code{this} access}
left out). To relieve the user of the Dataflow Framework from
manually determining the two cases, we consistently use
\code{FieldAccessNode} for field accesses, where the receiver might be
-an \code{ImplicitThisNode}. For instance, this is shown in the
-earlier example \autoref{lst:CFGFieldAssignment}.
-
-\begin{workinprogress}
-I don't see a \code{implicitThisNode} in \autoref{lst:CFGFieldAssignment}.
-\end{workinprogress}
+an \code{ImplicitThisNode}.
\subsubsection{Assert statements}
@@ -1105,20 +1077,18 @@ \subsubsection{Assert statements}
annotations. However, when assertions are disabled, it would be
unsound to assume that they had any effect on dataflow information.
-Our solution is to offer the user of the Dataflow Framework, and
-ultimately the user of the Checker Framework, the option of stating that
+The user of the Dataflow Framework may specify that
assertions are enabled or disabled. When assertions are assumed to be
-disabled, no CFG Nodes are built for the assert statement at all.
+disabled, no CFG Nodes are built for the assert statement.
When assertions are assumed to be enabled, CFG Nodes are built to
represent the condition of the assert statement and, in the else
successor of a ConditionalBlock, CFG Nodes are built to represent the
detail expression of the assert, if any.
-If assertions are not assumed to be enabled or disabled, then we
-generate a CFG that is conservative and represents the fact that the
+If assertions are not assumed to be enabled or disabled, then
+the CFG is conservative and represents the fact that the
assert statement may execute or may not. This takes the form of a
-ConditionalBlock that branches on a fake variable. For example, the
-code in \autoref{lst:CFGAssert} produces the control flow graph in
+ConditionalBlock that branches on a fake variable. For example, see
\autoref{fig:CFGAssert}. The fake variable named
\code{assertionsEnabled#num0} controls the first ConditionalBlock.
The then successor of the ConditionalBlock is the same subgraph of CFG
@@ -1127,19 +1097,10 @@ \subsubsection{Assert statements}
subgraph of CFG Nodes that would be created if assertions were assumed
to be disabled.
-\flow{Assert}{Example of an assert statement translated with
+\flow{CFGAssert}{.15}{2.9}{Example of an assert statement translated with
assertions neither assumed to be enabled nor assumed to be
disabled.}
-\begin{workinprogress}
-How should the user choose between the three possibilities?
-\end{workinprogress}
-
-\begin{workinprogress}
-Why are there two basic blocks for the \code{AssertionError} and then
-the \code{throw}? Why are they not in the same basic block, as there
-is no alternate control flow?
-\end{workinprogress}
\subsubsection{Varargs method invocation}
\label{sec:varargs}
@@ -1148,28 +1109,28 @@ \subsubsection{Varargs method invocation}
\code{m(1, 2, 3)} will be compiled as \code{m(new int[]\{1, 2, 3\})}
when the signature of \code{m} is \code{m(int... args)}. Dataflow
Framework creates an \code{ArrayCreationNode} with initializer for varargs
-in the same way as Java compiler. Note that it doesn't create an \code{ArrayCreationNode}
-when the varargs is an array which is same depth with the type of
-the formal parameter or \code{null} is given as actual varargs.
+in the same way as the Java compiler does.
+Note that it doesn't create an \code{ArrayCreationNode}
+when the varargs is an array with the same depth as the type of
+the formal parameter, or if \code{null} is given as the actual varargs argument.
\subsubsection{Default case and fall through for switch statement}
\label{sec:default-switch}
-Switch statement is handled as a chain of \code{CaseNode} and nodes in
+A switch statement is handled as a chain of \code{CaseNode} and nodes in
the case. \code{CaseNode} makes a branch by comparing the equality of
the expression of the switch statement and the expression of the case.
Note that the expression of a switch statement must be executed just only
-once at first of switch statement. To refer its value, a fake variable
+once at the beginning of the switch statement. To refer to its value, a fake variable
is created and it is assigned to a fake variable. \code{THEN_TO_BOTH}
edge goes to nodes in the case and \code{ELSE_TO_BOTH} edge goes to next
\code{CaseNode}. When a next is default case, it goes to nodes in the default
case. If a break statement is in nodes, it creates an edge to next node of
the switch statement. If there is any possibility of fall-through, an edge
to the first of nodes in the next case is created after nodes in the case.
-For example, the code in \autoref{lst:CFGSwitch} produces the control flow
-graph in \autoref{fig:CFGSwitch}. The fake variable named \code{switch#num0}
+For example, see \autoref{fig:CFGSwitch}. The fake variable named \code{switch#num0}
is created and each of case nodes creates the branches.
-\flow{Switch}{Example of a switch statement with case, default and fall through.}
+\flow{CFGSwitch}{.21}{1.45}{Example of a switch statement with case, default and fall through.}
\subsubsection{Handling \code{finally} blocks}
\label{sec:try-finally}
@@ -1196,12 +1157,7 @@ \subsection{AST to CFG Translation}
\begin{itemize}
\item \textbf{Simple extended node.} An extended node can just be a
wrapper for a node that does not throw an exception,
- as defined in Definition~\ref{def:node}.
- \begin{workinprogress}
- Say how non-exception-throwing nodes are distinguished in
- Table~\autoref{tab:nodes}. Exception-throwing ones need to
- include throw, call, field access, typecast, division, ...
- \end{workinprogress}
+ as defined in Definition~\ref{def:node}.
\item \textbf{Exception extended node.} Similar to a simple
node, an exception extended node contains a node, but this
node might throw an exception at runtime.
@@ -1417,11 +1373,7 @@ \subsubsection{Conversions and node-tree mapping}
\section{Dataflow Analysis}
This section describes how the dataflow analysis over the control-flow
-graph is performed and what the user of the framework has to implement
-to define a particular analysis.
-
-
-\subsection{Overview}
+graph is performed and how to implement a particular analysis.
Roughly, a dataflow analysis in the framework works as follows. Given
the abstract syntax tree of a method, the framework computes the
@@ -1432,49 +1384,17 @@ \subsection{Overview}
functions are specific to the particular analysis and are used to
approximate the runtime behavior of different statements and expressions.
-An analysis result contains two parts:
-
-\begin{enumerate}
-\item
- A node-value mapping (\code{Analysis.nodeValues}) from node to
- abstract value. Only nodes that can take on an abstract value are
- used as keys. For example, in the Checker Framework, the mapping is
- from expression nodes to annotated types.
-
-\item
- A set of \emph{stores}. Each store maps a flow expression to an
- abstract value. Each store is associated with a specific program
- point. The framework keeps explicit stores for the start of each
- basic block (\code{Analysis.stores}) and computes the store for
- other program points on the fly.
-\end{enumerate}
-
-\begin{workinprogress}
-There needs to be a definition of ``program point''.
-\end{workinprogress}
-
-
-After an analysis has iterated to a fix-point, the computed dataflow
-information is maintained in an AnalysisResult, which can map either
-nodes or trees to abstract values.
-
-
-
\subsection{Managing Intermediate Results of the Analysis}
\label{sec:node-mapping}
\label{sec:store-management}
-\begin{workinprogress}
-This feels repetitive with the previous one. Combine them in whole
- or in part?
-\end{workinprogress}
Conceptually, the dataflow analysis computes an abstract value for
every node and flow expression\footnote{Certain dataflow analysis
might choose not to produce an abstract value for every node. For
instance, a constant propagation analysis would only be concerned
- with nodes of a numerical type, and ignore other nodes.}. The
+ with nodes of a numerical type, and could ignore other nodes.}. The
transfer function (\autoref{sec:transfer-fnc}) produces these abstract
values, taking as input the abstract values computed earlier for
sub-expressions. For instance, in a constant propagation analysis,
@@ -1483,18 +1403,25 @@ \subsection{Managing Intermediate Results of the Analysis}
\code{AdditionNode} is a constant if and only if both operands are
constant.
-There are two parts to the analysis result.
+An analysis result contains two parts:
\begin{enumerate}
\item
-The \emph{node-value mapping} maps \code{Node}s to their abstract
-values. The framework consciously does not store the abstract value
+The \emph{node-value mapping} (\code{Analysis.nodeValues}) maps \code{Node}s to their abstract
+values. Only nodes that can take on an abstract value are
+used as keys. For example, in the Checker Framework, the mapping is
+from expression nodes to annotated types.
+
+The framework consciously does not store the abstract value
directly in the node, to remove any coupling between the control-flow
graph and a particular analysis. This allows the control-flow graph
to be constructed only once, and then reused for different dataflow
analyses.
\item
+A set of \emph{stores}. Each store maps a flow expression to an
+abstract value. Each store is associated with a specific program point.
+
The stores tracked by an analysis implement the \code{Store}
interface, which defines the following operations:
\begin{itemize}
@@ -1519,14 +1446,18 @@ \subsection{Managing Intermediate Results of the Analysis}
\end{verbatim}
Every store is associated with a particular point in the control-flow
-graph, and all stores are managed by the framework. It maintains a
-single store for every basic block that represents the information
-available at the beginning of that block. When dataflow information
+graph, and all stores are managed by the framework. It saves an explicit store
+for the start of each basic block.
+When dataflow information
is requested for a later point in a block, the analysis applies the
-transfer function to compute it from the initial store.
+transfer function to recompute it from the initial store.
\end{enumerate}
+After an analysis has iterated to a fix-point, the computed dataflow
+information is maintained in an AnalysisResult, which can map either
+nodes or trees to abstract values.
+
\subsection{Answering Questions}
\label{sec:answering-questions}
@@ -1549,7 +1480,7 @@ \subsection{Answering Questions}
\end{itemize}
\end{enumerate}
-The store may first need to be computed, as the framework does not
+The store may first need to be (re-)computed, as the framework does not
store all intermediate stores but rather only those for key positions
as described in \autoref{sec:store-management}.
@@ -1573,28 +1504,25 @@ \subsection{Answering Questions}
\subsection{Transfer Function}
\label{sec:transfer-fnc}
-A transfer function has to provide the following:
-\begin{itemize}
-\item A method that returns the initial store for a method, given the
- list of arguments (as \code{LocalVariableNode}s) and the
- \code{MethodTree} (useful if the initial store depends on the method
- signature, for instance).
-
- \begin{workinprogress}
- Why are the arguments to the method call LocalVariableNodes? Or
- should this be parameters? Make clear whether this is about an
- invocation of a method or a method declaration.
- \end{workinprogress}
+A transfer function is an object that has a transfer method for
+every \code{Node} type, and also a transfer method for procedure entry.
-\item A transfer method for every \code{Node} type that takes a store
+\begin{itemize}
+\item A transfer method for a \code{Node} type takes a store
and the node, and produces an updated store. This is achieved by
implementing the \code{NodeVisitor} interface for the store
type \code{S}.
-These transfer methods also get access to the abstract value of any
-sub-node of the node \code n under consideration. This is not limited
-to immediate children, but the abstract value for any node contained
-in \code n can be queried.
+ These transfer methods also get access to the abstract value of any
+ sub-node of the node \code n under consideration. This is not limited
+ to immediate children, but the abstract value for any node contained
+ in \code n can be queried.
+
+\item A transfer method for procedure entry returns the initial store, given the
+ list of parameters (as \code{LocalVariableNode}s that represent the formal
+ parameters) and the
+ \code{MethodTree} (useful if the initial store depends on the procedure
+ signature, for instance).
\end{itemize}
@@ -1654,10 +1582,7 @@ \subsection{Flow Rules}
else store of its successor by not propagating information to the else
store which might conflict with information already there, and
conversely for \code{ELSE_TO_ELSE}.
-
-\begin{workinprogress}
-What happens to the other store in these operations?
-\end{workinprogress}
+See \autoref{sec:cond-exp} for more details and an example.
Currently, we only use flow rules for short-circuiting edges of
conditional ands and ors. The CFG builder sets the flow rule of each
@@ -1669,10 +1594,6 @@ \subsection{Flow Rules}
analyzed, so it is a requirement that at least one predecessor block
writes the then store and at least one writes the else store.
-\begin{workinprogress}
-How are these flow rules attached/changed?
-\end{workinprogress}
-
\subsection{Concurrency}
@@ -1691,10 +1612,6 @@ \subsection{Concurrency}
behaves monotonically, however it is not yet used to preserve dataflow
information about fields under concurrent semantics.
-\begin{workinprogress}
-Do we have an issue filed for the last point above?
-\end{workinprogress}
-
\section{Example: Constant Propagation}
@@ -1734,12 +1651,12 @@ \section{Example: Constant Propagation}
function that considers the \code{EqualToNode}, and if it is of the
form \code{a == e} for a local variable \code{a} and constant
\code{e}, passes the correct information to one of the branches. This
-is also shown in the example of \autoref{fig:ConstSimple}.
+is also shown in \autoref{fig:ConstSimple}.
-\text{Example.} A small example is shown in \autoref{lst:ConstSimple}
-and \autoref{fig:ConstSimple}.
+\text{Example.} A small example is shown in \autoref{fig:ConstSimple}.
-\constantpropagation{Simple}{Simple sequential program to illustrate constant propagation.}
+\flow{ConstSimple}{.45}{1}{Simple sequential program to illustrate constant
+ propagation. Intermediate analysis results are shown.}
\section{Example: Live Variable}
@@ -1764,22 +1681,18 @@ \section{Example: Live Variable}
is a backward transfer function). The transfer function visits assignments to
update the information of live variables for each node in the stores.
-\textbf{Example.} An example is shown in \autoref{lst:LiveSimple} and
-\autoref{fig:LiveSimple}.
+\textbf{Example.} An example is shown in \autoref{fig:LiveSimple}.
-\livevariable{Simple}{Simple sequential program to illustrate live variable.}
+\flow{LiveSimple}{.33}{1}{Simple sequential program to illustrate live variable. Intermediate analysis results are shown.}
\section{Default Analysis}
-\begin{workinprogress}
-I feel like there is a missing cross-reference or two to this section.
-\end{workinprogress}
\subsection{Overview}
The default flow-sensitive analysis \code{org.checkerframework.framework.flow.CFAnalysis}
-works for the qualifier hierarchy of any checker defined in the
+works for any checker defined in the
Checker Framework. This generality is both a strength and a weakness
because the default analysis can always run but the facts it can
deduce are limited. The default analysis is extensible so checkers
diff --git a/dataflow/manual/dataflow.tex b/dataflow/manual/dataflow.tex
index eabb57691fe..26df71afaf8 100644
--- a/dataflow/manual/dataflow.tex
+++ b/dataflow/manual/dataflow.tex
@@ -50,6 +50,7 @@
numberstyle=\tiny,
stepnumber=1,
breaklines=true,
+ breakatwhitespace,
frame=lines,
showstringspaces=false,
tabsize=2,
@@ -87,28 +88,26 @@
\newtheorem{definition}{Definition}[section]
% control-flow graph images and listings
-\newcommand{\flowlst}[2]{\lstinputlisting[caption=#2,label=lst:#1,float]{examples/#1.java}}
-\newcommand{\flowimg}[2]{\begin{figure}
+% Arguments 2 and 3 control how much horizontal space the code takes on the page.
+\newcommand{\flow}[4]{
+\begin{figure}
+\centering\vspace{0pt}
+\begin{minipage}[t]{#2\textwidth}
+\centering\vspace{0pt}
+\begin{minipage}[t]{#3\textwidth}
+\lstinputlisting{examples/#1.java}
+\end{minipage}%
+\end{minipage}%
+\begin{minipage}[t]{.6\textwidth}
+\centering\vspace{0pt}
\includegraphics[scale=0.6]{examples/graphs/#1.pdf}
\centering
-\caption{#2}
+\end{minipage}
+\caption{#4}
\label{fig:#1}
\end{figure}}
-\newcommand{\flow}[2]{
- \flowlst{CFG#1}{{#2 Its CFG is depicted in \autoref{fig:CFG#1}.}}
- \flowimg{CFG#1}{The control-flow graph for \autoref{lst:CFG#1}.}
-}
-\newcommand{\constantpropagation}[2]{
- \flowlst{Const#1}{{#2 Its CFG and intermediate analysis results are depicted in \autoref{fig:Const#1}.}}
- \flowimg{Const#1}{The control-flow graph (including intermediate analysis results) for \autoref{lst:Const#1}.}
-}
-
-\newcommand{\livevariable}[2]{
-\flowlst{Live#1}{{#2 Its CFG and intermediate analysis results are depicted in \autoref{fig:Live#1}.}}
-\flowimg{Live#1}{The control-flow graph (including intermediate analysis results) for \autoref{lst:Live#1}.}
-}
-% references to the java specification
+% references to the Java Language Specification.
\newcommand{\jlsref}[1]{JLS~\textsection{}#1}
diff --git a/dataflow/manual/examples/CFGAssert.java b/dataflow/manual/examples/CFGAssert.java
index 5f5050357a1..1bc3eb59135 100644
--- a/dataflow/manual/examples/CFGAssert.java
+++ b/dataflow/manual/examples/CFGAssert.java
@@ -1,5 +1,6 @@
class Test {
- void testAssert(Object a) {
- assert a != null : "Argument is null";
- }
+ void testAssert(Object a) {
+ assert a != null
+ : "Argument is null";
+ }
}
diff --git a/dataflow/manual/examples/CFGConditionalOr.java b/dataflow/manual/examples/CFGConditionalOr.java
index 896cf44bce7..03e263a416f 100644
--- a/dataflow/manual/examples/CFGConditionalOr.java
+++ b/dataflow/manual/examples/CFGConditionalOr.java
@@ -1,8 +1,8 @@
class Test {
- void test(boolean b1, boolean b2, boolean b3) {
- int x = 0;
- if (b1 || (b2 || b3)) {
- x = 1;
- }
+ void test(boolean b1, boolean b2, boolean b3) {
+ int x = 0;
+ if (b1 || (b2 || b3)) {
+ x = 1;
}
+ }
}
diff --git a/dataflow/manual/examples/CFGConditionalOr2.java b/dataflow/manual/examples/CFGConditionalOr2.java
index 93bcf908b40..dc9b2855074 100644
--- a/dataflow/manual/examples/CFGConditionalOr2.java
+++ b/dataflow/manual/examples/CFGConditionalOr2.java
@@ -1,6 +1,6 @@
class Test {
- void test(boolean b1, boolean b2, boolean b3) {
- int x = 0;
- boolean b = b1 || (b2 || b3);
- }
+ void test(boolean b1, boolean b2, boolean b3) {
+ int x = 0;
+ boolean b = b1 || (b2 || b3);
+ }
}
diff --git a/dataflow/manual/examples/CFGFieldAssignment.java b/dataflow/manual/examples/CFGFieldAssignment.java
index 0bbecdddee1..898e1882072 100644
--- a/dataflow/manual/examples/CFGFieldAssignment.java
+++ b/dataflow/manual/examples/CFGFieldAssignment.java
@@ -1,7 +1,7 @@
class Test {
- int f;
+ int f;
- void test(Test x) {
- x.f = 1;
- }
+ void test(Test x) {
+ x.f = 1;
+ }
}
diff --git a/dataflow/manual/examples/CFGIfStatement.java b/dataflow/manual/examples/CFGIfStatement.java
index db83f01ef58..f4ffd99be40 100644
--- a/dataflow/manual/examples/CFGIfStatement.java
+++ b/dataflow/manual/examples/CFGIfStatement.java
@@ -1,10 +1,10 @@
class Test {
- void testIf(boolean b1) {
- int x = 0;
- if (b1) {
- x = 1;
- } else {
- x = 2;
- }
+ void testIf(boolean b1) {
+ int x = 0;
+ if (b1) {
+ x = 1;
+ } else {
+ x = 2;
}
+ }
}
diff --git a/dataflow/manual/examples/CFGSimple.java b/dataflow/manual/examples/CFGSimple.java
index 387ba72ce61..2aedb61de84 100644
--- a/dataflow/manual/examples/CFGSimple.java
+++ b/dataflow/manual/examples/CFGSimple.java
@@ -1,8 +1,8 @@
class Test {
- void test(boolean b) {
- int x = 2;
- if (b) {
- x = 1;
- }
+ void test(boolean b) {
+ int x = 2;
+ if (b) {
+ x = 1;
}
+ }
}
diff --git a/dataflow/manual/examples/CFGSwitch.java b/dataflow/manual/examples/CFGSwitch.java
index 91f2d95141c..ae8eea293ce 100644
--- a/dataflow/manual/examples/CFGSwitch.java
+++ b/dataflow/manual/examples/CFGSwitch.java
@@ -1,14 +1,14 @@
class Test {
- void test(int x) {
- switch (x) {
- case 1:
- int a = x;
- break;
- case 2:
- int b = x;
- default:
- int c = x;
- break;
- }
+ void test(int x) {
+ switch (x) {
+ case 1:
+ int a = x;
+ break;
+ case 2:
+ int b = x;
+ default:
+ int c = x;
+ break;
}
+ }
}
diff --git a/dataflow/manual/examples/ConstSimple.java b/dataflow/manual/examples/ConstSimple.java
index 144fe4cad35..150dfd20281 100644
--- a/dataflow/manual/examples/ConstSimple.java
+++ b/dataflow/manual/examples/ConstSimple.java
@@ -1,16 +1,16 @@
class Test {
- void test(boolean b, int a) {
- int x = 1;
- int y = 0;
- if (b) {
- x = 2;
- } else {
- x = 2;
- y = a;
- }
- x = 3;
- if (a == 2) {
- x = 4;
- }
+ void test(boolean b, int a) {
+ int x = 1;
+ int y = 0;
+ if (b) {
+ x = 2;
+ } else {
+ x = 2;
+ y = a;
}
+ x = 3;
+ if (a == 2) {
+ x = 4;
+ }
+ }
}
diff --git a/dataflow/manual/examples/LiveSimple.java b/dataflow/manual/examples/LiveSimple.java
index 891241c18fe..641ac2eb4fc 100644
--- a/dataflow/manual/examples/LiveSimple.java
+++ b/dataflow/manual/examples/LiveSimple.java
@@ -1,10 +1,10 @@
public class Test {
- public void test() {
- int a = 1, b = 2, c = 3;
- if (a > 0) {
- int d = a + c;
- } else {
- int e = a + b;
- }
+ public void test() {
+ int a = 1, b = 2, c = 3;
+ if (a > 0) {
+ int d = a + c;
+ } else {
+ int e = a + b;
}
+ }
}
diff --git a/dataflow/manual/examples/graphs/LiveSimple.pdf b/dataflow/manual/examples/graphs/LiveSimple.pdf
index 53f72a05274..a1e44e54efc 100644
Binary files a/dataflow/manual/examples/graphs/LiveSimple.pdf and b/dataflow/manual/examples/graphs/LiveSimple.pdf differ
diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java
index 36ee3346a60..74b1fda1087 100644
--- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java
+++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java
@@ -11,6 +11,8 @@
import java.util.PriorityQueue;
import java.util.Set;
import javax.lang.model.element.Element;
+import org.checkerframework.checker.interning.qual.FindDistinct;
+import org.checkerframework.checker.interning.qual.InternedDistinct;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
@@ -74,13 +76,13 @@ public abstract class AbstractAnalysis<
* !isRunning ==> (currentNode == null)
*
*/
- protected @Nullable Node currentNode;
+ protected @InternedDistinct @Nullable Node currentNode;
/**
* The tree that is currently being looked at. The transfer function can set this tree to make
* sure that calls to {@code getValue} will not return information for this given tree.
*/
- protected @Nullable Tree currentTree;
+ protected @InternedDistinct @Nullable Tree currentTree;
/** The current transfer input when the analysis is running. */
protected @Nullable TransferInput currentInput;
@@ -100,10 +102,19 @@ public abstract class AbstractAnalysis<
*
* @param currentTree the tree that should be currently looked at
*/
- public void setCurrentTree(Tree currentTree) {
+ public void setCurrentTree(@FindDistinct Tree currentTree) {
this.currentTree = currentTree;
}
+ /**
+ * Set the node that is currently being looked at.
+ *
+ * @param currentNode the node that should be currently looked at
+ */
+ protected void setCurrentNode(@FindDistinct @Nullable Node currentNode) {
+ this.currentNode = currentNode;
+ }
+
/**
* Implementation of common features for {@link BackwardAnalysisImpl} and {@link
* ForwardAnalysisImpl}.
@@ -150,7 +161,7 @@ public Direction getDirection() {
}
@Override
- @SuppressWarnings("contracts.precondition.override.invalid") // implementation field
+ @SuppressWarnings("nullness:contracts.precondition.override.invalid") // implementation field
@RequiresNonNull("cfg")
public AnalysisResult getResult() {
if (isRunning) {
@@ -213,7 +224,7 @@ public IdentityHashMap getNodeValues() {
}
@Override
- @SuppressWarnings("contracts.precondition.override.invalid") // implementation field
+ @SuppressWarnings("nullness:contracts.precondition.override.invalid") // implementation field
@RequiresNonNull("cfg")
public @Nullable S getRegularExitStore() {
SpecialBlock regularExitBlock = cfg.getRegularExitBlock();
@@ -225,7 +236,7 @@ public IdentityHashMap getNodeValues() {
}
@Override
- @SuppressWarnings("contracts.precondition.override.invalid") // implementation field
+ @SuppressWarnings("nullness:contracts.precondition.override.invalid") // implementation field
@RequiresNonNull("cfg")
public @Nullable S getExceptionalExitStore() {
SpecialBlock exceptionalExitBlock = cfg.getExceptionalExitBlock();
@@ -251,14 +262,7 @@ public IdentityHashMap getNodeValues() {
return cfg.getNodesCorrespondingToTree(t);
}
- /**
- * Return the abstract value for {@link Tree} {@code t}, or {@code null} if no information is
- * available. Note that if the analysis has not finished yet, this value might not represent the
- * final value for this node.
- *
- * @param t the given tree
- * @return the abstract value for the given tree
- */
+ @Override
public @Nullable V getValue(Tree t) {
// we don't have a org.checkerframework.dataflow fact about the current node yet
if (t == currentTree) {
@@ -328,9 +332,10 @@ protected TransferResult callTransferFunction(
return new RegularTransferResult<>(null, transferInput.getRegularStore());
}
transferInput.node = node;
- currentNode = node;
+ setCurrentNode(node);
+ @SuppressWarnings("nullness") // CF bug: "INFERENCE FAILED"
TransferResult transferResult = node.accept(transferFunction, transferInput);
- currentNode = null;
+ setCurrentNode(null);
if (node instanceof AssignmentNode) {
// store the flow-refined value effectively for final local variables
AssignmentNode assignment = (AssignmentNode) node;
@@ -432,7 +437,7 @@ protected static class Worklist {
* forward analysis.
*/
public class ForwardDFOComparator implements Comparator {
- @SuppressWarnings("unboxing.of.nullable")
+ @SuppressWarnings("nullness:unboxing.of.nullable")
@Override
public int compare(Block b1, Block b2) {
return depthFirstOrder.get(b1) - depthFirstOrder.get(b2);
@@ -444,7 +449,7 @@ public int compare(Block b1, Block b2) {
* backward analysis.
*/
public class BackwardDFOComparator implements Comparator {
- @SuppressWarnings("unboxing.of.nullable")
+ @SuppressWarnings("nullness:unboxing.of.nullable")
@Override
public int compare(Block b1, Block b2) {
return depthFirstOrder.get(b2) - depthFirstOrder.get(b1);
diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/Analysis.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/Analysis.java
index 476c61a75cd..13964b5235c 100644
--- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/Analysis.java
+++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/Analysis.java
@@ -1,5 +1,6 @@
package org.checkerframework.dataflow.analysis;
+import com.sun.source.tree.Tree;
import java.util.IdentityHashMap;
import java.util.Map;
import org.checkerframework.checker.nullness.qual.Nullable;
@@ -116,6 +117,16 @@ S runAnalysisFor(
*/
@Nullable V getValue(Node n);
+ /**
+ * Return the abstract value for {@link Tree} {@code t}, or {@code null} if no information is
+ * available. Note that if the analysis has not finished yet, this value might not represent the
+ * final value for this node.
+ *
+ * @param t the given tree
+ * @return the abstract value for the given tree
+ */
+ @Nullable V getValue(Tree t);
+
/**
* Returns the regular exit store, or {@code null}, if there is no such store (because the
* method cannot exit through the regular exit block).
diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/BackwardAnalysisImpl.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/BackwardAnalysisImpl.java
index 888b0a801d7..4c665047980 100644
--- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/BackwardAnalysisImpl.java
+++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/BackwardAnalysisImpl.java
@@ -4,13 +4,13 @@
import java.util.List;
import java.util.ListIterator;
import java.util.Map;
+import org.checkerframework.checker.interning.qual.FindDistinct;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;
import org.checkerframework.dataflow.analysis.Store.FlowRule;
import org.checkerframework.dataflow.cfg.ControlFlowGraph;
import org.checkerframework.dataflow.cfg.UnderlyingAST;
import org.checkerframework.dataflow.cfg.block.Block;
-import org.checkerframework.dataflow.cfg.block.BlockImpl;
import org.checkerframework.dataflow.cfg.block.ConditionalBlock;
import org.checkerframework.dataflow.cfg.block.ExceptionBlock;
import org.checkerframework.dataflow.cfg.block.RegularBlock;
@@ -115,7 +115,7 @@ public void performAnalysisBlock(Block b) {
firstNode = node;
}
// Propagate store to predecessors
- for (BlockImpl pred : rb.getPredecessors()) {
+ for (Block pred : rb.getPredecessors()) {
assert currentInput != null : "@AssumeAssertion(nullness): invariant";
propagateStoresTo(
pred,
@@ -143,7 +143,7 @@ public void performAnalysisBlock(Block b) {
.getRegularStore()
.leastUpperBound(exceptionStore)
: transferResult.getRegularStore();
- for (BlockImpl pred : eb.getPredecessors()) {
+ for (Block pred : eb.getPredecessors()) {
addStoreAfter(pred, node, mergedStore, addToWorklistAgain);
}
break;
@@ -154,7 +154,7 @@ public void performAnalysisBlock(Block b) {
TransferInput inputAfter = getInput(cb);
assert inputAfter != null : "@AssumeAssertion(nullness): invariant";
TransferInput input = inputAfter.copy();
- for (BlockImpl pred : cb.getPredecessors()) {
+ for (Block pred : cb.getPredecessors()) {
propagateStoresTo(pred, null, input, FlowRule.EACH_TO_EACH, false);
}
break;
@@ -173,7 +173,7 @@ public void performAnalysisBlock(Block b) {
|| sType == SpecialBlockType.EXCEPTIONAL_EXIT;
TransferInput input = getInput(sb);
assert input != null : "@AssumeAssertion(nullness): invariant";
- for (BlockImpl pred : sb.getPredecessors()) {
+ for (Block pred : sb.getPredecessors()) {
propagateStoresTo(pred, null, input, FlowRule.EACH_TO_EACH, false);
}
}
@@ -285,6 +285,7 @@ protected void addStoreAfter(Block pred, @Nullable Node node, S s, boolean addBl
(exceptionStore != null) ? exceptionStore.leastUpperBound(s) : s;
if (!newExceptionStore.equals(exceptionStore)) {
exceptionStores.put(ebPred, newExceptionStore);
+ inputs.put(ebPred, new TransferInput(node, this, newExceptionStore));
addBlockToWorklist = true;
}
}
@@ -314,7 +315,7 @@ protected void addStoreAfter(Block pred, @Nullable Node node, S s, boolean addBl
@Override
public S runAnalysisFor(
- Node node,
+ @FindDistinct Node node,
boolean before,
TransferInput transferInput,
IdentityHashMap nodeValues,
@@ -339,11 +340,12 @@ public S runAnalysisFor(
ListIterator reverseIter = nodeList.listIterator(nodeList.size());
while (reverseIter.hasPrevious()) {
Node n = reverseIter.previous();
- currentNode = n;
+ setCurrentNode(n);
if (n == node && !before) {
return store.getRegularStore();
}
- // Copy the store to preserve to change the state in {@link #inputs}
+ // Copy the store to avoid changing other blocks' transfer inputs in
+ // {@link #inputs}
TransferResult transferResult =
callTransferFunction(n, store.copy());
if (n == node) {
@@ -368,9 +370,11 @@ public S runAnalysisFor(
if (!before) {
return transferInput.getRegularStore();
}
- currentNode = node;
+ setCurrentNode(node);
+ // Copy the store to avoid changing other blocks' transfer inputs in {@link
+ // #inputs}
TransferResult transferResult =
- callTransferFunction(node, transferInput);
+ callTransferFunction(node, transferInput.copy());
// Merge transfer result with the exception store of this exceptional block
S exceptionStore = exceptionStores.get(eb);
return exceptionStore == null
@@ -383,7 +387,7 @@ public S runAnalysisFor(
}
} finally {
- currentNode = oldCurrentNode;
+ setCurrentNode(oldCurrentNode);
isRunning = false;
}
}
diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/FlowExpressions.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/FlowExpressions.java
index 6fcfc44abc2..72b5b641c3a 100644
--- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/FlowExpressions.java
+++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/FlowExpressions.java
@@ -26,6 +26,8 @@
import javax.lang.model.element.VariableElement;
import javax.lang.model.type.TypeKind;
import javax.lang.model.type.TypeMirror;
+import org.checkerframework.checker.interning.qual.EqualsMethod;
+import org.checkerframework.checker.interning.qual.UsesObjectEquals;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.dataflow.cfg.node.ArrayAccessNode;
import org.checkerframework.dataflow.cfg.node.ArrayCreationNode;
@@ -444,9 +446,23 @@ private static Receiver internalReprOfMemberSelect(
return internalArguments;
}
+ // The syntax that the Checker Framework uses for Java expressions also includes "" and
+ // "#1" for formal parameters. However, there are no special subclasses (AST nodes) for those
+ // extensions.
/**
- * The poorly-named Receiver class is actually a Java AST. Each subclass represents a different
- * type of expression, such as MethodCall, ArrayAccess, LocalVariable, etc.
+ * This class represents a Java expression and its type. It does not represent all possible Java
+ * expressions (for example, it does not represent a ternary expression; use {@link
+ * FlowExpressions.Unknown} for unrepresentable expressions).
+ *
+ *
This class's representation is like an AST: subparts are also expressions. For declared
+ * names (fields, local variables, and methods), it also contains an Element.
+ *
+ *
Each subclass represents a different type of expression, such as {@link
+ * FlowExpressions.MethodCall}, {@link FlowExpressions.ArrayAccess}, {@link
+ * FlowExpressions.LocalVariable}, etc.
+ *
+ * @see the syntax
+ * of Java expressions supported by the Checker Framework
*/
public abstract static class Receiver {
/** The type of this expression. */
@@ -495,10 +511,12 @@ public boolean containsUnknown() {
public abstract boolean isUnmodifiableByOtherCode();
/**
- * Returns true if and only if the two receiver are syntactically identical.
+ * Returns true if and only if the two receivers are syntactically identical.
*
- * @return true if and only if the two receiver are syntactically identical
+ * @param other the other object to compare to this one
+ * @return true if and only if the two receivers are syntactically identical
*/
+ @EqualsMethod
public boolean syntacticEquals(Receiver other) {
return other == this;
}
@@ -734,7 +752,14 @@ public boolean containsModifiableAliasOf(Store> store, Receiver other) {
}
}
+ /** Stands for any expression that the Dataflow Framework lacks explicit support for. */
+ @UsesObjectEquals
public static class Unknown extends Receiver {
+ /**
+ * Create a new Unknown receiver.
+ *
+ * @param type the Java type of this receiver
+ */
public Unknown(TypeMirror type) {
super(type);
}
@@ -1074,11 +1099,14 @@ public boolean containsModifiableAliasOf(Store> store, Receiver other) {
@Override
public boolean equals(@Nullable Object obj) {
+ if (this == obj) {
+ return true;
+ }
if (!(obj instanceof MethodCall)) {
return false;
}
if (method.getKind() == ElementKind.CONSTRUCTOR) {
- return this == obj;
+ return false;
}
MethodCall other = (MethodCall) obj;
return parameters.equals(other.parameters)
diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/ForwardAnalysisImpl.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/ForwardAnalysisImpl.java
index d075f562f68..a35bc78e335 100644
--- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/ForwardAnalysisImpl.java
+++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/ForwardAnalysisImpl.java
@@ -9,6 +9,7 @@
import java.util.Map;
import java.util.Set;
import javax.lang.model.type.TypeMirror;
+import org.checkerframework.checker.interning.qual.FindDistinct;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;
import org.checkerframework.dataflow.cfg.ControlFlowGraph;
@@ -224,7 +225,7 @@ public void performAnalysisBlock(Block b) {
}
@Override
- @SuppressWarnings("contracts.precondition.override.invalid") // implementation field
+ @SuppressWarnings("nullness:contracts.precondition.override.invalid") // implementation field
@RequiresNonNull("cfg")
public List>> getReturnStatementStores() {
List>> result = new ArrayList<>();
@@ -237,7 +238,7 @@ public void performAnalysisBlock(Block b) {
@Override
public S runAnalysisFor(
- Node node,
+ @FindDistinct Node node,
boolean before,
TransferInput transferInput,
IdentityHashMap nodeValues,
@@ -274,14 +275,15 @@ public S runAnalysisFor(
TransferInput store = transferInput;
TransferResult transferResult;
for (Node n : rb.getContents()) {
- currentNode = n;
+ setCurrentNode(n);
if (n == node && before) {
return store.getRegularStore();
}
if (cache != null && cache.containsKey(n)) {
transferResult = cache.get(n);
} else {
- // Copy the store to preserve to change the state in the cache
+ // Copy the store to avoid changing other blocks' transfer inputs in
+ // {@link #inputs}
transferResult = callTransferFunction(n, store.copy());
if (cache != null) {
cache.put(n, transferResult);
@@ -310,9 +312,11 @@ public S runAnalysisFor(
if (before) {
return transferInput.getRegularStore();
}
- currentNode = node;
+ setCurrentNode(node);
+ // Copy the store to avoid changing other blocks' transfer inputs in {@link
+ // #inputs}
TransferResult transferResult =
- callTransferFunction(node, transferInput);
+ callTransferFunction(node, transferInput.copy());
return transferResult.getRegularStore();
}
default:
@@ -320,7 +324,7 @@ public S runAnalysisFor(
throw new BugInCF("Unexpected block type: " + block.getType());
}
} finally {
- currentNode = oldCurrentNode;
+ setCurrentNode(oldCurrentNode);
isRunning = false;
}
}
@@ -502,7 +506,9 @@ protected void addStoreBefore(
break;
}
case BOTH:
- if (thenStore == elseStore) {
+ @SuppressWarnings("interning:not.interned")
+ boolean sameStore = (thenStore == elseStore);
+ if (sameStore) {
// Currently there is only one regular store
S newStore = mergeStores(s, thenStore, shouldWiden);
if (!newStore.equals(thenStore)) {
diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/TransferInput.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/TransferInput.java
index 6682873967d..f6b47e20e3d 100644
--- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/TransferInput.java
+++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/TransferInput.java
@@ -22,8 +22,8 @@ public class TransferInput, S extends Store> {
protected @Nullable Node node;
/**
- * The regular result store (or {@code null} if none is present). The following invariant is
- * maintained:
+ * The regular result store (or {@code null} if none is present, because {@link #thenStore} and
+ * {@link #elseStore} are set). The following invariant is maintained:
*
*
* store == null ⇔ thenStore != null && elseStore != null
@@ -32,22 +32,14 @@ public class TransferInput, S extends Store> {
protected final @Nullable S store;
/**
- * The 'then' result store (or {@code null} if none is present). The following invariant is
- * maintained:
- *
- *
+ * The 'then' result store (or {@code null} if none is present). See invariant at {@link
+ * #store}.
*/
protected final @Nullable S thenStore;
/**
- * The 'else' result store (or {@code null} if none is present). The following invariant is
- * maintained:
- *
- *
+ * The 'else' result store (or {@code null} if none is present). See invariant at {@link
+ * #store}.
*/
protected final @Nullable S elseStore;
@@ -221,7 +213,7 @@ public S getElseStore() {
* potentially not equal
*/
public boolean containsTwoStores() {
- return (thenStore != null && elseStore != null);
+ return store == null;
}
/**
diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/AbstractCFGVisualizer.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/AbstractCFGVisualizer.java
index e10175c3600..a315e1bf007 100644
--- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/AbstractCFGVisualizer.java
+++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/AbstractCFGVisualizer.java
@@ -44,8 +44,9 @@ public abstract class AbstractCFGVisualizer<
implements CFGVisualizer {
/**
- * Initialized in {@link #init(Map)}. If its value is {@code true}, {@link CFGVisualizer}
- * returns more detailed information.
+ * If {@code true}, {@link CFGVisualizer} returns more detailed information.
+ *
+ *
Initialized in {@link #init(Map)}.
*/
protected boolean verbose;
@@ -57,12 +58,24 @@ public abstract class AbstractCFGVisualizer<
@Override
public void init(Map args) {
- Object verb = args.get("verbose");
- this.verbose =
- verb != null
- && (verb instanceof String
- ? Boolean.parseBoolean((String) verb)
- : (boolean) verb);
+ this.verbose = toBoolean(args.get("verbose"));
+ }
+
+ /**
+ * Convert the value to boolean, by parsing a string or casting any other value. null converts
+ * to false.
+ *
+ * @param o an object to convert to boolean
+ * @return {@code o} converted to boolean
+ */
+ private static boolean toBoolean(@Nullable Object o) {
+ if (o == null) {
+ return false;
+ }
+ if (o instanceof String) {
+ return Boolean.parseBoolean((String) o);
+ }
+ return (boolean) o;
}
/**
@@ -104,12 +117,15 @@ protected String visualizeGraphWithoutHeaderAndFooter(
}
/**
- * Adds the successors of the current block to the work list and the visited blocks list.
+ * Outputs, to sbGraph, a visualization of a block's edges, but not the block itself. (The block
+ * itself is output elsewhere.) Also adds the successors of the block to the work list and the
+ * visited blocks list.
*
* @param cur the current block
- * @param visited the set of blocks that have already been visited or are in the work list
- * @param workList the queue of blocks to be processed
- * @param sbGraph the {@link StringBuilder} to store the graph
+ * @param visited the set of blocks that have already been visited or are in the work list; side
+ * effected by this method
+ * @param workList the queue of blocks to be processed; side effected by this method
+ * @param sbGraph the {@link StringBuilder} to store the graph; side effected by this method
*/
protected void handleSuccessorsHelper(
Block cur, Set visited, Queue workList, StringBuilder sbGraph) {
@@ -454,12 +470,12 @@ protected abstract String visualizeNodes(
/**
* Generate the String representation of an edge.
*
- * @param sId the ID of current block
- * @param eId the ID of successor block
+ * @param sId a representation of the current block, such as its ID
+ * @param eId a representation of the successor block, such as its ID
* @param flowRule the content of the edge
* @return the String representation of the edge
*/
- protected abstract String addEdge(long sId, long eId, String flowRule);
+ protected abstract String addEdge(Object sId, Object eId, String flowRule);
/**
* Return the header of the generated graph.
@@ -476,15 +492,16 @@ protected abstract String visualizeNodes(
protected abstract String visualizeGraphFooter();
/**
- * Return the simple String of the process order of a node, e.g., "Process order: 23". When a
- * node have multiple process orders, a sequence of numbers will be returned, e.g., "Process
- * order: 23,25".
+ * Given a list of process orders (integers), returns a string representation.
+ *
+ *
Examples: "Process order: 23", "Process order: 23,25".
*
- * @param order the list of the process order to be processed
- * @return the String representation of the process order of the node
+ * @param order a list of process orders
+ * @return a String representation of the given process orders
*/
protected String getProcessOrderSimpleString(List order) {
- return "Process order: " + order.toString().replaceAll("[\\[\\]]", "");
+ String orderString = order.toString();
+ return "Process order: " + orderString.substring(1, orderString.length() - 1);
}
/**
diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java
index f42d5a1d463..2e6dfcf19b0 100644
--- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java
+++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java
@@ -91,6 +91,7 @@
import javax.lang.model.type.UnionType;
import javax.lang.model.util.Elements;
import javax.lang.model.util.Types;
+import org.checkerframework.checker.interning.qual.FindDistinct;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.dataflow.analysis.Store;
import org.checkerframework.dataflow.cfg.CFGBuilder.ExtendedNode.ExtendedNodeType;
@@ -209,6 +210,7 @@
* preserving the control flow structure.
*
*/
+@SuppressWarnings("nullness") // TODO
public class CFGBuilder {
/** This class should never be instantiated. Protected to still allow subclasses. */
@@ -281,13 +283,15 @@ public static ControlFlowGraph build(
* An extended node can be one of several things (depending on its {@code type}):
*
*
- *
NODE. An extended node of this type is just a wrapper for a {@link Node} (that
- * cannot throw exceptions).
- *
EXCEPTION_NODE. A wrapper for a {@link Node} which can throw exceptions. It
- * contains a label for every possible exception type the node might throw.
- *
UNCONDITIONAL_JUMP. An unconditional jump to a label.
- *
TWO_TARGET_CONDITIONAL_JUMP. A conditional jump with two targets for both the
- * 'then' and 'else' branch.
+ *
NODE: {@link CFGBuilder.NodeHolder}. An extended node of this type is just a
+ * wrapper for a {@link Node} (that cannot throw exceptions).
+ *
EXCEPTION_NODE: {@link CFGBuilder.NodeWithExceptionsHolder}. A wrapper for a
+ * {@link Node} which can throw exceptions. It contains a label for every possible
+ * exception type the node might throw.
+ *
UNCONDITIONAL_JUMP: {@link CFGBuilder.UnconditionalJump}. An unconditional
+ * jump to a label.
+ *
TWO_TARGET_CONDITIONAL_JUMP: {@link CFGBuilder.ConditionalJump}. A conditional
+ * jump with two targets for both the 'then' and 'else' branch.
*
*/
protected abstract static class ExtendedNode {
@@ -916,9 +920,9 @@ public static ControlFlowGraph process(ControlFlowGraph cfg) {
// fix predecessor lists by removing any unreachable predecessors
for (Block c : worklist) {
BlockImpl cur = (BlockImpl) c;
- for (BlockImpl pred : new HashSet<>(cur.getPredecessors())) {
+ for (Block pred : new HashSet<>(cur.getPredecessors())) {
if (!worklist.contains(pred)) {
- cur.removePredecessor(pred);
+ cur.removePredecessor((BlockImpl) pred);
}
}
}
@@ -1008,6 +1012,7 @@ public static ControlFlowGraph process(ControlFlowGraph cfg) {
* @param predecessors an empty set to be filled by this method with all predecessors
* @return the single successor of the set of the empty basic blocks
*/
+ @SuppressWarnings("interning:not.interned") // AST node comparisons
protected static BlockImpl computeNeighborhoodOfEmptyBlock(
RegularBlockImpl start,
Set empty,
@@ -1052,7 +1057,8 @@ protected static void computeNeighborhoodOfEmptyBlockBackwards(
RegularBlockImpl cur = start;
empty.add(cur);
- for (final BlockImpl pred : cur.getPredecessors()) {
+ for (final Block p : cur.getPredecessors()) {
+ BlockImpl pred = (BlockImpl) p;
switch (pred.getType()) {
case SPECIAL_BLOCK:
// add pred correctly to predecessor list
@@ -1087,7 +1093,12 @@ protected static void computeNeighborhoodOfEmptyBlockBackwards(
* place where previously the edge pointed to {@code cur}. Additionally, the predecessor
* holder also takes care of unlinking (i.e., removing the {@code pred} from {@code cur's}
* predecessors).
+ *
+ * @param pred a block whose successor should be set
+ * @param cur the previous successor of {@code pred}
+ * @return a predecessor holder to set the successor of {@code pred}
*/
+ @SuppressWarnings("interning:not.interned") // AST node comparisons
protected static PredecessorHolder getPredecessorHolder(
final BlockImpl pred, final BlockImpl cur) {
switch (pred.getType()) {
@@ -1224,6 +1235,7 @@ private CFGTranslationPhaseTwo() {}
* empty regular basic blocks or conditional blocks with the same block as 'then' and
* 'else' successor)
*/
+ @SuppressWarnings("interning:not.interned") // AST node comparisons
public static ControlFlowGraph process(PhaseOneResult in) {
Map
-
+
GSoC ideas 2020
@@ -203,8 +203,8 @@
How to get started: do a case study
to suppress a warning. Convince yourself that both branches can
execute, or else don't add the if statement.
If you add a @SuppressWarnings annotation,
- write
- it on the smallest possible scope and
+ write
+ it on the smallest possible scope and
explain
why the checker warning is a false positive and you are certain
the code is safe.
diff --git a/docs/developer/release/maven-artifacts/checker-pom.xml b/docs/developer/release/maven-artifacts/checker-pom.xml
index 564ca7a53e6..14593e721ae 100644
--- a/docs/developer/release/maven-artifacts/checker-pom.xml
+++ b/docs/developer/release/maven-artifacts/checker-pom.xml
@@ -33,6 +33,8 @@
+
+
mernstMichael Ernst
diff --git a/docs/developer/release/maven-artifacts/checker-qual-android-pom.xml b/docs/developer/release/maven-artifacts/checker-qual-android-pom.xml
index f637f980365..ee6247eb739 100644
--- a/docs/developer/release/maven-artifacts/checker-qual-android-pom.xml
+++ b/docs/developer/release/maven-artifacts/checker-qual-android-pom.xml
@@ -39,6 +39,8 @@
+
+
mernstMichael Ernst
diff --git a/docs/developer/release/maven-artifacts/checker-qual-pom.xml b/docs/developer/release/maven-artifacts/checker-qual-pom.xml
index bf6a3cbd532..22112d238c2 100644
--- a/docs/developer/release/maven-artifacts/checker-qual-pom.xml
+++ b/docs/developer/release/maven-artifacts/checker-qual-pom.xml
@@ -33,6 +33,8 @@
+
+
mernstMichael Ernst
diff --git a/docs/developer/release/maven-artifacts/dataflow-pom.xml b/docs/developer/release/maven-artifacts/dataflow-pom.xml
index b832a1a8375..8f3391e581e 100644
--- a/docs/developer/release/maven-artifacts/dataflow-pom.xml
+++ b/docs/developer/release/maven-artifacts/dataflow-pom.xml
@@ -43,6 +43,8 @@
+
+
mernstMichael Ernst
diff --git a/docs/developer/release/maven-artifacts/dataflow-shaded-pom.xml b/docs/developer/release/maven-artifacts/dataflow-shaded-pom.xml
index 1dc75c1d323..f5a7a5c155d 100644
--- a/docs/developer/release/maven-artifacts/dataflow-shaded-pom.xml
+++ b/docs/developer/release/maven-artifacts/dataflow-shaded-pom.xml
@@ -30,6 +30,8 @@
+
+
mernstMichael Ernst
diff --git a/docs/developer/release/maven-artifacts/framework-test-pom.xml b/docs/developer/release/maven-artifacts/framework-test-pom.xml
index f6abca146cf..504deb8a4be 100644
--- a/docs/developer/release/maven-artifacts/framework-test-pom.xml
+++ b/docs/developer/release/maven-artifacts/framework-test-pom.xml
@@ -44,6 +44,8 @@
+
+
mernstMichael Ernst
diff --git a/docs/developer/release/maven-artifacts/javacutil-pom.xml b/docs/developer/release/maven-artifacts/javacutil-pom.xml
index 3eb1929b3cb..4f6b16fa2b1 100644
--- a/docs/developer/release/maven-artifacts/javacutil-pom.xml
+++ b/docs/developer/release/maven-artifacts/javacutil-pom.xml
@@ -50,6 +50,8 @@
+
+
mernstMichael Ernst
diff --git a/docs/examples/MavenExample/pom.xml b/docs/examples/MavenExample/pom.xml
index f3b7f18dd50..90802b228eb 100644
--- a/docs/examples/MavenExample/pom.xml
+++ b/docs/examples/MavenExample/pom.xml
@@ -14,7 +14,7 @@
UTF-8${com.google.errorprone:javac:jar}
- 3.5.0
+ 3.6.0
@@ -108,10 +108,10 @@
-Aquals=myPackage.qual.MyFenum,myPackage.qual.MyCustomType
-->
-Alint
-
-
-
-
+
+
+
+
diff --git a/docs/examples/MavenExampleJDK11/pom.xml b/docs/examples/MavenExampleJDK11/pom.xml
index 80c245f62d9..a8fe50473e8 100644
--- a/docs/examples/MavenExampleJDK11/pom.xml
+++ b/docs/examples/MavenExampleJDK11/pom.xml
@@ -12,7 +12,7 @@
UTF-8
- 3.5.0
+ 3.6.0
diff --git a/docs/examples/fenum-extension/Expected.txt b/docs/examples/fenum-extension/Expected.txt
index 87d3cb16063..71361f47cc4 100644
--- a/docs/examples/fenum-extension/Expected.txt
+++ b/docs/examples/fenum-extension/Expected.txt
@@ -43,12 +43,12 @@ Demo.java:29: error: [assignment.type.incompatible] incompatible types in assign
^
found : @Fenum("B") int
required: @Fenum("A") int
-Demo.java:32: error: [argument.type.incompatible] incompatible types in argument.
+Demo.java:32: error: [argument.type.incompatible] incompatible argument for parameter p of fenumArg.
fenumArg(5); // Direct use of value forbidden!
^
found : @FenumUnqualified int
required: @Fenum("A") int
-Demo.java:33: error: [argument.type.incompatible] incompatible types in argument.
+Demo.java:33: error: [argument.type.incompatible] incompatible argument for parameter p of fenumArg.
fenumArg(TestStatic.BCONST1); // Incompatible fenums forbidden!
^
found : @Fenum("B") int
@@ -63,12 +63,12 @@ Demo.java:37: error: [assignment.type.incompatible] incompatible types in assign
^
found : @Fenum("A") int
required: @MyFenum int
-Demo.java:40: error: [argument.type.incompatible] incompatible types in argument.
+Demo.java:40: error: [argument.type.incompatible] incompatible argument for parameter p of myFenumArg.
myFenumArg(8); // Direct use of value forbidden!
^
found : @FenumUnqualified int
required: @MyFenum int
-Demo.java:41: error: [argument.type.incompatible] incompatible types in argument.
+Demo.java:41: error: [argument.type.incompatible] incompatible argument for parameter p of myFenumArg.
myFenumArg(TestStatic.BCONST2); // Incompatible fenums forbidden!
^
found : @Fenum("B") int
diff --git a/docs/examples/lombok/Makefile b/docs/examples/lombok/Makefile
index 5003a44887b..f01c4d37dd1 100644
--- a/docs/examples/lombok/Makefile
+++ b/docs/examples/lombok/Makefile
@@ -4,7 +4,7 @@
# So check for both the error message and make sure it is for the right assignment.
all: clean
- ../../../gradlew build > Out.txt 2>&1
- (grep -qF "User.java:9: error: [argument.type.incompatible] incompatible types in argument." Out.txt \
+ (grep -qF "User.java:9: error: [argument.type.incompatible] incompatible argument for parameter y of y." Out.txt \
&& grep -qF "Foo.java:12: error: [assignment.type.incompatible] incompatible types in assignment." Out.txt \
&& grep -qF "y = null; // error" Out.txt) \
|| (echo "===== start of Out.txt =====" && cat Out.txt && echo "===== end of Out.txt =====" && false)
diff --git a/docs/examples/subtyping-extension/Expected.txt b/docs/examples/subtyping-extension/Expected.txt
index 6358c8f797d..8370787c3cd 100644
--- a/docs/examples/subtyping-extension/Expected.txt
+++ b/docs/examples/subtyping-extension/Expected.txt
@@ -1,7 +1,7 @@
Demo.java:13: warning: [cast.unsafe] cast from "@PossiblyUnencrypted String" to "@Encrypted String" cannot be statically verified
return (@Encrypted String) new String(b);
^
-Demo.java:36: error: [argument.type.incompatible] incompatible types in argument.
+Demo.java:36: error: [argument.type.incompatible] incompatible argument for parameter msg of sendOverTheInternet.
sendOverTheInternet(password); // invalid
^
found : @PossiblyUnencrypted String
diff --git a/docs/manual/accumulation-checker.tex b/docs/manual/accumulation-checker.tex
index ddb0132e280..949d015e9df 100644
--- a/docs/manual/accumulation-checker.tex
+++ b/docs/manual/accumulation-checker.tex
@@ -55,6 +55,21 @@
\href{https://github.com/typetools/checker-framework/blob/master/framework/src/test/java/testaccumulation/qual/TestAccumulationBottom.java}{TestAccumulationBottom.java}.
It should take no arguments, and should be a subtype of the accumulator type you defined earlier.
+You may also define a predicate annotation, analogous to
+\href{https://github.com/typetools/checker-framework/blob/master/framework/src/test/java/testaccumulation/qual/TestAccumulationPredicate.java}{TestAccumulationPredicate.java}.
+It must have a single argument named \ of type \.
+The predicate syntax supports
+\begin{itemize}
+\item \<||> disjunctions
+\item \<\&\&> conjunctions
+\item \ logical complement. \<"!x"> means
+``it is not true that \ was definitely accumulated'' or, equivalently, ``there is no path on which \ was accumulated''.
+Note that this does \textbf{not} mean ``\ was not accumulated'' --- it is not a violation of the specification \<"!x"> if \ is accumulated
+on some paths, but not others.
+\item \<(...)> parentheses for precedence
+\end{itemize}
+
+
\paragraphAndLabel{Setting up the checker}{accumulation-setup}
Define a new class that extends \refclass{common/accumulation}{AccumulationChecker}.
@@ -62,8 +77,9 @@
Define a new class that extends \refclass{common/accumulation}{AccumulationAnnotatedTypeFactory}.
You must create a new constructor whose only argument is a \refclass{common/basetype}{BaseTypeChecker}.
-Your constructor should call the \ constructor defined in
-\refclass{common/accumulation}{AccumulationAnnotatedTypeFactory}.
+Your constructor should call one of the \ constructors defined in
+\refclass{common/accumulation}{AccumulationAnnotatedTypeFactory} (which one depends on whether or not
+you defined a predicate annotation).
\paragraphAndLabel{Adding accumulation logic}{accumulation-accumulating}
diff --git a/docs/manual/advanced-features.tex b/docs/manual/advanced-features.tex
index d3867b8dd00..69b3f558a78 100644
--- a/docs/manual/advanced-features.tex
+++ b/docs/manual/advanced-features.tex
@@ -96,7 +96,9 @@
This means that \<@B MyClass> is an invalid type. (Annotations on class declarations may also specify
default annotations for uses of the type; see Section~\ref{default-for-use})
-An upper bound can also be specified by the type-system designer using the meta-annotation
+If it is not possible to annotate the class's definition (e.g., for
+primitives and some library classes),
+the type-system designer can specify an upper bound by using the meta-annotation
\refqualclass{framework/qual}{UpperBoundFor}.
If no annotation is present on a type declaration and if no \<@UpperBoundFor> mentions the type, then
@@ -128,8 +130,8 @@
These operations might refine its type. If a user wishes to annotate a method that does type refinement,
its formal parameter must be of illegal type \<@A MyClass>, which requires a warning suppression.
-If the framework forbid expressions and local variables from having types inconsistent with the class annotation,
-then important APIs and common coding paradigms will no longer type-check.
+If the framework were to forbid expressions and local variables from having types inconsistent with the class annotation,
+then important APIs and common coding paradigms would no longer type-check.
Consider the annotation
\begin{Verbatim}
@@ -225,7 +227,7 @@
this is usually CLIMB-to-top (Section~\ref{climb-to-top}) (CLIMB means \textbf{C}asts, \textbf{L}ocals,
\textbf{I}nstanceof, and (some) i\textbf{M}plicit \textbf{B}ounds).
\item
- The qualifier with the meta-annotation \<@DefaultQualifierInHierarchy>
+ The qualifier with the meta-annotation \refqualclass{framework/qual}{DefaultQualifierInHierarchy}.
\end{enumerate}
If the unannotated type is the type of a local variable, then the first 5 rules are skipped and only
@@ -1140,7 +1142,9 @@
\item \refqualclass{checker/lock/qual}{Holding}
\end{itemize}
-The set of permitted expressions is a subset of all Java expressions:
+The set of permitted expressions is a subset of all Java expressions,
+with a few extensions, formal parameters like \<\#1> and (for some type
+systems) \code{}.
\begin{itemize}
\item
@@ -1246,20 +1250,12 @@
\textbf{Limitations:}
-The following Java expressions may not currently be written:
-% The Checker Framework is best at reasoning about Java expressions that
-% are variable references, but these expressions are not.
-\begin{itemize}
-\item String concatenation expressions.
-\item Mathematical operators (plus, minus, division, ...).
-\item Comparisons (equality, less than, etc.).
-\end{itemize}
-
-Additionally, it is not possible to write
-quantification over all array components (e.g. to express that all
+It is not possible to write a
+quantification over all array components (e.g., to express that all
array elements are non-null). There is no such Java expression, but it
would be useful when writing specifications.
+
\sectionAndLabel{Field invariants}{field-invariants}
Sometimes a field declared in a superclass has a more precise type in a
diff --git a/docs/manual/annotating-libraries.tex b/docs/manual/annotating-libraries.tex
index cb4012a224c..e61332c795e 100644
--- a/docs/manual/annotating-libraries.tex
+++ b/docs/manual/annotating-libraries.tex
@@ -189,9 +189,29 @@
Whenever you annotate any part of a file, fully annotate the file! That
is, write annotations for all the methods and fields, based on their
-documentation. If you don't annotate the whole file, then users may be
-surprised that calls to some methods type-check as expected whereas other
-methods do not (because they have not been annotated).
+documentation. Here are reasons for this rule:
+
+\begin{itemize}
+\item
+ If you annotate just part of the file, then users may be surprised that
+ calls to some methods type-check as expected whereas other methods do not
+ (because they have not been annotated).
+\item
+ Annotating one method or field at a time may lead to inconsistencies
+ between different parts of the file. Different people may make different
+ assumptions, might write annotations in a way that is locally convenient
+ but globally inconsistent, or might not read all the documentation of the
+ class to understand how it works.
+\item
+ It is not much more effort to annotate an entire class versus one method
+ or field. In either case it is usually necessary to understand the entire
+ class's design and implementation. Once you have done that, you might as
+ well annotate the whole thing.
+\item
+ If you fully annotate the file, it is possible to type-check the library to
+ verify the annotations. (Even if you do not do this right now, it eases
+ the task in the future.)
+\end{itemize}
\subsectionAndLabel{Verify your annotations}{library-tips-verify}
@@ -367,7 +387,7 @@
annotation. For classes without \<@AnnotatedFor>, the checker uses
conservative defaults
(see Section~\ref{defaults-classfile}) for any type use with no explicit
-user-written annotation, and the checker issues no warnings.
+user-written annotation, \emph{and} the checker issues no warnings.
\end{sloppypar}
The \refqualclass{framework/qual}{AnnotatedFor} annotation, written on a
@@ -553,14 +573,11 @@
\subsectionAndLabel{Creating a stub file}{stub-creating}
-Stub files are generally stored together with the checker implementation,
-in the same directory as the checker's \<.java> source code.
-
\subsubsectionAndLabel{If you have access to the Java source code}{stub-creating-with-source}
Every Java file is a stub file. If you have access to the Java file,
-rename file \ to \. You can add
+copy file \ to \. You can add
annotations to the signatures, leaving the method bodies unchanged.
The stub file parser silently ignores any annotations that it cannot
resolve to a type, so don't forget the \ statement.
@@ -625,7 +642,8 @@
\begin{Verbatim}
cd nullness-stub
- java -cp $CHECKERFRAMEWORK/checker/dist/checker.jar org.checkerframework.framework.stub.StubGenerator java.lang.String > String.astub
+ java -cp $CHECKERFRAMEWORK/checker/dist/checker.jar \
+ org.checkerframework.framework.stub.StubGenerator java.lang.String > String.astub
\end{Verbatim}
Supply it with the fully-qualified name of the class for which you wish to
@@ -661,6 +679,30 @@
\end{enumerate}
+\subsectionAndLabel{Distributing stub files}{stub-creating}
+
+If you are writing stub files but are not writing a checker, you can place
+the stub files anywhere that is convenient. However, please consider
+providing your stub files to the checker author, so that other users can
+also benefit from the stub files you wrote.
+
+If you are distributing stub files with a checker implementation, the stub
+files appear in the same directory as the checker class, which is a subtype of
+\. A \refqualclass{framework/qual}{StubFiles} annotation
+on the checker class lists stub files that are always used. For stub files
+whose use is optional (for example, because the behavior is unsound, or
+unsound except in certain circumstances), users must supply the
+\<-Astubs=...> command-line option.
+
+If a stub file contains annotations that are used by the framework rather
+than by any specific checker (such as purity annotations), and you wish to
+distribute it with the Checker Framework, put the stub file in directory
+\. You can also do this if the stub file has
+annotations for multiple checkers. To use a stub file in directory
+\, users must supply the
+\<-Astubs=checker.jar/stub-file-name.astub> command-line option.
+
+
\subsectionAndLabel{Troubleshooting stub libraries}{stub-troubleshooting}
diff --git a/docs/manual/contributors.tex b/docs/manual/contributors.tex
index 1f21d095b1e..70f76e9b002 100644
--- a/docs/manual/contributors.tex
+++ b/docs/manual/contributors.tex
@@ -73,13 +73,16 @@
Nhat Nguyen,
Nikhil Shinde,
Nima Karimipour,
+Nitin Kumar Das,
Oleg Shchelykalnov,
+Olek Wojnar,
Pascal Wittmann,
Patrick Meiring,
Paul Vines,
Paulo Barros,
Philip Lai,
Prionti Nasir,
+Priti Chattopadhyay,
Rashmi Mudduluru,
Ravi Roshan,
Renato Athaydes,
diff --git a/docs/manual/creating-a-checker.tex b/docs/manual/creating-a-checker.tex
index 2c7991da151..1c189236d05 100644
--- a/docs/manual/creating-a-checker.tex
+++ b/docs/manual/creating-a-checker.tex
@@ -1168,7 +1168,7 @@
The annotated type of expressions and types are defined via type introduction rules in the
type factory. For most expressions and types, these rules are the same regardless of the type system.
-For example, the type of a method invocation expression is the return type of the invoked method
+For example, the type of a method invocation expression is the return type of the invoked method,
viewpoint-adapted for the call site. The framework implements these rules so that all type systems
automatically use them. For other expressions, such as string literals, their (annotated) types depend
on the type system, so the framework provides way to specify what qualifiers should apply to these expressions.
@@ -1783,6 +1783,8 @@
already reported the bug, and you want to continue using the checker on a
large codebase without being inundated in stack traces.
+\item \code{-AdumpOnErrors}: Outputs a stack trace when reporting errors or warnings.
+
\end{itemize}
@@ -1905,17 +1907,23 @@
The graph also contains information about flow-sensitively refined
types of various expressions at many program points.
- The argument is a comma-separated sequence of values or key-value pairs.
+ The argument is a comma-separated sequence of keys or key--value pairs.
The first argument is the fully-qualified name of the
\ implementation
- that should be used. The remaining values or key-value pairs are
- passed to \.
+ that should be used. The remaining keys or key--value pairs are
+ passed to \. Supported keys include
+ \begin{itemize}
+ \item \
+ \item \ directory into which to write files
+ \item \
+ \end{itemize}
\end{itemize}
\noindent
You can also use \refclass{dataflow/cfg}{CFGVisualizeLauncher} to generate a DOT
or String representation of the control flow graph of a given method in a given class.
+The CFG is generated and output, but no dataflow analysis is performed.
\begin{itemize}
@@ -1926,7 +1934,7 @@
java -Xbootclasspath/p:$CHECKERFRAMEWORK/checker/dist/javac.jar \
-cp $CHECKERFRAMEWORK/checker/dist/checker.jar \
org.checkerframework.dataflow.cfg.CFGVisualizeLauncher \
- MyClass.java output/ -class MyClass -method test -pdf
+ MyClass.java --class MyClass --method test --pdf
\end{Verbatim}
\end{smaller}
@@ -1937,7 +1945,7 @@
\begin{Verbatim}
java -cp $CHECKERFRAMEWORK/checker/dist/checker.jar \
org.checkerframework.dataflow.cfg.CFGVisualizeLauncher \
- MyClass.java output/ -class MyClass -method test -pdf
+ MyClass.java --class MyClass --method test --pdf
\end{Verbatim}
\end{smaller}
@@ -1945,9 +1953,22 @@
\noindent
The above command will generate the corresponding dot and pdf files for the
-method \code{test} in the class \code{MyClass} in the directory \