Skip to content

Fix Diagnostic Positions#185

Open
rcosta358 wants to merge 2 commits intomainfrom
fix-errors
Open

Fix Diagnostic Positions#185
rcosta358 wants to merge 2 commits intomainfrom
fix-errors

Conversation

@rcosta358
Copy link
Collaborator

This PR fixes the target locations of some errors and warnings:

  • All errors except for refinement and state refinement errors now correctly target the predicates that caused them
  • The non-existent class warning now targets the qualified name of the class that we are trying to refine

Examples

Before

Warning: Could not find class 'non.existent.Class'
...
5 | @ExternalRefinementsFor("non.existent.Class")
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
6 | public interface NonExistentClass {
...


State Conflict Error: Found multiple disjoint states in state transition: state transition can only go to one state of each state set
...
12 |     @StateRefinement(from="open(this) && closed(this)")
13 |     public void close() {}
   |                 ^^^^^^^^^^
...

Not Found Error: Variable 'x' not found
...
 8 |         @Refinement("x > 0")
 9 |         int y = 1;
   |             ^^^^^^
...

Syntax Error: Invalid refinement expression, expected a logical predicate
...
 8 |         @Refinement("x $ 0")
   |         ^^^^^^^^^^^^^^^^^^^^
 9 |         int x = -1;
...

After

Warning: Could not find class 'non.existent.Class'
...
5 | @ExternalRefinementsFor("non.existent.Class")
  |                         ^^^^^^^^^^^^^^^^^^^^
6 | public interface NonExistentClass {
...

State Conflict Error: Found multiple disjoint states in state transition: state transition can only go to one state of each state set
...
12 |     @StateRefinement(from="open(this) && closed(this)")
   |                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
13 |     public void close() {}
...

Not Found Error: Variable 'x' not found
...
 8 |         @Refinement("x > 0")
   |                     ^^^^^^^
 9 |         int y = 1;
...

Syntax Error: Invalid refinement expression, expected a logical predicate
...
 8 |         @Refinement("x $ 0")
   |                     ^^^^^^^
 9 |         int x = -1;
...

Before merging into main, and after #177 has been merged into main, this branch should be updated with improve-test-suite to ensure proper testing.

@rcosta358 rcosta358 self-assigned this Mar 19, 2026
@rcosta358 rcosta358 added the error messages Related to error messages label Mar 19, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

error messages Related to error messages

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant