gyhughes / checker-framework Goto Github PK
View Code? Open in Web Editor NEWThis project forked from typetools/checker-framework
Pluggable type-checking for Java
Home Page: http://checkerframework.org/
License: Other
checker-framework's People
Contributors
Stargazers
Watchers
checker-framework's Issues
Expression "new boolean[a.length]" causes a crash
Test case in file checker/tests/index/index-introduction/Issue28.java.
This code:
class Issue28 {
public void fn_is_permutation(int[] a) {
boolean[] see = new boolean[a.length];
}
}
causes this stack trace:
error: AnnotatedTypeMirror.addAnnotation: null is not a valid annotation.
Compilation unit: src/plume/ArraysMdeCrashing.java
Exception: java.lang.Throwable; Stack trace: org.checkerframework.framework.source.SourceChecker.errorAbort(SourceChecker.java:718)
org.checkerframework.javacutil.ErrorReporter.errorAbort(ErrorReporter.java:28)
org.checkerframework.framework.type.AnnotatedTypeMirror.addAnnotation(AnnotatedTypeMirror.java:562)
org.checkerframework.checker.index.IndexAnnotatedTypeFactory$IndexTreeAnnotator.visitNewArray(IndexAnnotatedTypeFactory.java:124)
org.checkerframework.checker.index.IndexAnnotatedTypeFactory$IndexTreeAnnotator.visitNewArray(IndexAnnotatedTypeFactory.java:97)
com.sun.tools.javac.tree.JCTree$JCNewArray.accept(JCTree.java:1574)
com.sun.source.util.SimpleTreeVisitor.visit(SimpleTreeVisitor.java:53)
org.checkerframework.framework.type.treeannotator.ListTreeAnnotator.defaultAction(ListTreeAnnotator.java:38)
org.checkerframework.framework.type.treeannotator.ListTreeAnnotator.defaultAction(ListTreeAnnotator.java:21)
com.sun.source.util.SimpleTreeVisitor.visitNewArray(SimpleTreeVisitor.java:173)
com.sun.tools.javac.tree.JCTree$JCNewArray.accept(JCTree.java:1574)
com.sun.source.util.SimpleTreeVisitor.visit(SimpleTreeVisitor.java:53)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.addComputedTypeAnnotations(GenericAnnotatedTypeFactory.java:1060)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.addComputedTypeAnnotations(GenericAnnotatedTypeFactory.java:1037)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:959)
org.checkerframework.framework.flow.CFAbstractTransfer.getValueFromFactory(CFAbstractTransfer.java:213)
org.checkerframework.framework.flow.CFAbstractTransfer.visitNode(CFAbstractTransfer.java:547)
org.checkerframework.framework.flow.CFAbstractTransfer.visitNode(CFAbstractTransfer.java:101)
org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor.visitArrayCreation(AbstractNodeVisitor.java:347)
org.checkerframework.dataflow.cfg.node.ArrayCreationNode.accept(ArrayCreationNode.java:71)
org.checkerframework.dataflow.analysis.Analysis.callTransferFunction(Analysis.java:362)
org.checkerframework.dataflow.analysis.Analysis.performAnalysis(Analysis.java:199)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:893)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:861)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.performFlowAnalysis(GenericAnnotatedTypeFactory.java:805)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.checkAndPerformFlowAnalysis(GenericAnnotatedTypeFactory.java:1090)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.addComputedTypeAnnotations(GenericAnnotatedTypeFactory.java:1057)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.addComputedTypeAnnotations(GenericAnnotatedTypeFactory.java:1037)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:959)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:2115)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:297)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:171)
com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:720)
com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:50)
org.checkerframework.framework.source.SourceVisitor.visit(SourceVisitor.java:70)
org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:942)
org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:448)
org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:209)
com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:681)
com.sun.tools.javac.api.MultiTaskListener.finished(MultiTaskListener.java:111)
com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1342)
com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1296)
com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:901)
com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:860)
com.sun.tools.javac.main.Main.compile(Main.java:523)
com.sun.tools.javac.main.Main.compile(Main.java:381)
com.sun.tools.javac.main.Main.compile(Main.java:370)
com.sun.tools.javac.main.Main.compile(Main.java:361)
com.sun.tools.javac.Main.compile(Main.java:56)
com.sun.tools.javac.Main.main(Main.java:42)
1 error
Checker crashing on running certain pieces of code
Upon trying to run the checker on a specific piece of code, a NullPointerException is thrown, crashing the program.
I can't attach java files here directly, so I put a folder on drive with the files needed to reproduce the error.
https://drive.google.com/drive/folders/0ByNy04xRyVnXLU9jUllzYVlFd00
Edit: moved to drive
Stack trace:
[coxw2@detroit zxing-gridsampler]$ javac -processor IndexChecker -AprintErrorStack BitMatrix.java
error: SourceChecker.typeProcess: unexpected Throwable (NullPointerException) while processing BitMatrix.java
Compilation unit: BitMatrix.java
Exception: java.lang.NullPointerException; Stack trace: org.checkerframework.checker.index.IndexStore.applyTransfer(IndexStore.java:66)
org.checkerframework.checker.index.IndexStore.updateForMethodCall(IndexStore.java:42)
org.checkerframework.checker.index.IndexStore.updateForMethodCall(IndexStore.java:19)
org.checkerframework.framework.flow.CFAbstractTransfer.visitMethodInvocation(CFAbstractTransfer.java:892)
org.checkerframework.framework.flow.CFAbstractTransfer.visitMethodInvocation(CFAbstractTransfer.java:101)
org.checkerframework.dataflow.cfg.node.MethodInvocationNode.accept(MethodInvocationNode.java:81)
org.checkerframework.dataflow.analysis.Analysis.callTransferFunction(Analysis.java:362)
org.checkerframework.dataflow.analysis.Analysis.performAnalysis(Analysis.java:220)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:893)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:861)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.performFlowAnalysis(GenericAnnotatedTypeFactory.java:805)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.checkAndPerformFlowAnalysis(GenericAnnotatedTypeFactory.java:1090)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.annotateImplicit(GenericAnnotatedTypeFactory.java:1057)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.annotateImplicit(GenericAnnotatedTypeFactory.java:1037)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:921)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:2082)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:297)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:171)
com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:720)
com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:50)
org.checkerframework.framework.source.SourceVisitor.visit(SourceVisitor.java:70)
org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:943)
org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:448)
org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:209)
com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:681)
com.sun.tools.javac.api.MultiTaskListener.finished(MultiTaskListener.java:111)
com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1342)
com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1296)
com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:901)
com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:860)
com.sun.tools.javac.main.Main.compile(Main.java:523)
com.sun.tools.javac.main.Main.compile(Main.java:381)
com.sun.tools.javac.main.Main.compile(Main.java:370)
com.sun.tools.javac.main.Main.compile(Main.java:361)
com.sun.tools.javac.Main.compile(Main.java:56)
com.sun.tools.javac.Main.main(Main.java:42)
1 error
Allow a variable to be an index for two arrays
See test case in file checker/tests/index/index-introduction/IndexForTwoArrays.java (which is currently disabled, until this issue is addressed).
Post-decrement is treated like pre-decrement
For a test case, see file checker/tests/index/index-transfer/Issue27.java
Warning Suppression
Figure out how to properly suppress an indexing warning
toArray and asList should preserve @MinLen annotations
For a test case, see file checker/tests/index/index-transfer/Issue26.java
We don't have tests for Unary Operations (++, --)
MinLen support for lists and Strings
@IndexFor() should require an argument
It is meaningless to write these annotations
@IndexFor()
@IndexOrHigh()
@IndexOrLow()
@LTLength()
@MinLen()
because an argument should always be required. However, the Index Checker permits this and many of the Index Checker's tests use it.
The default arguments should be removed from the definitions of these qualifiers. That will force you to change all tests so that they pass an array name whenever using these qualifiers.
Unexpected Throwable (IndexOutOfBoundsException) while processing
Error causing files are in the drive at:
https://drive.google.com/drive/folders/0ByNy04xRyVnXQTk2OERpcEwtRlU
This was using a developer build of commit 8692b7f.
Exact error:
$ javac -processor IndexChecker GradeBook.java
error: SourceChecker.typeProcess: unexpected Throwable (IndexOutOfBoundsException) while processing GradeBook.java; message: Index: 0, Size: 0
Compilation unit: GradeBook.java
Exception: java.lang.IndexOutOfBoundsException: Index: 0, Size: 0; Stack trace: java.util.ArrayList.rangeCheck(ArrayList.java:653)
java.util.ArrayList.get(ArrayList.java:429)
org.checkerframework.dataflow.cfg.node.ArrayCreationNode.getDimension(ArrayCreationNode.java:53)
org.checkerframework.checker.index.IndexTransfer.visitAssignment(IndexTransfer.java:49)
org.checkerframework.checker.index.IndexTransfer.visitAssignment(IndexTransfer.java:31)
org.checkerframework.dataflow.cfg.node.AssignmentNode.accept(AssignmentNode.java:65)
org.checkerframework.dataflow.analysis.Analysis.callTransferFunction(Analysis.java:362)
org.checkerframework.dataflow.analysis.Analysis.performAnalysis(Analysis.java:199)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:893)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:861)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.performFlowAnalysis(GenericAnnotatedTypeFactory.java:805)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.checkAndPerformFlowAnalysis(GenericAnnotatedTypeFactory.java:1090)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.annotateImplicit(GenericAnnotatedTypeFactory.java:1057)
org.checkerframework.framework.type.GenericAnnotatedTypeFactory.annotateImplicit(GenericAnnotatedTypeFactory.java:1037)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:921)
org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:2082)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:297)
org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:171)
com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:720)
com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:50)
org.checkerframework.framework.source.SourceVisitor.visit(SourceVisitor.java:70)
org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:943)
org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:448)
org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:209)
com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:681)
com.sun.tools.javac.api.MultiTaskListener.finished(MultiTaskListener.java:111)
com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1342)
com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1296)
com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:901)
com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:860)
com.sun.tools.javac.main.Main.compile(Main.java:523)
com.sun.tools.javac.main.Main.compile(Main.java:381)
com.sun.tools.javac.main.Main.compile(Main.java:370)
com.sun.tools.javac.main.Main.compile(Main.java:361)
com.sun.tools.javac.Main.compile(Main.java:56)
com.sun.tools.javac.Main.main(Main.java:42)
1 error
Multiple warning messages
The issue came up when showing the demo and can easily be reproduced by running the demo via cli.
Tests for indexchecker not configured to run in ant
According to the ReadMe in the tests dir we must:
- create a top-level JUnit test, such as:
checker-framework/checker/tests/src/tests/NullnessReflectionTest.java
It is a subclass of CheckerFrameworkTest, and its list of checker
options must include "-Anomsgtext". (See the API documentation for
CheckerFrameworkTest for more detailed information.) - change checker-framework/checker/build.xml to run those tests
arr[arr.length - 1]
allow arr[arr.length - 1] if its length is > 0 (@minlen(1+))
Data flow refinement: indexOrLow == indexOrHigh
The conditional equality check of an IndexOrLow and an IndexOrHigh variable of the same array should lead to refinement to IndexFor type, in the corresponding branch.
Figures should be drawn in SVG
Low-priority issue: Figures in the Index Checker manual chapter should be in SVG format, consistently with other checkers.
More informative message when index is a manifest literal
When the index argument is a literal, one can receive an error message like this:
src/plume/TestPlume.java:1392: warning: [array.access.unsafe.high] Potentially unsafe array access: the index could be too high
int goal_r = rm[0];
^
found : @NonNegative int
required: @IndexFor("rm") int
It would be good to create a different error key than array.access.unsafe.high, whose message gives the type of the array (the needed type will be @MinLen(...) rather than than of the constant index expression.
Bugs in IndexChecker test files
Tests in tests/index-hierarchy, tests/index-type, and tests/index-introduction don't import the quals for the indexchecker that they use.
They additionally do not initialize arrays properly. int arr = new int[] instead of int[] arr = new int[]
Represent "i >= -1" and/or "i >= 1"
The Index Checker seems to need a type to represent ">= -1" and/or ">= 1". (The latter could be named @Positive.)
See file checker/tests/index/index-dataflow/GENegativeOne.java for a test case.
Data flow refinement: indexOrLow > -1
The conditional indexOrLow != -1 leads to refinement to type IndexFor, however the check >-1 does not lead to IndexFor.
Data flow refinement in else clauses
if (indexOrLow < IndexFor) {
// codeblock1
} else {
//codeblock2
}
In codeblock2, indexOrLow should have type IndexFor.
new A[arr.length] should have the same @MinLen annotation as arr did
There is a test case (currently skipped) in file checker/tests/index/index-introduction/NewArrayOfLengthOfMinLenArray.java
indexOf return type
The return type of indexOf should be inferred to be @IndexOrLow.
For a test case, see file checker/tests/index/index-introduction/IndexOf.java
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.