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

Coverage check fails due to case-sensitivity #562

Closed
senier opened this issue Jan 26, 2021 · 4 comments
Closed

Coverage check fails due to case-sensitivity #562

senier opened this issue Jan 26, 2021 · 4 comments
Labels
bug model Related to model package (e.g., model verification)

Comments

@senier
Copy link
Member

senier commented Jan 26, 2021

The following spec fails only due to f2 being lower case:

package Casing is
   type T is mod 2 ** 32;
   type M is
      message
         F1 : T
            --  Upper-case F2 works!
            then f2 if F1 = 4;
         F2 : T;
         F3 : T;
      end message;
end Casing;
$ rflx check casing.rflx 
Parsing casing.rflx
Processing Casing
casing.rflx:3:9: model: error: path does not cover whole message
casing.rflx:5:10: model: info: on path: "F1"
casing.rflx:7:18: model: info: on path: "f2"
casing.rflx:9:10: model: info: on path: "F3"
@senier senier created this issue from a note in RecordFlux 0.7 (To do) Jan 26, 2021
@senier senier added bug model Related to model package (e.g., model verification) labels Jan 26, 2021
@treiher
Copy link
Collaborator

treiher commented Jan 29, 2021

The specification shouldn't be case-sensitive, but I also don't really like that F2 and f2 refers to the same thing. What about showing a warning when different notations are used for an entity?

For Ada the compiler shows the following for a similar case:

rflx-tlv.ads:36:17: (style) bad casing of "MSG_ERROR" declared at line 10

@senier
Copy link
Member Author

senier commented Jan 29, 2021

A warning is easily ignored. I think we should got further and adopt something different than case insensitivity. Once you used an identifier with a specific casing, using it with a different casing is an error (don't know how this is called - "case preservation"?).

@treiher
Copy link
Collaborator

treiher commented Jan 29, 2021

That sounds even better. I think the verification should still be case-insensitive to avoid subsequent errors and therefore I have created a separate issue for enforcing "case preservation": #563.

@senier senier removed this from To do in RecordFlux 0.7 Aug 23, 2022
@senier senier added this to To do in RecordFlux Future via automation Aug 23, 2022
adacore-bot pushed a commit that referenced this issue Feb 7, 2024
@treiher
Copy link
Collaborator

treiher commented Feb 29, 2024

Will be fixed in the 0.19.0 release.

@treiher treiher closed this as completed Feb 29, 2024
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)
Projects
No open projects
Development

No branches or pull requests

2 participants