KeY does not know that enum constants are non-null

[FliegendeWurst]

Description

KeY seemingly doesn't have a rule that makes enum constants non-null.

Reproducible

always

Steps to reproduce

Try to prove the contract below.

File Severity.java

public enum Severity {
    INFO,
    WARNING,
    CRITIQUE	
}

File Checker.java

public class Checker {
    /*@ public normal_behaviour
      @ ensures \result != null;
      @*/
    Severity checkIt() {
        return Severity.INFO;
    }
}

Additional information

---

• Commit: c95c570

[WolframPfeifer]

We just discussed this in our KaKeY meeting. The point is that enums are translated to normal classes, and the class could be in a broken state (if an exception was thrown during initialization, for example in a user-defined constructor). Thus, in general it is not known that the constant is not null. However, this information is encoded in the static invariant of the enum class. So for this particular case it should be sufficient to add the static invariant as a precondition.

However, we agreed that the scenario where it could be null really is a weird corner case, and we should think about how to handle the standard case better.

[mattulbrich]

I double checked with some experiments and looked it up. There cannot even be weird corner cases that lead to enum constant fields pointing to null. Then you would receive a java.lang.ExceptionInInitializerError instead. Assuming they are different is save.