JML parser makes no distinction between int and long literals

[wadoon]

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

---

Description

Currently long literals in JML must not have a trailing 'l' or 'L'.
The syntax of number literals in JML should be the same as in Java.

Interestingly, one exception exists: Assignments to ghost fields (initialisation and via set-statement) actually require the trailing 'l' or 'L', if the value exceeds the int range.

Reproducible

always

Steps to reproduce

Try to load the following class:

class LiteralTest {
    static long longLiteral = 0x100000000L;         // accepted by parser

    /*@ normal_behavior
      @ ensures \result == 0x100000000L;            // not accepted by parser
      (at)*/
    static long test() {
        return longLiteral;
    }

}

This results in an SLTranslationException:
Mismatched token at line 5:38 'L'

---

• Commit: d0c574550b85be8e7d38287389bc870d0454662c
• Component: ~"JML Parser"
• Severity: ~LOW

---

Information:

• created_at: 2017-06-19T16:19:58.676Z
• updated_at: 2018-06-15T07:25:11.527Z
• closed_at: 2018-06-15T07:25:11.499Z (closed_by: pfeifer)
• milestone:
• user_notes_count: 1