Make refinement context parameters unique in Switch_To_*

Close #593
AdaCore · Mar 8, 2021 · 39bc205 · 39bc205
1 parent 6d4179e
commit 39bc205
Show file tree

Hide file tree

Showing 6 changed files with 92 additions and 71 deletions.
diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py
@@ -2719,8 +2719,8 @@ def __create_switch_procedure(
     ) -> UnitPart:
         pdu_name = flat_name(refinement.pdu.full_name)
         sdu_name = flat_name(refinement.sdu.full_name)
-        pdu_context = f"{pdu_name}_Context"
-        sdu_context = f"{sdu_name}_Context"
+        pdu_context = f"{pdu_name}_PDU_Context"
+        sdu_context = f"{sdu_name}_SDU_Context"
         refined_field_affixed_name = f"{pdu_name}.{refinement.field.affixed_name}"
 
         specification = ProcedureSpecification(

diff --git a/tests/integration/specification_model_generator_test.py b/tests/integration/specification_model_generator_test.py
@@ -297,3 +297,24 @@ def test_refinement_with_imported_enum_literal(tmp_path: Path) -> None:
         """
     )
     utils.assert_compilable_code(p.create_model(), tmp_path)
+
+
+def test_refinement_with_self(tmp_path: Path) -> None:
+    utils.assert_compilable_code_string(
+        """
+           package Test is
+              type Tag is (T1 => 1) with Size => 8;
+              type Len is mod 2**8;
+              type Packet is
+                 message
+                    Tag : Tag;
+                    Len : Len;
+                    Val : Opaque
+                       with Size => 8 * Len;
+                 end message;
+              for Packet use (Val => Packet)
+                 if Tag = T1;
+           end Test;
+        """,
+        tmp_path,
+    )
diff --git a/tests/spark/generated/rflx-in_ethernet-generic_contains.adb b/tests/spark/generated/rflx-in_ethernet-generic_contains.adb
@@ -5,14 +5,14 @@ package body RFLX.In_Ethernet.Generic_Contains with
   SPARK_Mode
 is
 
-   procedure Switch_To_Payload (Ethernet_Frame_Context : in out Ethernet_Frame.Context; IPv4_Packet_Context : out IPv4_Packet.Context) is
-      First : constant Types.Bit_Index := Ethernet_Frame.Field_First (Ethernet_Frame_Context, Ethernet_Frame.F_Payload);
-      Last : constant Types.Bit_Index := Ethernet_Frame.Field_Last (Ethernet_Frame_Context, Ethernet_Frame.F_Payload);
+   procedure Switch_To_Payload (Ethernet_Frame_PDU_Context : in out Ethernet_Frame.Context; IPv4_Packet_SDU_Context : out IPv4_Packet.Context) is
+      First : constant Types.Bit_Index := Ethernet_Frame.Field_First (Ethernet_Frame_PDU_Context, Ethernet_Frame.F_Payload);
+      Last : constant Types.Bit_Index := Ethernet_Frame.Field_Last (Ethernet_Frame_PDU_Context, Ethernet_Frame.F_Payload);
       Buffer : Types.Bytes_Ptr;
    begin
-      Ethernet_Frame.Take_Buffer (Ethernet_Frame_Context, Buffer);
+      Ethernet_Frame.Take_Buffer (Ethernet_Frame_PDU_Context, Buffer);
       pragma Warnings (Off, "unused assignment to ""Buffer""");
-      IPv4_Packet.Initialize (IPv4_Packet_Context, Buffer, First, Last);
+      IPv4_Packet.Initialize (IPv4_Packet_SDU_Context, Buffer, First, Last);
       pragma Warnings (On, "unused assignment to ""Buffer""");
    end Switch_To_Payload;
 

diff --git a/tests/spark/generated/rflx-in_ethernet-generic_contains.ads b/tests/spark/generated/rflx-in_ethernet-generic_contains.ads
@@ -26,25 +26,25 @@ is
 
    use type Ethernet_Frame.Field_Cursors;
 
