Ensure compatibility to GNAT Pro 23.0w

Ref. #905

.github/workflows/tests.yml

@@ -257,6 +257,8 @@ jobs:
             gnat-version: "21.2"
           - gnat-distrib: "pro"
             gnat-version: "22.0"
+          - gnat-distrib: "pro"
+            gnat-version: "23.0w-20220202"
           - gnat-distrib: "fsf"
     env:
       python-version: 3.7

README.md

@@ -271,7 +271,7 @@ As a prerequisite, the following dependencies need to be installed:
 
 - For compiling the generated code, one of the following versions of GNAT is required:
     - [GNAT Community](https://www.adacore.com/download) 2020 or 2021
-    - [GNAT Pro](https://www.adacore.com/gnatpro) 20.2 or 21.2
+    - [GNAT Pro](https://www.adacore.com/gnatpro) 20.2, 21.2 or 22.0
     - [FSF GNAT](https://www.gnu.org/software/gnat/) 11.2 [![GNAT Alire Crate](https://img.shields.io/endpoint?url=https://alire.ada.dev/badges/gnat_native.json)](https://alire.ada.dev/crates/gnat_native.html)
 - [GNATcoll iconv binding](https://github.com/AdaCore/gnatcoll-bindings/tree/master/iconv) [![GNATcoll iconv binding Alire Crate](https://img.shields.io/endpoint?url=https://alire.ada.dev/badges/gnatcoll_iconv.json)](https://alire.ada.dev/crates/gnatcoll_iconv.html) must be installed separately if FSF GNAT is used.
 - For the formal verification of the generated code, the SPARK toolset provided by [GNAT Community](https://www.adacore.com/download) 2021 is required.

defaults.adc

@@ -1,6 +1,3 @@
+pragma Restrictions (No_Elaboration_Code);
 pragma Restrictions (No_Secondary_Stack);
--- ISSUE: Componolit/RecordFlux#905
--- The restriction `No_Elaboration_Code` requires `No_Tagged_Type_Registration`, if tagged types
--- are used. The support for `No_Tagged_Type_Registration` was added in GNAT Pro 23.x.
--- pragma Restrictions (No_Elaboration_Code);
--- pragma Restrictions (No_Tagged_Type_Registration);
+pragma Restrictions (No_Tagged_Type_Registration);

defaults.gpr

@@ -27,6 +27,14 @@ abstract project Defaults is
       when "asserts_enabled" | "runtime_compatible" =>
    end case;
 
+   Global_Configuration_Pragmas := "defaults_backward_compatible.adc";
+
+   case Compiler_Variant is
+      when "pro23.0w-20220202" | "pro23.0" | "pro23.1" | "pro23.2" =>
+         Global_Configuration_Pragmas := "defaults.adc";
+      when others =>
+   end case;
+
    Proof_Switches :=
    (
       "--prover=z3,cvc4,altergo",
@@ -81,9 +89,6 @@ abstract project Defaults is
       --  "-gnatwh",   --  Activate warnings on hiding.
       "-gnatwt",   --  Activate warnings for tracking of deleted conditional code.
 
-      --  ISSUE: Componolit/RecordFlux#905
-      "-gnatwR",   --  Suppress warnings on redundant constructs.
-
       --  Style Checks
       "-gnaty3",    --  Specify indentation level.
       "-gnatya",    --  Check attribute casing.

defaults_backward_compatible.adc

@@ -0,0 +1 @@
+pragma Restrictions (No_Secondary_Stack);

rflx/generator/common.py

@@ -891,7 +891,11 @@ def create_sequence_instantiation(
         element_type_identifier = ada.ID(prefix * element_type.identifier)
         sequence_context = [
             ada.WithClause(prefix * const.SCALAR_SEQUENCE_PACKAGE),
-            ada.WithClause(prefix * element_type_package),
+            *(
+                [ada.WithClause(prefix * element_type_package)]
+                if element_type_package != sequence_type.package
+                else []
+            ),
         ]
         sequence_package = ada.GenericPackageInstantiation(
             ada.ID(sequence_type.identifier.flat if flat else prefix * sequence_type.identifier),

rflx/generator/generator.py

@@ -3688,7 +3688,6 @@ def __create_refinement(self, refinement: Refinement) -> None:
             unit.declaration_context.extend(
                 [
                     WithClause(sdu_identifier),
-                    UsePackageClause(sdu_identifier),
                 ]
             )
 

rflx/generator/session.py

@@ -247,8 +247,9 @@ def _model_type(self, identifier: rid.ID) -> model.Type:
         ]
 
     def _create(self) -> None:
-        self._unit_part = self._create_state_machine()
+        state_machine = self._create_state_machine()
         self._declaration_context, self._body_context = self._create_context()
+        self._unit_part = UnitPart(body=self._create_use_clauses_body()) + state_machine
 
     def _create_context(self) -> Tuple[List[ContextItem], List[ContextItem]]:
         declaration_context: List[ContextItem] = []
@@ -273,7 +274,11 @@ def _create_context(self) -> Tuple[List[ContextItem], List[ContextItem]]:
                 type_ = self._model_type(type_identifier)
                 context.extend(
                     [
-                        WithClause(self._prefix * ID(type_.package)),
+                        *(
+                            [WithClause(self._prefix * ID(type_.package))]
+                            if type_.package != self._session.identifier.parent
+                            else []
+                        ),
                         *(
                             [
                                 WithClause(self._prefix * ID(type_.identifier)),
@@ -300,26 +305,22 @@ def _create_context(self) -> Tuple[List[ContextItem], List[ContextItem]]:
                 body_context.append(
                     WithClause(self._prefix * const.TYPES_PACKAGE),
                 )
-            body_context.append(
-                UseTypeClause(self._prefix * ID(type_identifier)),
-            )
 
-        use_type_clauses = {i for i in body_context if isinstance(i, UseTypeClause)}
         body_context = [
-            i
-            for i in body_context
-            if isinstance(i, UseTypeClause)
-            or (
-                isinstance(i, WithClause)
-                and (
-                    i not in declaration_context
-                    or any(utc.identifier.parent == i.identifier for utc in use_type_clauses)
-                )
-            )
+            i for i in body_context if isinstance(i, WithClause) and i not in declaration_context
         ]
 
         return (declaration_context, body_context)
 
+    def _create_use_clauses_body(self) -> list[Declaration]:
+        return [
+            UseTypeClause(self._prefix * ID(type_identifier))
+            for type_identifier in self._session_context.used_types_body
+            if type_identifier.parent
+            not in [INTERNAL_PACKAGE, BUILTINS_PACKAGE, self._session.identifier.parent]
+            and type_identifier not in self._session_context.used_types
+        ]
+
     def _create_state_machine(self) -> UnitPart:
         evaluated_declarations = self._evaluate_declarations(
             self._session.declarations.values(),
@@ -2978,7 +2979,9 @@ def func(expression: expr.Expr) -> expr.Expr:
             # pylint: disable = too-many-branches, too-many-return-statements
             if isinstance(expression, (expr.Relation, expr.MathBinExpr)):
                 for e in [expression.left, expression.right]:
-                    if isinstance(e.type_, (rty.Integer, rty.Enumeration)):
+                    if isinstance(e.type_, rty.Integer) or (
+                        isinstance(e.type_, rty.Enumeration) and not e.type_.always_valid
+                    ):
                         self._session_context.used_types_body.append(e.type_.identifier)
 
             if isinstance(expression, expr.MathAssExpr):

tests/integration/messages/generated/rflx-universal-contains.ads

@@ -3,7 +3,6 @@ pragma Warnings (Off, "redundant conversion");
 with RFLX.RFLX_Types;
 with RFLX.Universal.Message;
 with RFLX.Universal.Option;
-use RFLX.Universal.Option;
 
 package RFLX.Universal.Contains with
   SPARK_Mode,

tests/integration/messages/generated/rflx-universal-option_types.ads

@@ -2,7 +2,6 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.RFLX_Scalar_Sequence;
-with RFLX.Universal;
 pragma Warnings (Off, "unit ""*RFLX_Types"" is not referenced");
 with RFLX.RFLX_Types;
 pragma Warnings (On, "unit ""*RFLX_Types"" is not referenced");

tests/integration/messages/generated/rflx-universal-values.ads

@@ -2,7 +2,6 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.RFLX_Scalar_Sequence;
-with RFLX.Universal;
 pragma Warnings (Off, "unit ""*RFLX_Types"" is not referenced");
 with RFLX.RFLX_Types;
 pragma Warnings (On, "unit ""*RFLX_Types"" is not referenced");

tests/integration/messages_with_implict_size/generated/rflx-test-session.adb

@@ -1,13 +1,13 @@
 pragma Restrictions (No_Streams);
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
-with RFLX.RFLX_Types;
-use type RFLX.RFLX_Types.Bit_Length;
 
 package body RFLX.Test.Session with
   SPARK_Mode
 is
 
+   use type RFLX.RFLX_Types.Bit_Length;
+
    procedure Start (Ctx : in out Context'Class) with
      Pre =>
        Initialized (Ctx),

tests/integration/messages_with_implict_size/generated/rflx-universal-contains.ads

@@ -3,7 +3,6 @@ pragma Warnings (Off, "redundant conversion");
 with RFLX.RFLX_Types;
 with RFLX.Universal.Message;
 with RFLX.Universal.Option;
-use RFLX.Universal.Option;
 
 package RFLX.Universal.Contains with
   SPARK_Mode,

tests/integration/messages_with_implict_size/generated/rflx-universal-option_types.ads

@@ -2,7 +2,6 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.RFLX_Scalar_Sequence;
-with RFLX.Universal;
 pragma Warnings (Off, "unit ""*RFLX_Types"" is not referenced");
 with RFLX.RFLX_Types;
 pragma Warnings (On, "unit ""*RFLX_Types"" is not referenced");

tests/integration/messages_with_implict_size/generated/rflx-universal-values.ads

@@ -2,7 +2,6 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.RFLX_Scalar_Sequence;
-with RFLX.Universal;
 pragma Warnings (Off, "unit ""*RFLX_Types"" is not referenced");
 with RFLX.RFLX_Types;
 pragma Warnings (On, "unit ""*RFLX_Types"" is not referenced");

tests/integration/parameterized_messages/generated/rflx-test-session.adb

@@ -1,15 +1,13 @@
 pragma Restrictions (No_Streams);
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
-with RFLX.Test;
-with RFLX.RFLX_Types;
-use type RFLX.RFLX_Types.Bit_Length;
-use type RFLX.Test.Length;
 
 package body RFLX.Test.Session with
   SPARK_Mode
 is
 
+   use type RFLX.RFLX_Types.Bit_Length;
+
    procedure Start (Ctx : in out Context'Class) with
      Pre =>
        Initialized (Ctx),

tests/integration/parameterized_messages/generated/rflx-test-session.ads

@@ -3,7 +3,6 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
 with RFLX.Test.Session_Allocator;
 with RFLX.RFLX_Types;
-with RFLX.Test;
 with RFLX.Test.Message;
 
 package RFLX.Test.Session with

tests/integration/session_append_unconstrained/generated/rflx-test-session.adb

@@ -3,13 +3,13 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
 with RFLX.Universal.Options;
 with RFLX.Universal.Option;
-with RFLX.RFLX_Types;
-use type RFLX.RFLX_Types.Bit_Length;
 
 package body RFLX.Test.Session with
   SPARK_Mode
 is
 
+   use type RFLX.RFLX_Types.Bit_Length;
+
    procedure Start (Ctx : in out Context'Class) with
      Pre =>
        Initialized (Ctx),

tests/integration/session_append_unconstrained/generated/rflx-universal-contains.ads

@@ -3,7 +3,6 @@ pragma Warnings (Off, "redundant conversion");
 with RFLX.RFLX_Types;
 with RFLX.Universal.Message;
 with RFLX.Universal.Option;
-use RFLX.Universal.Option;
 
 package RFLX.Universal.Contains with
   SPARK_Mode,

tests/integration/session_append_unconstrained/generated/rflx-universal-option_types.ads

@@ -2,7 +2,6 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.RFLX_Scalar_Sequence;
-with RFLX.Universal;
 pragma Warnings (Off, "unit ""*RFLX_Types"" is not referenced");
 with RFLX.RFLX_Types;
 pragma Warnings (On, "unit ""*RFLX_Types"" is not referenced");

tests/integration/session_append_unconstrained/generated/rflx-universal-values.ads

@@ -2,7 +2,6 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.RFLX_Scalar_Sequence;
-with RFLX.Universal;
 pragma Warnings (Off, "unit ""*RFLX_Types"" is not referenced");
 with RFLX.RFLX_Types;
 pragma Warnings (On, "unit ""*RFLX_Types"" is not referenced");

tests/integration/session_binding/generated/rflx-test-session.adb

@@ -1,16 +1,17 @@
 pragma Restrictions (No_Streams);
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
-with RFLX.Universal;
-use type RFLX.Universal.Message_Type;
-use type RFLX.Universal.Length;
-with RFLX.RFLX_Types;
-use type RFLX.RFLX_Types.Bit_Length;
 
 package body RFLX.Test.Session with
   SPARK_Mode
 is
 
+   use type RFLX.Universal.Message_Type;
+
+   use type RFLX.Universal.Length;
+
+   use type RFLX.RFLX_Types.Bit_Length;
+
    procedure Start (Ctx : in out Context'Class) with
      Pre =>
        Initialized (Ctx),

tests/integration/session_binding/generated/rflx-universal-contains.ads

@@ -3,7 +3,6 @@ pragma Warnings (Off, "redundant conversion");
 with RFLX.RFLX_Types;
 with RFLX.Universal.Message;
 with RFLX.Universal.Option;
-use RFLX.Universal.Option;
 
 package RFLX.Universal.Contains with
   SPARK_Mode,

tests/integration/session_binding/generated/rflx-universal-option_types.ads

@@ -2,7 +2,6 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.RFLX_Scalar_Sequence;
-with RFLX.Universal;
 pragma Warnings (Off, "unit ""*RFLX_Types"" is not referenced");
 with RFLX.RFLX_Types;
 pragma Warnings (On, "unit ""*RFLX_Types"" is not referenced");

tests/integration/session_binding/generated/rflx-universal-values.ads

@@ -2,7 +2,6 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.RFLX_Scalar_Sequence;
-with RFLX.Universal;
 pragma Warnings (Off, "unit ""*RFLX_Types"" is not referenced");
 with RFLX.RFLX_Types;
 pragma Warnings (On, "unit ""*RFLX_Types"" is not referenced");

tests/integration/session_channel_multiplexing/generated/rflx-test-session.adb

@@ -1,13 +1,13 @@
 pragma Restrictions (No_Streams);
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
-with RFLX.RFLX_Types;
-use type RFLX.RFLX_Types.Bit_Length;
 
 package body RFLX.Test.Session with
   SPARK_Mode
 is
 
+   use type RFLX.RFLX_Types.Bit_Length;
+
    procedure Start (Ctx : in out Context'Class) with
      Pre =>
        Initialized (Ctx),

tests/integration/session_channel_multiplexing/generated/rflx-universal-contains.ads

@@ -3,7 +3,6 @@ pragma Warnings (Off, "redundant conversion");
 with RFLX.RFLX_Types;
 with RFLX.Universal.Message;
 with RFLX.Universal.Option;
-use RFLX.Universal.Option;
 
 package RFLX.Universal.Contains with
   SPARK_Mode,

tests/integration/session_channel_multiplexing/generated/rflx-universal-option_types.ads

@@ -2,7 +2,6 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.RFLX_Scalar_Sequence;
-with RFLX.Universal;
 pragma Warnings (Off, "unit ""*RFLX_Types"" is not referenced");
 with RFLX.RFLX_Types;
 pragma Warnings (On, "unit ""*RFLX_Types"" is not referenced");

tests/integration/session_channel_multiplexing/generated/rflx-universal-values.ads

@@ -2,7 +2,6 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.RFLX_Scalar_Sequence;
-with RFLX.Universal;
 pragma Warnings (Off, "unit ""*RFLX_Types"" is not referenced");
 with RFLX.RFLX_Types;
 pragma Warnings (On, "unit ""*RFLX_Types"" is not referenced");

tests/integration/session_channels/generated/rflx-test-session.adb

@@ -1,13 +1,13 @@
 pragma Restrictions (No_Streams);
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
-with RFLX.RFLX_Types;
-use type RFLX.RFLX_Types.Bit_Length;
 
 package body RFLX.Test.Session with
   SPARK_Mode
 is
 
+   use type RFLX.RFLX_Types.Bit_Length;
+
    procedure Start (Ctx : in out Context'Class) with
      Pre =>
        Initialized (Ctx),

tests/integration/session_channels/generated/rflx-universal-contains.ads

@@ -3,7 +3,6 @@ pragma Warnings (Off, "redundant conversion");
 with RFLX.RFLX_Types;
 with RFLX.Universal.Message;
 with RFLX.Universal.Option;
-use RFLX.Universal.Option;
 
 package RFLX.Universal.Contains with
   SPARK_Mode,

tests/integration/session_channels/generated/rflx-universal-option_types.ads

@@ -2,7 +2,6 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.RFLX_Scalar_Sequence;
-with RFLX.Universal;
 pragma Warnings (Off, "unit ""*RFLX_Types"" is not referenced");
 with RFLX.RFLX_Types;
 pragma Warnings (On, "unit ""*RFLX_Types"" is not referenced");