static instance ghost fields are possible, but should not be

[mattulbrich]

Description

ghost instance static int x is a valid field declaration in KeY JML.
However, the modifiers contract each other and this should not be allowed.

Reproducible

always

Steps to reproduce

Add the above line into your code and it will not fail, but it should.

Additional information

Found by Fabian Koffer in his BSc thesis.

---

• Commit: 985c300