KeY modifier recognition defective

[wadoon]

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

---

• Mantis: MT-1414
• Submitted on: 2014-02-19 by (at)mulbrich
• Updated: 2014-02-19

Description

The detection of JML modifiers is corrupt:

1. If a JML modifier is not embedded into the last comment before
   a class element, it is ignored.

2. If the modifier string appears anywhere in the comment, this
   triggers the modifier to be set to true.

For instance:

• /(at)helper@/ /(at)pure@/ void n() { }
  declares a pure method which is not a helper method.

• /*@ ensures helperValue == 0; */ void m() { }
  declares a helper method.

Steps to reproduce

Load the attached file. In the Proof Management Dialog you can see
that the method m is pure, but not helper although specified.

Method n is pure and helper although it should be none.

Mehtod o is none, but should be pure and helper.

Additional Information

Responsible for this is the class JMLInfoExtractor in which the comments
are not parsed but a textual search is performed.

Files

A.java:

class A {
  int helperValue = 0;

  /*@ requires pureParam == 0;
    @ ensures helperValue == 0; 
    (at)*/
  void n(int pureParam) {}

  /*@ ensures true; */
  /*@ helper */
  /*@ pure (at)*/
  void m() {}


  /*@ ensures true; pure helper */
  /* Some ordinary comment */
  void o() {}
}

Associated Bugs

• Relates to MT-1166 with

History

• (at)mulbrich -- (NEW_BUG) 2014-02-19

• (at)mulbrich -- (NORMAL_TYPE) 2014-02-19

• (at)mulbrich -- (NORMAL_TYPE) 2014-02-19

• (at)mulbrich -- (DESCRIPTION_UPDATED) 2014-02-19

• (at)mulbrich -- (STEP_TO_REPRODUCE_UPDATED) 2014-02-19

• (at)mulbrich -- (ADDITIONAL_INFO_UPDATED) 2014-02-19

• (at)mulbrich -- (FILE_ADDED) 2014-02-19

• (at)mulbrich -- (BUG_ADD_RELATIONSHIP) 2014-02-19

Attributes

• Category: JML Parser
• Status: NEW
• Severity: MAJOR
• OS:
• Target Version:
• Resolution: OPEN
• Priority: NORMAL
• Reproducibility: ALWAYS
• Platform:
• Commit: fd6bd5ab08bbf1fb2a0a792eca158d87d9ac5cb9
• Build:
• Tags []
• Labels: ~JML Parser ~Bug ~NORMAL

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:31:02.689Z
• updated_at: 2020-11-12T21:35:59.921Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 1