Fields of multi-dimensional arrays cannot be referenced by a[*][*] in loop invariants

[wadoon]

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

---

• Mantis: MT-1402
• Submitted on: 2014-01-21 by (at)wasser
• Updated: 2014-02-14

Description

A loop invariant assignable clause may not contain references to multi-dimensional array fields, in the form of a[][] or similar. The problem seems to be that the a[] is interpreted as a location set, whereby the type is no longer correct for the further [] reference. Reference to a[0][] works. Also using \infinite_union to group all a[j][].

Steps to reproduce

public boolean[][] a;
public int i;

...

/*@ loop_invariant true;
  @ assignable a[*][*];
  @ decreasing i;
  (at)*/
  while (i > 0)
    i--;

Files

History

• (at)wasser -- (NEW_BUG) 2014-01-21

• (at)grahl -- (NORMAL_TYPE) 2014-02-14

• (at)grahl -- (NORMAL_TYPE) 2014-02-14

• (at)grahl -- (NORMAL_TYPE) 2014-02-14

Attributes

• Category: JML Parser
• Status: NEW
• Severity: FEATURE
• OS:
• Target Version:
• Resolution: OPEN
• Priority: LOW
• Reproducibility: ALWAYS
• Platform:
• Commit: 97bc4d39b1b54fbd6ea78f149e002647861f1847
• Build:
• Tags []
• Labels: ~JML Parser ~Feature ~LOW
• Version: 2.0.2

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:53:14.622Z
• updated_at: 2017-05-29T02:53:14.622Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 0