I have a class Edge.java
. When I run it through OpenJML, this happens:
error: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can.
Reason: com.sun.tools.javac.code.Symbol$TypeSymbol cannot be cast to com.sun.tools.javac.code.Symbol$ClassSymbol
Weird thing is, I haven't even started to put in the jml notations.
My jdk is 1.7, openjml is current (re-downloaded both to make sure).
This is the command used to run openjml (following the example from the site):
java -jar "E:\Downloads\openjml\openjml.jar" -esc -prover z3_4_3 -exec "E:\Downloads\z3-4.3.0-x64\bin\z3.exe" -noPurityCheck Test.java
Edit: I can confirm that even a very simple class with generics can cause this error:
public class Test<T> {
T i;
}
Edge.java
public class Edge<K> implements Comparable<Edge<K>> {
public K n1, n2;
public int weight;
public final int tiebreaker;
public static int nextTiebreaker = 0;
public Edge(K n1, K n2, int weight) {
this.n1 = n1;
this.n2 = n2;
this.weight = weight;
tiebreaker = nextTiebreaker++;
}
@Override
public int compareTo(Edge<K> o) {
if(this.weight > o.weight) return +1;
if(this.weight < o.weight) return -1;
return tiebreaker - o.tiebreaker; //Same cost, pick one to be the "larger"
}
}
The workaround that I found is to remove the -esc
option (runs extended static checking). Not sure of the proper way to solve this.