RecordFlux icon indicating copy to clipboard operation
RecordFlux copied to clipboard

Coverage check fails due to case-sensitivity

Open senier opened this issue 4 years ago • 3 comments

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 avatar Jan 26 '21 18:01 senier

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

treiher avatar Jan 29 '21 10:01 treiher

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"?).

senier avatar Jan 29 '21 11:01 senier

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.

treiher avatar Jan 29 '21 12:01 treiher

Will be fixed in the 0.19.0 release.

treiher avatar Feb 29 '24 10:02 treiher