Skip to content

Fix Annotation Position Lookup#141

Open
rcosta358 wants to merge 2 commits intomainfrom
fix-state-refinement-syntax-error
Open

Fix Annotation Position Lookup#141
rcosta358 wants to merge 2 commits intomainfrom
fix-state-refinement-syntax-error

Conversation

@rcosta358
Copy link
Collaborator

This PR fixes a small issue where if we had a syntax error in LiquidJava annotation other than @Refinement, a NoSuchMethodException was thrown because when trying to get the source location of the annotation, I only considered @Refinement annotations. Also added a test case with a syntax error in a state refinement that previously would throw an exception.

@rcosta358 rcosta358 self-assigned this Feb 6, 2026
@rcosta358 rcosta358 added the bug Something isn't working label Feb 6, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug Something isn't working

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant