Contracts for static initializers not usable

[wadoon]

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

---

• Mantis: MT-1092
• Submitted on: 2011-05-12 by (at)grahl
• Updated: 2014-08-05

Description

When doing proofs with static initialization, contracts cannot be applied. Java+JML files with appropriate specs load just fine, but the "apply contract" rule is not selectable. See also #702.

Files

Associated Bugs

• Relates to MT-702 with

History

• (at)grahl -- (NEW_BUG) 2011-05-12

• (at)grahl -- (BUG_ADD_RELATIONSHIP) 2011-05-12

• (at)grahl -- (BUG_ADD_RELATIONSHIP) 2011-11-28

• (at)grahl -- (BUG_ADD_RELATIONSHIP) 2013-07-23

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

• (at)grahl -- (TAG_ATTACHED) 2014-08-05

Attributes

• Category: JML (semantics)
• Status: NEW
• Severity: MINOR
• OS:
• Target Version:
• Resolution: OPEN
• Priority: LOW
• Reproducibility: ALWAYS
• Platform:
• Commit: None
• Build:
• Tags [{'name': 'static'}]
• Labels: ~JML (Semantics) ~Bug ~LOW

---

View in Mantis

---

Information:

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