KeY / Recoder transforms JML set statments for ghost variables wrongly

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

For a code fragment such as

  /*@ public normal_behavior
    @ ensures true;
    (at)*/
  public static int fib(int n) {
    int k0 = 1; int k1 = 1;

    //@ ghost int k0_old = k0;
    //@ ghost int k1_old = k1;

    /*@ loop_invariant
      @   n >= 2 ==> (
      @     i <= n + 1 &&
      @     k1 == k1_old + k0_old
      @   );
      @ decreases n-i+1;
      @ assignable \nothing;
      (at)*/
    for (int i = 2; i <= n; i++) {
      int tmp = k1;
      k1 = k0 + k1;
      k0 = tmp;

      //@ set k0_old = k0;
      //@ set k1_old = k1;
    }

    return k1;
  }

...KeY adds the Java statements resulting from setting the ghosts to the wrong places, that is outside the for loop and directly before the return:

for (int i = 2; i<=_n; i++) {
  int tmp = k1;
  k1=k0+k1;
  k0=tmp;
}
k0_old=k0;
k1_old=k1;

I understand that this is probably due to the fact that Recoder needs a statement to assign comments to, and that the next statement after the setters is the return statement, but in any case that is undesired behavior, even more so since a block is left.

---

Information:

• created_at: 2017-05-23T12:17:34.829Z
• updated_at: 2021-09-15T20:27:13.010Z
• closed_at: 2021-09-15T20:27:13.009Z (closed_by: weigl)
• milestone:
• user_notes_count: 4