[Checkers] Javari checker problems on Daikon
Michael Ernst
mernst at csail.mit.edu
Wed Sep 3 04:08:49 EDT 2008
When I run
make check-javari-all
in $inv/java, the Javari checker throws an exception.
Also, I suspect that since Daikon is un-annotated, it oughtn't be issuing
any errors.
Can you look into these problems?
Thanks!
-Mike
make check-javari-all
jsr308_imports=checkers.interning.quals.* /DS/home-0/mernst/research/invariants/scripts/javac-xlint -p ([/\\]jtb[/\\])|([/\\]junit[/\\]) javac -g -target 5 -typeprocessor checkers.javari.JavariChecker ...
./daikon/inv/ternary/threeScalar/FunctionBinaryFloat.java:122: warning: "@ReadOnly Object" may not be casted to the type "@Mutable FunctionBinaryFloat"
fb = (FunctionBinaryFloat) con.newInstance (new Object[] {});
^
./daikon/inv/ternary/threeScalar/FunctionBinary.java:122: warning: "@ReadOnly Object" may not be casted to the type "@Mutable FunctionBinary"
fb = (FunctionBinary) con.newInstance (new Object[] {});
^
./daikon/Quant.java:538: incompatible types.
found : @ReadOnly Object
required: @Mutable Object
boolean[] oneEltArray = collectboolean (i.next(), fields, fieldsStartIdx + 1);
^
./daikon/Quant.java:1781: incompatible types.
found : @ReadOnly Object
required: @Mutable Object
byte[] oneEltArray = collectbyte (i.next(), fields, fieldsStartIdx + 1);
^
./daikon/Quant.java:2280: incompatible types.
found : @ReadOnly Object
required: @Mutable Object
char[] oneEltArray = collectchar (i.next(), fields, fieldsStartIdx + 1);
^
./daikon/Quant.java:3518: incompatible types.
found : @ReadOnly Object
required: @Mutable Object
double[] oneEltArray = collectdouble (i.next(), fields, fieldsStartIdx + 1);
^
./daikon/Quant.java:4756: incompatible types.
found : @ReadOnly Object
required: @Mutable Object
float[] oneEltArray = collectfloat (i.next(), fields, fieldsStartIdx + 1);
^
./daikon/Quant.java:6148: incompatible types.
found : @ReadOnly Object
required: @Mutable Object
int[] oneEltArray = collectint (i.next(), fields, fieldsStartIdx + 1);
^
./daikon/Quant.java:7445: incompatible types.
found : @ReadOnly Object
required: @Mutable Object
long[] oneEltArray = collectlong (i.next(), fields, fieldsStartIdx + 1);
^
./daikon/Quant.java:8339: incompatible types.
found : @ReadOnly Object
required: @Mutable Object
short[] oneEltArray = collectshort (i.next(), fields, fieldsStartIdx + 1);
^
./daikon/Quant.java:8880: incompatible types.
found : @ReadOnly Object
required: @Mutable Object
Object[] oneEltArray = collectObject (i.next(), fields, fieldsStartIdx + 1);
^
./daikon/Quant.java:9358: cannot return a ReadOnly value as Mutable
return (ac).toArray(new String[]{});
^
./daikon/Quant.java:9382: incompatible types.
found : @ReadOnly Object
required: @Mutable Object
String[] oneEltArray = collectString (i.next(), fields, fieldsStartIdx + 1);
^
./daikon/Quant.java:9614: cannot return a ReadOnly value as Mutable
return ac.toArray(new java.lang.Object[]{});
^
./daikon/SearchNodeUtility.java:55: incompatible types.
found : @ReadOnly T extends @ReadOnly Object
required: @Mutable Object
if (start.equals(end)) {
^
./daikon/SearchNodeUtility.java:55: call to equals(java.lang.Object) not allowed on the given receiver.
found : @ReadOnly Object
required: @Mutable Object
if (start.equals(end)) {
^
./daikon/SearchNodeUtility.java:62: incompatible types.
found : @ReadOnly T extends @ReadOnly Object
required: @Mutable Object
int index = indexNodes.indexOf(start);
^
./daikon/SearchNodeUtility.java:71: incompatible types.
found : @ReadOnly T extends @ReadOnly Object
required: @Mutable Object
if (adjacentNode.equals(end)) {
^
./daikon/SearchNodeUtility.java:71: call to equals(java.lang.Object) not allowed on the given receiver.
found : @ReadOnly Object
required: @Mutable Object
if (adjacentNode.equals(end)) {
^
./daikon/SearchNodeUtility.java:75: incompatible types.
found : @ReadOnly T extends @ReadOnly Object
required: @Mutable Object
if (!visited.contains(adjacentNode) && found == false) {
^
./daikon/SearchNodeUtility.java:89: incompatible types.
found : @ReadOnly T extends @ReadOnly Object
required: @Mutable Object
if (!visited.contains(start) && stopConditions.contains(start)) {
^
./daikon/SearchNodeUtility.java:89: incompatible types.
found : @ReadOnly T extends @ReadOnly Object
required: @Mutable Object
if (!visited.contains(start) && stopConditions.contains(start)) {
^
./daikon/SearchNodeUtility.java:96: incompatible types.
found : @ReadOnly T extends @ReadOnly Object
required: @Mutable Object
int index = indexNodes.indexOf(start);
^
./daikon/SearchNodeUtility.java:105: incompatible types.
found : @ReadOnly T extends @ReadOnly Object
required: @Mutable Object
if (!visited.contains(adjacentNode) && foundNode == null) {
^
./daikon/dcomp/TypeStack.java:376: incompatible types.
found : @ReadOnly K extends @ReadOnly Object
required: @Mutable Object
System.out.printf("key: %s, value: %s%n", k, map.get(k));
^
./daikon/dcomp/TypeStack.java:376: incompatible types.
found : @ReadOnly V extends @ReadOnly Object
required: @Mutable Object
System.out.printf("key: %s, value: %s%n", k, map.get(k));
^
./daikon/dcomp/TypeStack.java:376: incompatible types.
found : @ReadOnly K extends @ReadOnly Object
required: @Mutable Object
System.out.printf("key: %s, value: %s%n", k, map.get(k));
^
./daikon/dcomp/StackVer.java:297: warning: "? extends @ReadOnly Object" may not be casted to the type "@Mutable InstructionContext"
if (((InstructionContext) oldchain.get(ss)).getInstruction().getInstruction() instanceof JsrInstruction){
^
./daikon/dcomp/StackVer.java:299: warning: "? extends @ReadOnly Object" may not be casted to the type "@Mutable InstructionContext"
lastJSR = (InstructionContext) oldchain.get(ss);
An annotation processor threw an uncaught exception.
Consult the following stack trace for details.
java.lang.Error: Javari processor threw unexpected exception when processing StackVer.java
at checkers.source.SourceChecker.process(SourceChecker.java:204)
at com.sun.tools.javac.processing.JavacProcessingEnvironment.callProcessor(JavacProcessingEnvironment.java:738)
at com.sun.tools.javac.processing.JavacProcessingEnvironment.discoverAndRunProcs(JavacProcessingEnvironment.java:667)
at com.sun.tools.javac.processing.JavacProcessingEnvironment.doProcessing(JavacProcessingEnvironment.java:812)
at com.sun.tools.javac.main.JavaCompiler.processAnnotations(JavaCompiler.java:1002)
at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:748)
at com.sun.tools.javac.main.Main.compile(Main.java:386)
at com.sun.tools.javac.main.Main.compile(Main.java:312)
at com.sun.tools.javac.main.Main.compile(Main.java:303)
at com.sun.tools.javac.Main.compile(Main.java:82)
at com.sun.tools.javac.Main.main(Main.java:67)
Caused by: java.lang.StringIndexOutOfBoundsException: String index out of range: 55
at java.lang.String.charAt(String.java:694)
at com.sun.tools.javac.util.Log.printErrLine(Log.java:251)
at com.sun.tools.javac.util.Log.writeDiagnostic(Log.java:343)
at com.sun.tools.javac.util.Log.report(Log.java:306)
at com.sun.tools.javac.util.AbstractLog.mandatoryWarning(AbstractLog.java:135)
at com.sun.tools.javac.processing.JavacMessager.printMessage(JavacMessager.java:169)
at checkers.source.SourceChecker.message(SourceChecker.java:295)
at checkers.source.SourceChecker.report(SourceChecker.java:409)
at checkers.basetype.BaseTypeVisitor.visitTypeCast(BaseTypeVisitor.java:444)
at com.sun.tools.javac.tree.JCTree$JCTypeCast.accept(JCTree.java:1591)
at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:110)
at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:80)
at com.sun.source.util.TreeScanner.visitAssignment(TreeScanner.java:293)
at checkers.basetype.BaseTypeVisitor.visitAssignment(BaseTypeVisitor.java:217)
at com.sun.tools.javac.tree.JCTree$JCAssign.accept(JCTree.java:1463)
at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:110)
at com.sun.source.util.TreeScanner.visitExpressionStatement(TreeScanner.java:239)
at com.sun.tools.javac.tree.JCTree$JCExpressionStatement.accept(JCTree.java:1155)
at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:110)
at com.sun.source.util.TreeScanner.scan(TreeScanner.java:90)
at com.sun.source.util.TreeScanner.visitBlock(TreeScanner.java:159)
at com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:781)
at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:110)
at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:80)
at com.sun.source.util.TreeScanner.visitIf(TreeScanner.java:233)
at com.sun.tools.javac.tree.JCTree$JCIf.accept(JCTree.java:1130)
at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:110)
at com.sun.source.util.TreeScanner.scan(TreeScanner.java:90)
at com.sun.source.util.TreeScanner.visitBlock(TreeScanner.java:159)
at com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:781)
at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:110)
at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:80)
at com.sun.source.util.TreeScanner.visitIf(TreeScanner.java:233)
at com.sun.tools.javac.tree.JCTree$JCIf.accept(JCTree.java:1130)
at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:110)
at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:80)
at com.sun.source.util.TreeScanner.scan(TreeScanner.java:90)
at com.sun.source.util.TreeScanner.visitBlock(TreeScanner.java:159)
at com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:781)
at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:110)
at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:80)
at com.sun.source.util.TreeScanner.visitForLoop(TreeScanner.java:178)
at com.sun.tools.javac.tree.JCTree$JCForLoop.accept(JCTree.java:876)
at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:110)
at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:80)
at com.sun.source.util.TreeScanner.scan(TreeScanner.java:90)
at com.sun.source.util.TreeScanner.visitBlock(TreeScanner.java:159)
at com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:781)
at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:110)
at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:80)
at com.sun.source.util.TreeScanner.visitIf(TreeScanner.java:233)
at com.sun.tools.javac.tree.JCTree$JCIf.accept(JCTree.java:1130)
at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:110)
at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:80)
at com.sun.source.util.TreeScanner.scan(TreeScanner.java:90)
at com.sun.source.util.TreeScanner.visitBlock(TreeScanner.java:159)
at com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:781)
at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:110)
at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:80)
at com.sun.source.util.TreeScanner.visitWhileLoop(TreeScanner.java:170)
at com.sun.tools.javac.tree.JCTree$JCWhileLoop.accept(JCTree.java:835)
at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:110)
at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:80)
at com.sun.source.util.TreeScanner.scan(TreeScanner.java:90)
at com.sun.source.util.TreeScanner.visitBlock(TreeScanner.java:159)
at com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:781)
at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:110)
at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:80)
at com.sun.source.util.TreeScanner.visitMethod(TreeScanner.java:143)
at checkers.basetype.BaseTypeVisitor.visitMethod(BaseTypeVisitor.java:184)
at com.sun.tools.javac.tree.JCTree$JCMethodDecl.accept(JCTree.java:681)
at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:110)
at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:80)
at com.sun.source.util.TreeScanner.scan(TreeScanner.java:90)
at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:98)
at com.sun.source.util.TreeScanner.visitClass(TreeScanner.java:132)
at checkers.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:127)
at checkers.javari.JavariVisitor.visitClass(JavariVisitor.java:52)
at checkers.javari.JavariVisitor.visitClass(JavariVisitor.java:23)
at com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:604)
at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:49)
at checkers.source.SourceChecker.process(SourceChecker.java:199)
... 10 more
make: *** [check-javari-all] Error 1
More information about the checkers
mailing list