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