Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

"Show inserted labels" diagnostics don't work when a label is inserted via macro #352

Closed
hwayne opened this issue Dec 2, 2024 · 0 comments · Fixed by #353
Closed

"Show inserted labels" diagnostics don't work when a label is inserted via macro #352

hwayne opened this issue Dec 2, 2024 · 0 comments · Fixed by #353
Assignees
Labels
bug Something isn't working

Comments

@hwayne
Copy link
Contributor

hwayne commented Dec 2, 2024

Description:

image

Steps to reproduce:

  1. In the settings file, set "tlaplus.pluscal.options": "-reportLabels",
  2. Translate the following algorithm:
(*--algorithm alg {
variable x = 1;
macro inc() {
    x := x + 1;
}
process (hello = 1) {
    x := x + 1;
    x := x + 1;
    inc();
    x := x + 1;
    x := x + 1;
}

} *)

Expectations:

Diagnostics should underline all five lines, showing that five labels were inserted. But diagnostics stop after the second label.

Cause:

The problem is this line in the PlusCal parser:

const matcher = /^\s\s([A-Za-z0-9_]+) at line \d+, column \d+$/g.exec(line);
if (!matcher) { // done parsing
this.nowParsingAddedLabels = false;
return false;
}

This matches regular labels, but labels inserted from macros have a different format:

The following labels were added:
  Lbl_1 at line 11, column 5
  Lbl_2 at line 12, column 5
  Lbl_3 at line 8, column 5 of macro called at line 13, column 5
  Lbl_4 at line 14, column 5
  Lbl_5 at line 15, column 5

So the label parser terminates early and doesn't label the macro or any lines past the macro.

Notes:

Go ahead and assign this to me, I can fix it next week

# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
bug Something isn't working
Development

Successfully merging a pull request may close this issue.

2 participants