nullable is ignored for arguments of model methods

[gewitternacht]

Description

When defining a model method with a nullable argument like

helper model int foo(nullable Nullable n) { ... }

it seems KeY ignores the nullable annotation.

For example, this can be observed when loading the contract for the model method itself, an accessible clause thereof or when applying the rule "Use Dependency Contract" on this model method: They all look the same as if nullable is omitted and contain (¬n = null)«impl».

Reproducible

always

Steps to reproduce

1. load Nullable.java in KeY
2. choose any contract of foo() to prove
3. observe the (¬n = null)«impl»

To understand where this is a problem for me:

1. load nullable.proof in KeY
2. observe that one subgoal necessary for applying "Use Dependency Contract" is not provable due to the ignored annotation

Note that this particular proof could be closed simply by not using the dependency contract and instead expanding the definition of foo(). However, this is not always (easily) possible in more complex proof situations.

Files: nullable.zip

---

• Commit: 6a92947