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

Pseudo-variable "Message" not handled correctly in message types #401

Closed
senier opened this issue Aug 11, 2020 · 1 comment · Fixed by #889
Closed

Pseudo-variable "Message" not handled correctly in message types #401

senier opened this issue Aug 11, 2020 · 1 comment · Fixed by #889
Assignees
Labels
bug model Related to model package (e.g., model verification)

Comments

@senier
Copy link
Member

senier commented Aug 11, 2020

package Test is

   type Inner is
      message
         null
            then Data
               with Length => Message'Length;
         Data : Opaque;
      end message;

   type Outer is
      message
         A : Boolean;
         Inner : Inner;
         B : Boolean;
      end message;

end Test;
$ rflx check test.rflx
Parsing test.rflx
Processing Test
test.rflx:6:18: model: error: unreachable field "Inner_Data" in "Test::Outer"
test.rflx:6:18: model: info: path 0 (A -> Inner_Data):
test.rflx:6:18: model: info: unsatisfied "Inner_Data'Last = (A'Last + 1 + Message'Length) - 1"
test.rflx:11:4: model: info: unsatisfied "Message'Last >= Inner_Data'Last"
test.rflx:13:10: model: info: unsatisfied "A'Last = (Message'First + 1) - 1"
test.rflx:11:4: model: info: unsatisfied "Message'Length = Message'Last - Message'First + 1"
test.rflx:15:10: model: error: unreachable field "B" in "Test::Outer"
test.rflx:15:10: model: info: path 0 (A -> Inner_Data -> B):
test.rflx:6:18: model: info: unsatisfied "Inner_Data'Last = (A'Last + 1 + Message'Length) - 1"
test.rflx:15:10: model: info: unsatisfied "B'Last = (Inner_Data'Last + 1 + 1) - 1"
test.rflx:13:10: model: info: unsatisfied "A'Last = (Message'First + 1) - 1"
test.rflx:11:4: model: info: unsatisfied "Message'Last >= B'Last"
test.rflx:11:4: model: info: unsatisfied "Message'Length = Message'Last - Message'First + 1"
model: error: unreachable field "Final" in "Test::Outer"
model: info: path 0 (A -> Inner_Data -> B -> Final):
test.rflx:6:18: model: info: unsatisfied "Inner_Data'Last = (A'Last + 1 + Message'Length) - 1"
test.rflx:15:10: model: info: unsatisfied "B'Last = (Inner_Data'Last + 1 + 1) - 1"
test.rflx:13:10: model: info: unsatisfied "A'Last = (Message'First + 1) - 1"
test.rflx:11:4: model: info: unsatisfied "Message'Last >= B'Last"
test.rflx:11:4: model: info: unsatisfied "Message'Length = Message'Last - Message'First + 1"
model: error: contradicting condition in "Test::Outer"
test.rflx:13:10: model: info: on path: "A"
test.rflx:6:18: model: info: on path: "Inner_Data"
test.rflx:13:10: model: info: unsatisfied "A'Last = (Message'First + 1) - 1"
test.rflx:11:4: model: info: unsatisfied "Message'Length = Message'Last - Message'First + 1"
test.rflx:6:18: model: info: unsatisfied "Inner_Data'Last = (A'Last + 1 + Message'Length) - 1"
test.rflx:11:4: model: info: unsatisfied "Message'Last >= Inner_Data'Last"
model: error: contradicting condition in "Test::Outer"
test.rflx:13:10: model: info: on path: "A"
test.rflx:6:18: model: info: on path: "Inner_Data"
test.rflx:15:10: model: info: on path: "B"
test.rflx:13:10: model: info: unsatisfied "A'Last = (Message'First + 1) - 1"
test.rflx:11:4: model: info: unsatisfied "Message'Length = Message'Last - Message'First + 1"
test.rflx:6:18: model: info: unsatisfied "Inner_Data'Last = (A'Last + 1 + Message'Length) - 1"
test.rflx:15:10: model: info: unsatisfied "B'Last = (Inner_Data'Last + 1 + 1) - 1"
test.rflx:11:4: model: info: unsatisfied "Message'Last >= B'Last"
@senier senier created this issue from a note in RecordFlux 0.5 (To do) Aug 11, 2020
@treiher treiher added the model Related to model package (e.g., model verification) label Aug 11, 2020
@senier senier added the bug label Aug 11, 2020
senier pushed a commit to senier/rflx_asn1_der that referenced this issue Aug 12, 2020
@senier senier added this to To do in RecordFlux Future via automation Oct 12, 2020
@senier senier removed this from To do in RecordFlux 0.5 Oct 12, 2020
@treiher
Copy link
Collaborator

treiher commented Oct 11, 2021

The issue will be obsolete after realization of #736, as the use of Message'Size in size aspects will be prohibited. The use case can be realized by parameterized messages.

@treiher treiher removed this from To do in RecordFlux Future Oct 11, 2021
@treiher treiher added this to To do in RecordFlux 0.6 via automation Oct 11, 2021
@treiher treiher self-assigned this Dec 14, 2021
@treiher treiher moved this from To do to Implementation in RecordFlux 0.6 Dec 14, 2021
treiher added a commit that referenced this issue Dec 14, 2021
treiher added a commit that referenced this issue Dec 16, 2021
treiher added a commit that referenced this issue Dec 17, 2021
treiher added a commit that referenced this issue Dec 20, 2021
treiher added a commit that referenced this issue Dec 21, 2021
treiher added a commit that referenced this issue Dec 21, 2021
@senier senier moved this from Implementation to Review in RecordFlux 0.6 Dec 21, 2021
RecordFlux 0.6 automation moved this from Review to Done Jan 3, 2022
treiher added a commit that referenced this issue Jan 3, 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)
Projects
No open projects
2 participants