Problem with RAC assertion error line numbers
Opened this issue · 0 comments
davidcok commented
The example in the OpenJMLUserGuide: examples/racreporting/A.java
yields the output
Exception in thread "main" java.lang.AssertionError: examples/racreporting/A.java:5: verify: JML Division by zero
int j = i/(i-i);
^
at java.base/org.jmlspecs.runtime.Utils.assertionFailureL(Utils.java:89)
at A.main(A.java:1)
It is not clear why the line number is 1 instead of 5 in A.main(A.java:1)
It seems the line number is wrong when --rac-java-checks is used but correct without it