-   procedure Switch_To_Payload (Ethernet_Frame_Context : in out Ethernet_Frame.Context; IPv4_Packet_Context : out IPv4_Packet.Context) with
+   procedure Switch_To_Payload (Ethernet_Frame_PDU_Context : in out Ethernet_Frame.Context; IPv4_Packet_SDU_Context : out IPv4_Packet.Context) with
      Pre =>
-       not Ethernet_Frame_Context'Constrained
-       and not IPv4_Packet_Context'Constrained
-       and Ethernet_Frame.Has_Buffer (Ethernet_Frame_Context)
-       and Ethernet_Frame.Present (Ethernet_Frame_Context, Ethernet_Frame.F_Payload)
-       and Ethernet_Frame.Valid (Ethernet_Frame_Context, Ethernet_Frame.F_Type_Length)
-       and IPv4_Packet_In_Ethernet_Frame_Payload (Ethernet_Frame_Context),
+       not Ethernet_Frame_PDU_Context'Constrained
+       and not IPv4_Packet_SDU_Context'Constrained
+       and Ethernet_Frame.Has_Buffer (Ethernet_Frame_PDU_Context)
+       and Ethernet_Frame.Present (Ethernet_Frame_PDU_Context, Ethernet_Frame.F_Payload)
+       and Ethernet_Frame.Valid (Ethernet_Frame_PDU_Context, Ethernet_Frame.F_Type_Length)
+       and IPv4_Packet_In_Ethernet_Frame_Payload (Ethernet_Frame_PDU_Context),
      Post =>
-       not Ethernet_Frame.Has_Buffer (Ethernet_Frame_Context)
-       and IPv4_Packet.Has_Buffer (IPv4_Packet_Context)
-       and Ethernet_Frame_Context.Buffer_First = IPv4_Packet_Context.Buffer_First
-       and Ethernet_Frame_Context.Buffer_Last = IPv4_Packet_Context.Buffer_Last
-       and IPv4_Packet_Context.First = Ethernet_Frame.Field_First (Ethernet_Frame_Context, Ethernet_Frame.F_Payload)
-       and IPv4_Packet_Context.Last = Ethernet_Frame.Field_Last (Ethernet_Frame_Context, Ethernet_Frame.F_Payload)
-       and IPv4_Packet.Initialized (IPv4_Packet_Context)
-       and Ethernet_Frame_Context.Buffer_First = Ethernet_Frame_Context.Buffer_First'Old
-       and Ethernet_Frame_Context.Buffer_Last = Ethernet_Frame_Context.Buffer_Last'Old
-       and Ethernet_Frame_Context.First = Ethernet_Frame_Context.First'Old
-       and Ethernet_Frame.Context_Cursors (Ethernet_Frame_Context) = Ethernet_Frame.Context_Cursors (Ethernet_Frame_Context)'Old;
+       not Ethernet_Frame.Has_Buffer (Ethernet_Frame_PDU_Context)
+       and IPv4_Packet.Has_Buffer (IPv4_Packet_SDU_Context)
+       and Ethernet_Frame_PDU_Context.Buffer_First = IPv4_Packet_SDU_Context.Buffer_First
+       and Ethernet_Frame_PDU_Context.Buffer_Last = IPv4_Packet_SDU_Context.Buffer_Last
+       and IPv4_Packet_SDU_Context.First = Ethernet_Frame.Field_First (Ethernet_Frame_PDU_Context, Ethernet_Frame.F_Payload)
+       and IPv4_Packet_SDU_Context.Last = Ethernet_Frame.Field_Last (Ethernet_Frame_PDU_Context, Ethernet_Frame.F_Payload)
+       and IPv4_Packet.Initialized (IPv4_Packet_SDU_Context)
+       and Ethernet_Frame_PDU_Context.Buffer_First = Ethernet_Frame_PDU_Context.Buffer_First'Old
+       and Ethernet_Frame_PDU_Context.Buffer_Last = Ethernet_Frame_PDU_Context.Buffer_Last'Old
+       and Ethernet_Frame_PDU_Context.First = Ethernet_Frame_PDU_Context.First'Old
+       and Ethernet_Frame.Context_Cursors (Ethernet_Frame_PDU_Context) = Ethernet_Frame.Context_Cursors (Ethernet_Frame_PDU_Context)'Old;
 
 end RFLX.In_Ethernet.Generic_Contains;
