#411 All Eclipse hover error messages turned into "Counterexample: no proof information available"

[Arend Rensink]

After installing OpenJML in Eclipse Luna, all Java-related error messages reported by hovering over the squiggly line in the Java editor have the same message: "Counterexample: no proof information available".

The errors reported in the Problems view, as well as the hovers over the error marker in the left margin, are unaffected (meaning they are what they should be).

[Peter Würtz Vinther Jørgensen]

I also have this problem. I am using Eclipse Luna too.

[Arend Rensink]

Just wanted to remind you that this is still unsolved. It really decreases the usability of the plugin, unfortunately.

[Davide Basile]

just installed OpenJML plugin on Eclipse , I solved the problem by setting the runtime environment to 1.8 and run a TypeCheck JML

[David Cok]

Yes - this problem is fixed in current OpenJML (0.8.51). Note that you do have to be running Java 1.8. It appears that Eclipse downloads in 2020ff presume Java 11, causing problems also. I'm successful with Eclipse 2019-12, and am workiung to upgrade OpenJML to currnet Java (instead of Java 8)