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

Fix handling of messages with single opaque field #888

Closed
treiher opened this issue Dec 21, 2021 · 0 comments · Fixed by #967
Closed

Fix handling of messages with single opaque field #888

treiher opened this issue Dec 21, 2021 · 0 comments · Fixed by #967
Assignees
Labels
bug generator Related to generator package (SPARK code generation)

Comments

@treiher
Copy link
Collaborator

treiher commented Dec 21, 2021

package Test is

   type Message is
      message
         Data : Opaque;
      end message;

   generic
      Channel : Channel with Readable, Writable;
   session Session with
      Initial => Start,
      Final => Terminated
   is
      M_R : Message; 
      M_S : Message; 
   begin
      state Start is
      begin
         Channel'Read (M_R); 
      transition
         goto Process 
      end Start;

      state Process is
      begin
         M_S := Message'(Data => M_R.Data);
      transition
         goto Reply 
      exception
         goto Terminated 
      end Process;

      state Reply is
      begin
         Channel'Write (M_S); 
      transition
         goto Terminated 
      end Reply;

      state Terminated is null state; 
   end Session;

end Test;
input:
  Channel:
    - 1 2 3
output:
  - Channel
sequence: |
  Write Channel: 1 2 3
  State: Start
  State: Process
  Read Channel: 1 2 3
  State: Reply
E           AssertionError: non-zero exit status 1
E           Write Channel: 1 2 3
E           State: Start
E           State: Process
E           
E           raised CONSTRAINT_ERROR : rflx-test-message.ads:574 range check failed
@treiher treiher added bug generator Related to generator package (SPARK code generation) labels Dec 21, 2021
@treiher treiher added this to To do in RecordFlux 0.6 via automation Dec 21, 2021
@treiher treiher self-assigned this Mar 25, 2022
@treiher treiher moved this from To do to Implementation in RecordFlux 0.6 Mar 25, 2022
@treiher treiher moved this from Implementation to Review in RecordFlux 0.6 Mar 25, 2022
RecordFlux 0.6 automation moved this from Review to Done Mar 28, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug generator Related to generator package (SPARK code generation)
Projects
No open projects
Development

Successfully merging a pull request may close this issue.

1 participant