diff --git a/tests/spark/generated/rflx-in_ipv4-generic_contains.adb b/tests/spark/generated/rflx-in_ipv4-generic_contains.adb
@@ -5,25 +5,25 @@ package body RFLX.In_IPv4.Generic_Contains with
   SPARK_Mode
 is
 
-   procedure Switch_To_Payload (IPv4_Packet_Context : in out IPv4_Packet.Context; UDP_Datagram_Context : out UDP_Datagram.Context) is
-      First : constant Types.Bit_Index := IPv4_Packet.Field_First (IPv4_Packet_Context, IPv4_Packet.F_Payload);
-      Last : constant Types.Bit_Index := IPv4_Packet.Field_Last (IPv4_Packet_Context, IPv4_Packet.F_Payload);
+   procedure Switch_To_Payload (IPv4_Packet_PDU_Context : in out IPv4_Packet.Context; UDP_Datagram_SDU_Context : out UDP_Datagram.Context) is
+      First : constant Types.Bit_Index := IPv4_Packet.Field_First (IPv4_Packet_PDU_Context, IPv4_Packet.F_Payload);
+      Last : constant Types.Bit_Index := IPv4_Packet.Field_Last (IPv4_Packet_PDU_Context, IPv4_Packet.F_Payload);
       Buffer : Types.Bytes_Ptr;
    begin
-      IPv4_Packet.Take_Buffer (IPv4_Packet_Context, Buffer);
+      IPv4_Packet.Take_Buffer (IPv4_Packet_PDU_Context, Buffer);
       pragma Warnings (Off, "unused assignment to ""Buffer""");
-      UDP_Datagram.Initialize (UDP_Datagram_Context, Buffer, First, Last);
+      UDP_Datagram.Initialize (UDP_Datagram_SDU_Context, Buffer, First, Last);
       pragma Warnings (On, "unused assignment to ""Buffer""");
    end Switch_To_Payload;
 
-   procedure Switch_To_Payload (IPv4_Packet_Context : in out IPv4_Packet.Context; ICMP_Message_Context : out ICMP_Message.Context) is
-      First : constant Types.Bit_Index := IPv4_Packet.Field_First (IPv4_Packet_Context, IPv4_Packet.F_Payload);
-      Last : constant Types.Bit_Index := IPv4_Packet.Field_Last (IPv4_Packet_Context, IPv4_Packet.F_Payload);
+   procedure Switch_To_Payload (IPv4_Packet_PDU_Context : in out IPv4_Packet.Context; ICMP_Message_SDU_Context : out ICMP_Message.Context) is
+      First : constant Types.Bit_Index := IPv4_Packet.Field_First (IPv4_Packet_PDU_Context, IPv4_Packet.F_Payload);
+      Last : constant Types.Bit_Index := IPv4_Packet.Field_Last (IPv4_Packet_PDU_Context, IPv4_Packet.F_Payload);
       Buffer : Types.Bytes_Ptr;
    begin
-      IPv4_Packet.Take_Buffer (IPv4_Packet_Context, Buffer);
+      IPv4_Packet.Take_Buffer (IPv4_Packet_PDU_Context, Buffer);
       pragma Warnings (Off, "unused assignment to ""Buffer""");
-      ICMP_Message.Initialize (ICMP_Message_Context, Buffer, First, Last);
+      ICMP_Message.Initialize (ICMP_Message_SDU_Context, Buffer, First, Last);
       pragma Warnings (On, "unused assignment to ""Buffer""");
    end Switch_To_Payload;
 

diff --git a/tests/spark/generated/rflx-in_ipv4-generic_contains.ads b/tests/spark/generated/rflx-in_ipv4-generic_contains.ads
@@ -29,26 +29,26 @@ is
 
    use type IPv4_Packet.Field_Cursors;
 
-   procedure Switch_To_Payload (IPv4_Packet_Context : in out IPv4_Packet.Context; UDP_Datagram_Context : out UDP_Datagram.Context) with
+   procedure Switch_To_Payload (IPv4_Packet_PDU_Context : in out IPv4_Packet.Context; UDP_Datagram_SDU_Context : out UDP_Datagram.Context) with
      Pre =>
