Handle Boolean builtin type in formal function types

Closes #882
AdaCore · Dec 20, 2021 · 4f9a5e7 · 4f9a5e7
1 parent c1223a1
commit 4f9a5e7
Show file tree

Hide file tree

Showing 9 changed files with 42 additions and 4 deletions.
diff --git a/rflx/generator/session.py b/rflx/generator/session.py
@@ -329,6 +329,8 @@ def _create_function_parameters(
                 [ID(function.identifier)],
                 ID(self._prefix * function.return_type * "Structure")
                 if isinstance(function.type_, rty.Message)
+                else ID("Boolean")
+                if function.return_type == rty.BOOLEAN or function.type_ == rty.BOOLEAN
                 else ID(self._prefix * function.return_type),
             )
         )
@@ -347,6 +349,8 @@ def _create_function_parameters(
                     [ID(a.identifier)],
                     ID(const.TYPES_BYTES)
                     if a.type_ == rty.OPAQUE
+                    else ID("Boolean")
+                    if a.type_ == rty.BOOLEAN
                     else ID(self._prefix * a.type_identifier * "Structure")
                     if isinstance(a.type_, rty.Message)
                     else ID(self._prefix * a.type_identifier),

diff --git a/tests/integration/session_functions/config.yml b/tests/integration/session_functions/config.yml
@@ -1,6 +1,7 @@
 functions:
   - Func.Get_Message_Type
   - Func.Create_Message
+  - Func.Valid_Message
 input:
   Channel:
     - 1 0 3 0 1 2

diff --git a/tests/integration/session_functions/generated/rflx-test-session.adb b/tests/integration/session_functions/generated/rflx-test-session.adb
@@ -35,9 +35,11 @@ is
      Post =>
        Initialized
    is
+      Valid : Boolean;
       Message_Type : Universal.Option_Type;
    begin
       Get_Message_Type (Message_Type);
+      Valid_Message (Valid, Message_Type, True);
       if Universal.Message.Structural_Valid (Message_Ctx, Universal.Message.F_Data) then
          declare
             Fixed_Size_Message : Fixed_Size.Simple_Message.Structure;
@@ -49,7 +51,11 @@ is
          P_Next_State := S_Terminated;
          return;
       end if;
-      P_Next_State := S_Reply;
+      if not Valid then
+         P_Next_State := S_Terminated;
+      else
+         P_Next_State := S_Reply;
+      end if;
    end Process;
 
    procedure Reply (P_Next_State : out State) with

diff --git a/tests/integration/session_functions/generated/rflx-test-session.ads b/tests/integration/session_functions/generated/rflx-test-session.ads
@@ -10,6 +10,7 @@ with RFLX.Fixed_Size.Simple_Message;
 generic
    with procedure Get_Message_Type (Get_Message_Type : out RFLX.Universal.Option_Type);
    with procedure Create_Message (Create_Message : out RFLX.Fixed_Size.Simple_Message.Structure; Message_Type : RFLX.Universal.Option_Type; Data : RFLX_Types.Bytes);
+   with procedure Valid_Message (Valid_Message : out Boolean; Message_Type : RFLX.Universal.Option_Type; Strict : Boolean);
 package RFLX.Test.Session with
   SPARK_Mode,
   Initial_Condition =>

diff --git a/tests/integration/session_functions/src/func.adb b/tests/integration/session_functions/src/func.adb
@@ -21,4 +21,14 @@ is
       end if;
    end Create_Message;
 
+   procedure Valid_Message
+      (Valid_Message : out Boolean;
+       Message_Type  :     RFLX.Universal.Option_Type;
+       Strict        :     Boolean)
+   is
+      use type RFLX.Universal.Option_Type;
+   begin
+      Valid_Message := Strict and then Message_Type = (Known => True, Enum => RFLX.Universal.OT_Data);
+   end Valid_Message;
+
 end Func;
diff --git a/tests/integration/session_functions/src/func.ads b/tests/integration/session_functions/src/func.ads
@@ -14,4 +14,6 @@ is
 
    procedure Create_Message (Result : out RFLX.Fixed_Size.Simple_Message.Structure; Message_Type : RFLX.Universal.Option_Type; Data : RFLX.RFLX_Types.Bytes);
 
+   procedure Valid_Message (Valid_Message : out Boolean; Message_Type : RFLX.Universal.Option_Type; Strict : Boolean);
+
 end Func;
diff --git a/tests/integration/session_functions/test.rflx b/tests/integration/session_functions/test.rflx
@@ -12,6 +12,11 @@ package Test is
          (Message_Type : Universal::Option_Type;
           Data : Opaque)
       return Fixed_Size::Simple_Message;
+      -- §S-P-F-P-S, §S-P-F-P-O, §S-P-F-R-S
+      with function Valid_Message
+         (Message_Type : Universal::Option_Type;
+          Strict : Boolean)
+      return Boolean;
    session Session with
       Initial => Start,
       Final => Terminated
@@ -31,11 +36,15 @@ package Test is
       end Start;
 
       state Process is
+         Valid : Boolean; -- §S-S-D-V-T-SC
          Message_Type : Universal::Option_Type; -- §S-S-D-V-T-SC, §S-S-D-V-E-N
       begin
          Message_Type := Get_Message_Type; -- §S-S-A-A-CL, §S-E-CL-N
+         Valid := Valid_Message (Message_Type, True); --  §S-S-A-A-CL, §S-E-CL-S, §S-E-CL-L
          Fixed_Size_Message := Create_Message (Message_Type, Message.Data); -- §S-S-A-A-CL, §S-E-CL-V, §S-E-CL-S
       transition
+         goto Terminated
+            if Valid = False -- §S-S-T-BE
          goto Reply -- §S-S-T-N
       exception
          goto Terminated -- §S-S-E

diff --git a/tests/unit/ada_test.py b/tests/unit/ada_test.py
@@ -557,3 +557,8 @@ def test_while_str() -> None:
 
 def test_qualified_expr() -> None:
     assert str(ada.QualifiedExpr("T", ada.Variable("A"))) == "T'(A)"
+
+
+def test_parameter() -> None:
+    assert str(ada.Parameter(["P1"], "T")) == "P1 : T"
+    assert str(ada.Parameter(["P1"], ada.ID("Boolean"))) == "P1 : Boolean"
diff --git a/tests/unit/generator_test.py b/tests/unit/generator_test.py
@@ -327,7 +327,7 @@ def test_full_base_type_name() -> None:
                     specification=ada.ProcedureSpecification(
                         identifier="F",
                         parameters=[
-                            ada.OutParameter(["F"], "T"),
+                            ada.OutParameter(["F"], ID("Boolean")),
                         ],
                     )
                 ),
@@ -337,7 +337,7 @@ def test_full_base_type_name() -> None:
             decl.FunctionDeclaration(
                 "F",
                 [
-                    decl.Argument("P1", "T1", type_=rty.BOOLEAN),
+                    decl.Argument("P1", "Boolean", type_=rty.BOOLEAN),
                     decl.Argument("P2", "T2", type_=rty.OPAQUE),
                     decl.Argument("P3", "T3", type_=rty.Enumeration("T4", always_valid=True)),
                     decl.Argument("P4", "T4", type_=rty.Integer("T2")),
@@ -352,7 +352,7 @@ def test_full_base_type_name() -> None:
                         identifier="F",
                         parameters=[
                             ada.OutParameter(["F"], "T.Structure"),
-                            ada.Parameter(["P1"], "T1"),
+                            ada.Parameter(["P1"], "Boolean"),
                             ada.Parameter(["P2"], const.TYPES_BYTES),
                             ada.Parameter(["P3"], "T3"),
                             ada.Parameter(["P4"], "T4"),