Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

Arbitrary identifier accepted as message parameter #874

Closed
senier opened this issue Dec 9, 2021 · 1 comment · Fixed by #1202
Closed

Arbitrary identifier accepted as message parameter #874

senier opened this issue Dec 9, 2021 · 1 comment · Fixed by #1202
Assignees
Labels
bug model Related to model package (e.g., model verification) small Effort of one person-day or less

Comments

@senier
Copy link
Member

senier commented Dec 9, 2021

The following specification should be rejected as the parameter passed to the message type does not exist:

package Test is
   type T is mod 2 ** 8;
   type M1 (P : Boolean) is
      message
         F : T;
      end message;
   type M2 is
      message
         F : M1 (P => Blubber);
      end message;
end Test;

Currently rflx check succeeds on this specification.

@senier senier created this issue from a note in RecordFlux 0.6 (To do) Dec 9, 2021
@senier senier added bug model Related to model package (e.g., model verification) labels Dec 9, 2021
@treiher treiher added the small Effort of one person-day or less label Jan 27, 2022
@mhadhbir mhadhbir moved this from To do to Implementation in RecordFlux 0.6 Feb 10, 2022
@treiher
Copy link
Collaborator

treiher commented Feb 11, 2022

The actual problem is that P is unused in M1. The use of message types as field types is just some form of syntactic sugar. The message model does not contain that information. Blubber just gets lost during merging M1 into M2. Only the resulting message is verified, where no Blubber exists anymore. I think the best solution would be to just add a check for unused message parameters here:

https://github.com/Componolit/RecordFlux/blob/5e894e44a07d3d6d26b745bff00add009ac9f8da/rflx/model/message.py#L796-L802

mhadhbir added a commit that referenced this issue Feb 17, 2022
mhadhbir added a commit that referenced this issue Feb 17, 2022
@senier senier moved this from Implementation to To do in RecordFlux 0.6 Mar 1, 2022
@senier senier removed this from To do in RecordFlux 0.6 Aug 23, 2022
@senier senier added this to To do in RecordFlux Future via automation Aug 23, 2022
@senier senier moved this from To do to Backlog in RecordFlux Future Aug 24, 2022
@senier senier moved this from Backlog to To do in RecordFlux Future Aug 24, 2022
@senier senier removed this from Medium in RecordFlux Future Aug 30, 2022
@senier senier added this to To do in RecordFlux 0.7 via automation Aug 30, 2022
@treiher treiher self-assigned this Sep 23, 2022
@treiher treiher moved this from To do to Implementation in RecordFlux 0.7 Sep 23, 2022
treiher added a commit that referenced this issue Sep 23, 2022
@treiher treiher moved this from Implementation to Review in RecordFlux 0.7 Sep 23, 2022
treiher added a commit that referenced this issue Sep 26, 2022
treiher added a commit that referenced this issue Sep 26, 2022
RecordFlux 0.7 automation moved this from Review to Done Sep 26, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug model Related to model package (e.g., model verification) small Effort of one person-day or less
Projects
No open projects
Development

Successfully merging a pull request may close this issue.

3 participants