-       not IPv4_Packet_Context'Constrained
-       and not UDP_Datagram_Context'Constrained
-       and IPv4_Packet.Has_Buffer (IPv4_Packet_Context)
-       and IPv4_Packet.Present (IPv4_Packet_Context, IPv4_Packet.F_Payload)
-       and IPv4_Packet.Valid (IPv4_Packet_Context, IPv4_Packet.F_Protocol)
-       and UDP_Datagram_In_IPv4_Packet_Payload (IPv4_Packet_Context),
+       not IPv4_Packet_PDU_Context'Constrained
+       and not UDP_Datagram_SDU_Context'Constrained
+       and IPv4_Packet.Has_Buffer (IPv4_Packet_PDU_Context)
+       and IPv4_Packet.Present (IPv4_Packet_PDU_Context, IPv4_Packet.F_Payload)
+       and IPv4_Packet.Valid (IPv4_Packet_PDU_Context, IPv4_Packet.F_Protocol)
+       and UDP_Datagram_In_IPv4_Packet_Payload (IPv4_Packet_PDU_Context),
      Post =>
-       not IPv4_Packet.Has_Buffer (IPv4_Packet_Context)
-       and UDP_Datagram.Has_Buffer (UDP_Datagram_Context)
-       and IPv4_Packet_Context.Buffer_First = UDP_Datagram_Context.Buffer_First
-       and IPv4_Packet_Context.Buffer_Last = UDP_Datagram_Context.Buffer_Last
-       and UDP_Datagram_Context.First = IPv4_Packet.Field_First (IPv4_Packet_Context, IPv4_Packet.F_Payload)
-       and UDP_Datagram_Context.Last = IPv4_Packet.Field_Last (IPv4_Packet_Context, IPv4_Packet.F_Payload)
-       and UDP_Datagram.Initialized (UDP_Datagram_Context)
-       and IPv4_Packet_Context.Buffer_First = IPv4_Packet_Context.Buffer_First'Old
-       and IPv4_Packet_Context.Buffer_Last = IPv4_Packet_Context.Buffer_Last'Old
-       and IPv4_Packet_Context.First = IPv4_Packet_Context.First'Old
-       and IPv4_Packet.Context_Cursors (IPv4_Packet_Context) = IPv4_Packet.Context_Cursors (IPv4_Packet_Context)'Old;
+       not IPv4_Packet.Has_Buffer (IPv4_Packet_PDU_Context)
+       and UDP_Datagram.Has_Buffer (UDP_Datagram_SDU_Context)
+       and IPv4_Packet_PDU_Context.Buffer_First = UDP_Datagram_SDU_Context.Buffer_First
+       and IPv4_Packet_PDU_Context.Buffer_Last = UDP_Datagram_SDU_Context.Buffer_Last
+       and UDP_Datagram_SDU_Context.First = IPv4_Packet.Field_First (IPv4_Packet_PDU_Context, IPv4_Packet.F_Payload)
+       and UDP_Datagram_SDU_Context.Last = IPv4_Packet.Field_Last (IPv4_Packet_PDU_Context, IPv4_Packet.F_Payload)
+       and UDP_Datagram.Initialized (UDP_Datagram_SDU_Context)
+       and IPv4_Packet_PDU_Context.Buffer_First = IPv4_Packet_PDU_Context.Buffer_First'Old
+       and IPv4_Packet_PDU_Context.Buffer_Last = IPv4_Packet_PDU_Context.Buffer_Last'Old
+       and IPv4_Packet_PDU_Context.First = IPv4_Packet_PDU_Context.First'Old
+       and IPv4_Packet.Context_Cursors (IPv4_Packet_PDU_Context) = IPv4_Packet.Context_Cursors (IPv4_Packet_PDU_Context)'Old;
 
    function ICMP_Message_In_IPv4_Packet_Payload (Ctx : IPv4_Packet.Context) return Boolean is
      (IPv4_Packet.Has_Buffer (Ctx)
@@ -57,25 +57,25 @@ is
       and then IPv4_Packet.Get_Protocol (Ctx).Known
       and then IPv4_Packet.Get_Protocol (Ctx).Enum = IPv4.PROTOCOL_ICMP);
 
