Unsupported JML features should not prevent loading the problem

[wadoon]

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

---

• Mantis: MT-930

• Submitted on: 2008-12-09 by (at)most

• Updated: 2012-03-09

• Assigned to: (at)bweiss

Description

Some unsupported JML features prevent problems from being loaded (either gracefully or less gracefully), while they can be simply ignored and warned about. Some examples:

• informal predicates (KeY exists with an appropriate message)
• (at)assume statements (KeY mumbles about ghost or model fields)
• (at)assert statements (similar)
• (at)nowarn pragmas (similar)

Probably more, these are only from the top of my head...

Files

Notes

(at)bweiss at 2008-12-09

The error messages are better now for the cases you mentioned.

(at)bweiss at 2008-12-22

Graceful handling of unsupported JML features is implemented in 2bf9425. There may still be some features which the parser does not know about -- if you find any of these, feel free to reopen.

History

• (at)most -- (NEW_BUG) 2008-12-09

• (at)bweiss -- (BUGNOTE_ADDED) 2008-12-09

• (at)bweiss -- (BUGNOTE_ADDED) 2008-12-22

• (at)bweiss -- (NORMAL_TYPE) 2008-12-22

• (at)bweiss -- (NORMAL_TYPE) 2008-12-22

• (at)bweiss -- (NORMAL_TYPE) 2008-12-22

• (at)most -- (NORMAL_TYPE) 2012-03-09

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

Attributes

• Category: JML (semantics)
• Status: CLOSED
• Severity: FEATURE
• OS:
• Target Version:
• Resolution: FIXED
• Priority: HIGH
• Reproducibility: ALWAYS
• Platform:
• Commit: None
• Build:
• Tags []
• Labels: ~JML (Semantics) ~Feature ~HIGH

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:26:21.158Z
• updated_at: 2017-05-29T02:26:21.801Z
• closed_at: 2017-05-29T02:26:21.739Z (closed_by: )
• milestone:
• user_notes_count: 0