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

Boolean type not correctly generated for generic session functions #882

Closed
senier opened this issue Dec 17, 2021 · 0 comments · Fixed by #885
Closed

Boolean type not correctly generated for generic session functions #882

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

Comments

@senier
Copy link
Member

senier commented Dec 17, 2021

The following spec

package Test is

   type Reserved_7 is mod 2 ** 7;
   type M is
      message
         F1 : Boolean;
         F2 : Reserved_7;
      end message;
   generic
      with function Func (Arg : Boolean) return Boolean;                                                               
   session S with
      Initial => S1,
      Final   => Done
   is
   begin
      state S1 is
         Message : M;
         Value   : Boolean;
      begin
         Value := Func (True);
         Message := M'(F1 => Value, F2 => 0);                                                                          
      transition
         goto Done
      exception
         goto Done
      end S1;
      state Done is null state;
   end S;
end Test;

results in this session code:

generic
   with procedure Func (Func : out RFLX.__BUILTINS__.Boolean; Arg : RFLX.__BUILTINS__.Boolean);
package RFLX.Test.S with
  SPARK_Mode,
  Initial_Condition =>
    Uninitialized
is
[...]
@senier senier created this issue from a note in RecordFlux 0.6 (To do) Dec 17, 2021
@senier senier added bug generator Related to generator package (SPARK code generation) labels Dec 17, 2021
@senier senier self-assigned this Dec 17, 2021
@senier senier moved this from To do to Implementation in RecordFlux 0.6 Dec 17, 2021
senier pushed a commit that referenced this issue Dec 20, 2021
@senier senier moved this from Implementation to Review in RecordFlux 0.6 Dec 20, 2021
senier pushed a commit that referenced this issue Dec 20, 2021
senier pushed a commit that referenced this issue Dec 20, 2021
RecordFlux 0.6 automation moved this from Review to Done Dec 20, 2021
senier pushed a commit that referenced this issue Dec 20, 2021
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