-   procedure Switch_To_Payload (IPv4_Packet_Context : in out IPv4_Packet.Context; ICMP_Message_Context : out ICMP_Message.Context) with
+   procedure Switch_To_Payload (IPv4_Packet_PDU_Context : in out IPv4_Packet.Context; ICMP_Message_SDU_Context : out ICMP_Message.Context) with
      Pre =>
-       not IPv4_Packet_Context'Constrained
-       and not ICMP_Message_Context'Constrained
-       and IPv4_Packet.Has_Buffer (IPv4_Packet_Context)
-       and IPv4_Packet.Present (IPv4_Packet_Context, IPv4_Packet.F_Payload)
-       and IPv4_Packet.Valid (IPv4_Packet_Context, IPv4_Packet.F_Protocol)
-       and ICMP_Message_In_IPv4_Packet_Payload (IPv4_Packet_Context),
+       not IPv4_Packet_PDU_Context'Constrained
+       and not ICMP_Message_SDU_Context'Constrained
+       and IPv4_Packet.Has_Buffer (IPv4_Packet_PDU_Context)
+       and IPv4_Packet.Present (IPv4_Packet_PDU_Context, IPv4_Packet.F_Payload)
+       and IPv4_Packet.Valid (IPv4_Packet_PDU_Context, IPv4_Packet.F_Protocol)
+       and ICMP_Message_In_IPv4_Packet_Payload (IPv4_Packet_PDU_Context),
      Post =>
-       not IPv4_Packet.Has_Buffer (IPv4_Packet_Context)
-       and ICMP_Message.Has_Buffer (ICMP_Message_Context)
-       and IPv4_Packet_Context.Buffer_First = ICMP_Message_Context.Buffer_First
-       and IPv4_Packet_Context.Buffer_Last = ICMP_Message_Context.Buffer_Last
-       and ICMP_Message_Context.First = IPv4_Packet.Field_First (IPv4_Packet_Context, IPv4_Packet.F_Payload)
-       and ICMP_Message_Context.Last = IPv4_Packet.Field_Last (IPv4_Packet_Context, IPv4_Packet.F_Payload)
-       and ICMP_Message.Initialized (ICMP_Message_Context)
-       and IPv4_Packet_Context.Buffer_First = IPv4_Packet_Context.Buffer_First'Old
-       and IPv4_Packet_Context.Buffer_Last = IPv4_Packet_Context.Buffer_Last'Old
-       and IPv4_Packet_Context.First = IPv4_Packet_Context.First'Old
-       and IPv4_Packet.Context_Cursors (IPv4_Packet_Context) = IPv4_Packet.Context_Cursors (IPv4_Packet_Context)'Old;
+       not IPv4_Packet.Has_Buffer (IPv4_Packet_PDU_Context)
+       and ICMP_Message.Has_Buffer (ICMP_Message_SDU_Context)
+       and IPv4_Packet_PDU_Context.Buffer_First = ICMP_Message_SDU_Context.Buffer_First
+       and IPv4_Packet_PDU_Context.Buffer_Last = ICMP_Message_SDU_Context.Buffer_Last
+       and ICMP_Message_SDU_Context.First = IPv4_Packet.Field_First (IPv4_Packet_PDU_Context, IPv4_Packet.F_Payload)
+       and ICMP_Message_SDU_Context.Last = IPv4_Packet.Field_Last (IPv4_Packet_PDU_Context, IPv4_Packet.F_Payload)
+       and ICMP_Message.Initialized (ICMP_Message_SDU_Context)
+       and IPv4_Packet_PDU_Context.Buffer_First = IPv4_Packet_PDU_Context.Buffer_First'Old
+       and IPv4_Packet_PDU_Context.Buffer_Last = IPv4_Packet_PDU_Context.Buffer_Last'Old
+       and IPv4_Packet_PDU_Context.First = IPv4_Packet_PDU_Context.First'Old
+       and IPv4_Packet.Context_Cursors (IPv4_Packet_PDU_Context) = IPv4_Packet.Context_Cursors (IPv4_Packet_PDU_Context)'Old;
 
 end RFLX.In_IPv4.Generic_Contains;