Assertions in ifs raise exceptions

[mattulbrich]

Description

Using assertions as ~last~ statement inside an (otherwise empty) if-then-block raises a class cast exception

Reproducible

always.

Steps to reproduce

Try to load:

class A {
    //@ ensures true;
    void m() {        
        if(true) {
            //@ assert true;
        } else {
        }            
    }
}

into KeY. It should load, but it will fail while converting to KeY data structures.

Adding a {} after assertion (like in the old days ...) resolves the problem

Additional information

de.uka.ilkd.key.java.ConvertException: class recoder.java.statement.If cannot be cast to class recoder.java.StatementBlock (recoder.java.statement.If and recoder.java.StatementBlock are in unnamed module of loader 'app')
	at de.uka.ilkd.key.java.Recoder2KeY.reportErrorWithPositionInFile(Recoder2KeY.java:1246)
	at de.uka.ilkd.key.java.Recoder2KeY.reportError(Recoder2KeY.java:1236)
	at de.uka.ilkd.key.java.Recoder2KeY.recoderCompilationUnitsAsFiles(Recoder2KeY.java:393)
	at de.uka.ilkd.key.java.Recoder2KeY.readCompilationUnitsAsFiles(Recoder2KeY.java:292)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.readJava(ProblemInitializer.java:282)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:520)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:455)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.createInitConfig(AbstractProblemLoader.java:518)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.loadEnvironment(AbstractProblemLoader.java:288)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:252)
	at de.uka.ilkd.key.proof.io.ProblemLoader.doWork(ProblemLoader.java:65)
	at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:118)
	at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:111)
	at java.desktop/javax.swing.SwingWorker$1.call(SwingWorker.java:304)
	at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
	at java.desktop/javax.swing.SwingWorker.run(SwingWorker.java:343)
	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
	at java.base/java.lang.Thread.run(Thread.java:829)
Caused by: java.lang.ClassCastException: class recoder.java.statement.If cannot be cast to class recoder.java.StatementBlock (recoder.java.statement.If and recoder.java.StatementBlock are in unnamed module of loader 'app')
	at de.uka.ilkd.key.java.recoderext.JMLTransformer.transformAssertStatement(JMLTransformer.java:388)
	at de.uka.ilkd.key.java.recoderext.JMLTransformer.transformMethodlevelCommentsHelper(JMLTransformer.java:556)
	at de.uka.ilkd.key.java.recoderext.JMLTransformer.transformMethodlevelCommentsHelper(JMLTransformer.java:523)
	at de.uka.ilkd.key.java.recoderext.JMLTransformer.transformMethodlevelCommentsHelper(JMLTransformer.java:523)
	at de.uka.ilkd.key.java.recoderext.JMLTransformer.transformMethodlevelComments(JMLTransformer.java:565)
	at de.uka.ilkd.key.java.recoderext.JMLTransformer.makeExplicit(JMLTransformer.java:684)
	at de.uka.ilkd.key.java.recoderext.RecoderModelTransformer.transform(RecoderModelTransformer.java:222)
	at recoder.kit.TwoPassTransformation.execute(TwoPassTransformation.java:91)
	at de.uka.ilkd.key.java.Recoder2KeY.transformModel(Recoder2KeY.java:829)
	at de.uka.ilkd.key.java.Recoder2KeY.recoderCompilationUnitsAsFiles(Recoder2KeY.java:384)
	... 16 more

---

I seem to remember that Alexander @wadoon implemented the improved parsing of JML comments, that's why I initially assign this issue to him.

• Commit: ae839323f6c11eb1504dd43934c5d58e86166c9a i.e. current main

EDIT: Corrected the description from "last statement" to "statement inside empty block". Last statement works, see also my comment with ; //@ assert true; below. @lks9