block contract not attached to empty block

[wadoon]

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

---

• Mantis: MT-1261
• Submitted on: 2013-01-17 by (at)grahl
• Updated: 2014-05-12

Description

Block contracts allow to attach pre-/postconditions and frames to arbitrary Java blocks. Contracts attached to empty blocks cannot be applied.

Steps to reproduce

class C {
  //@ ensures true;
  void foo () {
    //@ ensures true
    {}
  }
}

Files

Notes

(at)grahl at 2013-05-03

Adding ghost declarations / assignment won't work either.

History

• (at)grahl -- (NEW_BUG) 2013-01-17

• (at)grahl -- (BUGNOTE_ADDED) 2013-05-03

• (at)grahl -- (BUG_ADD_RELATIONSHIP) 2013-05-03

• (at)grahl -- (NORMAL_TYPE) 2014-01-03

• (at)grahl -- (NORMAL_TYPE) 2014-05-12

Attributes

• Category: JML (semantics)
• Status: NEW
• Severity: MINOR
• OS:
• Target Version:
• Resolution: OPEN
• Priority: NORMAL
• Reproducibility: ALWAYS
• Platform:
• Commit: 102764bdb5f199d5b5e8bb39334f65aed94b852f
• Build:
• Tags []
• Labels: ~JML (Semantics) ~Bug ~NORMAL
• Version: 2.0

---

View in Mantis

---

Information:

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