```java //@ lbl: {} //@ lbl: a = x; ``` Ghost labels should be converted into JmlGhostLabelStmt, which should behave (except for printing) like a LabeledStmts. Maybe we could reuse the original Java AST class and add a flag.
Ghost labels should be converted into JmlGhostLabelStmt, which
should behave (except for printing) like a LabeledStmts.
Maybe we could reuse the original Java AST class and add a flag.