Implement ghost labels

```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.
