Return statements in nested loops cannot be verified

[wadoon]

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

---

• Mantis: MT-1256
• Submitted on: 2012-12-19 by (at)mulbrich
• Updated: 2012-12-19

Description

A program with a return statement which appears within at least 2 nested loops cannot be verified in general.

The problem is that there is a program variable "rtrn" holding whether a return has been encountered. It is introduced when handling the first loop. Since it is a program variable assigned to in the loop body, it becomes anonymised when handling the inner loop. Due to this effect, the program loses information. This cannot be fixed in a JML invariant since the new program variables are introduced only after parsing the specification.

Steps to reproduce

Try to verify the attached file.

Files

AA.java:

class AA {

    boolean earlyExit;

    //@ ensures \result == 1;
    int m() {

    /*@ loop_invariant true; 
      @ decreases 100-i; 
      @ assignable \strictly_nothing;
      (at)*/
    for(int i = 0; i < 100; i++) {

        /* @ loop_invariant true;
          @ decreases 100-j; 
          @ assignable \strictly_nothing; 
          (at)*/
        for(int j= 0; j < 100; j++) {
        if(earlyExit) {
            return 1;
        }
        }
    }

    return 1;
    }
}

History

• (at)mulbrich -- (NEW_BUG) 2012-12-19

• (at)mulbrich -- (FILE_ADDED) 2012-12-19

Attributes

• Category: Calculus
• Status: NEW
• Severity: MAJOR
• OS:
• Target Version:
• Resolution: OPEN
• Priority: NORMAL
• Reproducibility: ALWAYS
• Platform:
• Commit: ?
• Build:
• Tags []
• Labels: ~Calculus ~Bug ~NORMAL

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:43:36.011Z
• updated_at: 2019-04-09T12:26:28.120Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 1

[FliegendeWurst]

It does work with the new Loop Scope rule (see #1495)