String literals in JML specification are not created

[Drodt]

Test.java

Description

Consider the following simple method that is obviously correct. KeY is unable to prove this method, even with queries enabled, because in the "yes" case, because it cannot show the precondition of s.equals("no"): It does not know that "no" is created.

/*@ public normal_behavior
    @   requires s != null;
    @   requires s.equals("yes") || s.equals("no");
    @   ensures s.equals("yes") ==> \result == 1;
    @   ensures s.equals("no")  ==> \result == 0;
    @   assignable \strictly_nothing;
    @*/
public int broken(String s) {
  if (s.equals("yes"))
    return 1;
  if (s.equals("no"))
    return 0;
  return -1;
}

Note that the following code works because both strings are created:

/*@ public normal_behavior
    @   requires s != null;
    @   requires s.equals("yes") || s.equals("no");
    @   ensures s.equals("yes") ==> \result == 1;
    @   ensures s.equals("no")  ==> \result == 0;
    @   assignable \strictly_nothing;
    @*/
public int works(String s) {
  // Have literals in the code so queries can evaluate
  String s1 = "yes";
  s1 = "no";
  if (s.equals("yes"))
    return 1;
  if (s.equals("no"))
    return 0;
  return -1;
}

Reproducible

Always.

Steps to reproduce

Describe the steps needed to reproduce the issue.

1. Load the example (method broken)
2. Press the green button

What is your expected behavior and what was the actual behavior?

Proof should close but doesn't

Additional information

This is also why the String tests fail in #3761

---

• Commit: 25fed6e