Skip to content

fixing lexing to support static invariants#3583

Merged
wadoon merged 1 commit intomainfrom
fixStaticInvIdentifier
Mar 14, 2025
Merged

fixing lexing to support static invariants#3583
wadoon merged 1 commit intomainfrom
fixStaticInvIdentifier

Conversation

@mattulbrich
Copy link
Member

Intended Change

This pull request includes a change to the IMPLICIT_IDENT rule in the KeYLexer.g4 file to allow an optional dollar sign before the letter sequence.

Lexer rule modification:

The reason is that static invariants are represented as Classname::<$inv> which one was not able to use in a manual cut.

But valid key terms should be parseable.

Plan

It is only a 4 character fix allowing implicit identifiers to start with a $.

Type of pull request

  • Bug fix (non-breaking tiny change which fixes an issue)

Ensuring quality

n/a

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

@wadoon wadoon added this pull request to the merge queue Mar 14, 2025
@wadoon wadoon added this to the v2.12.4 milestone Mar 14, 2025
Merged via the queue into main with commit 6d4688a Mar 14, 2025
7 checks passed
@wadoon wadoon deleted the fixStaticInvIdentifier branch March 14, 2025 04:05
@WolframPfeifer
Copy link
Member

I am not really a fan of the constructs o.<inv> and C.<$inv>. I wondered whether it would be a good idea to use something like C.class.<inv> for the latter. That would be at least one special construct less, and be closer to Java and the developer perspective ...

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants