Handling of class modifier is restricted

[wadoon]

Description

KeY does not correctly handle the annotation /*@ strictly_pure */ when given on a class declaration like /@* stricly_pure */ class A {}.

There is a general problem of JML (modifier) annotation in front of classes (aka. on type declaration level).

It won't be fixed in the current framework, we are waiting for @jmltoolkit/jmlparser.

Work around

Use a Java modifier, for example:

public /*@ strictly_pure */ class A {} 

This pushes the JML annotation from a type declaration

Reproducible

always

Steps to reproduce

1. Add the annotation /*@ strictly_pure */ before a class declaration.
2. Attempt to process in KeY.
3. Observe unexpected/incorrect behavior.

What is your expected behavior and what was the actual behavior?

Expected: Annotation is handled as intended.
Actual: Error or unexpected interpretation.

Additional information

This bug links to #3762.

---

• Commit: