Remove workarounds for earlier GNAT Community versions

Ref. #494
AdaCore · Jun 29, 2021 · a95b15b · a95b15b
1 parent 6e0fb7c
commit a95b15b
Show file tree

Hide file tree

Showing 16 changed files with 33 additions and 1,849 deletions.
diff --git a/rflx/generator/common.py b/rflx/generator/common.py
@@ -543,23 +543,13 @@ def sufficient_space_for_field_condition(field_name: ada.Name) -> ada.Expr:
     )
 
 
-def initialize_field_statements(
-    message: model.Message, field: model.Field, prefix: str
-) -> Sequence[ada.Statement]:
+def initialize_field_statements(field: model.Field) -> Sequence[ada.Statement]:
     return [
         ada.CallStatement(
             "Reset_Dependent_Fields",
             [ada.Variable("Ctx"), ada.Variable(field.affixed_name)],
         ),
         ada.Assignment("Ctx.Message_Last", ada.Variable("Last")),
-        # WORKAROUND:
-        # Limitation of GNAT Community 2019 / SPARK Pro 20.0
-        # Provability of predicate is increased by adding part of
-        # predicate as assert
-        ada.PragmaStatement(
-            "Assert",
-            [message_structure_invariant(message, prefix)],
-        ),
         ada.Assignment(
             ada.Indexed(ada.Variable("Ctx.Cursors"), ada.Variable(field.affixed_name)),
             ada.NamedAggregate(

diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py
@@ -2055,8 +2055,9 @@ def __create_equal_function(
             ],
         )
 
+    @staticmethod
     def __create_switch_procedures(
-        self, message: Message, sequence_fields: ty.Mapping[Field, Type]
+        message: Message, sequence_fields: ty.Mapping[Field, Type]
     ) -> UnitPart:
         def specification(field: Field) -> ProcedureSpecification:
             return ProcedureSpecification(
@@ -2230,7 +2231,7 @@ def specification(field: Field) -> ProcedureSpecification:
                                         "Invalid",
                                         [Variable("Ctx"), Variable(f.affixed_name)],
                                     ),
-                                    common.initialize_field_statements(message, f, self.__prefix),
+                                    common.initialize_field_statements(f),
                                 )
                             ]
                         ),

diff --git a/rflx/generator/parser.py b/rflx/generator/parser.py
@@ -12,7 +12,6 @@
     Call,
     CallStatement,
     Case,
-    CaseStatement,
     Div,
     Equal,
     Expr,
@@ -28,7 +27,6 @@
     Mod,
     Mul,
     NamedAggregate,
-    NullStatement,
     Number,
     ObjectDeclaration,
     Old,
@@ -44,7 +42,6 @@
     Selected,
     Size,
     Slice,
-    Statement,
     String,
     Subprogram,
     SubprogramBody,
@@ -177,8 +174,8 @@ def result(field: Field, message: Message) -> NamedAggregate:
             ],
         )
 
+    @staticmethod
     def create_verify_procedure(
-        self,
         message: Message,
         scalar_fields: Mapping[Field, Scalar],
         composite_fields: Sequence[Field],
@@ -248,43 +245,43 @@ def create_verify_procedure(
                 [
                     (
                         Call("Composite_Field", [Variable("Fld")]),
-                        [set_context_cursor_composite(scalar_fields, composite_fields)],
+                        [set_context_cursor_composite_field("Fld")],
                     )
                 ],
                 [set_context_cursor_scalar()],
             )
             if scalar_fields and composite_fields
             else set_context_cursor_scalar()
             if scalar_fields and not composite_fields
-            else set_context_cursor_composite(scalar_fields, composite_fields),
-            # WORKAROUND:
-            # Limitation of GNAT Community 2019 / SPARK Pro 20.0
-            # Provability of predicate is increased by adding part of
-            # predicate as assert
-            PragmaStatement("Assert", [common.message_structure_invariant(message, self.prefix)]),
-            # WORKAROUND:
-            # Limitation of GNAT Community 2019 / SPARK Pro 20.0
-            # Provability of predicate is increased by splitting
-            # assignment in multiple statements
-            IfStatement(
+            else set_context_cursor_composite_field("Fld"),
+            *(
                 [
-                    (
-                        Equal(Variable("Fld"), Variable(f.affixed_name)),
+                    # ISSUE: Componolit/RecordFlux#664
+                    # The provability of the context predicate is increased by splitting the
+                    # assignment into multiple statements.
+                    IfStatement(
                         [
-                            Assignment(
-                                Indexed(
-                                    Variable("Ctx.Cursors"),
-                                    Call("Successor", [Variable("Ctx"), Variable("Fld")]),
-                                ),
-                                NamedAggregate(
-                                    ("State", Variable("S_Invalid")),
-                                    ("Predecessor", Variable("Fld")),
-                                ),
+                            (
+                                Equal(Variable("Fld"), Variable(f.affixed_name)),
+                                [
+                                    Assignment(
+                                        Indexed(
+                                            Variable("Ctx.Cursors"),
+                                            Call("Successor", [Variable("Ctx"), Variable("Fld")]),
+                                        ),
+                                        NamedAggregate(
+                                            ("State", Variable("S_Invalid")),
+                                            ("Predecessor", Variable("Fld")),
+                                        ),
+                                    )
+                                ],
                             )
-                        ],
+                            for f in message.fields
+                        ]
                     )
-                    for f in message.fields
                 ]
+                if len(message.fields) > 1
+                else []
             ),
         ]
 
@@ -826,32 +823,6 @@ def set_context_cursor_scalar() -> Assignment:
     )
 
 
-def set_context_cursor_composite(
-    scalar_fields: Mapping[Field, Scalar], composite_fields: Sequence[Field]
-) -> Statement:
-    # WORKAROUND:
-    # Limitation of GNAT Community 2020
-    # The provability of the predicate of `Ctx` is increased by
-    # duplicating the assignment inside of a case statement.
-    return (
-        CaseStatement(
-            Variable("Fld"),
-            [
-                *[
-                    (
-                        Variable(f.affixed_name),
-                        [set_context_cursor_composite_field(f.affixed_name)],
-                    )
-                    for f in composite_fields
-                ],
-                *([(Variable("others"), [NullStatement()])] if scalar_fields else []),
-            ],
-        )
-        if len(composite_fields) > 1
-        else set_context_cursor_composite_field("Fld")
-    )
-
-
 def set_context_cursor_composite_field(field_name: str) -> Assignment:
     return Assignment(
         Indexed(

diff --git a/rflx/generator/serializer.py b/rflx/generator/serializer.py
@@ -772,7 +772,7 @@ def specification_public(field: Field) -> ProcedureSpecification:
                     SubprogramBody(
                         specification_private(f),
                         common.field_bit_location_declarations(Variable(f.affixed_name)),
-                        common.initialize_field_statements(message, f, self.prefix),
+                        common.initialize_field_statements(f),
                         [
                             Precondition(
                                 AndThen(

diff --git a/tests/spark/generated/rflx-enumeration-generic_message.adb b/tests/spark/generated/rflx-enumeration-generic_message.adb
@@ -160,15 +160,6 @@ is
                                   Field_Last (Ctx, Fld) mod Types.Byte'Size = 0));
                Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
                Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
-               pragma Assert ((if
-                                  Structural_Valid (Ctx.Cursors (F_Priority))
-                               then
-                                  Ctx.Cursors (F_Priority).Last - Ctx.Cursors (F_Priority).First + 1 = RFLX.Enumeration.Priority_Base'Size
-                                  and then Ctx.Cursors (F_Priority).Predecessor = F_Initial
-                                  and then Ctx.Cursors (F_Priority).First = Ctx.First));
-               if Fld = F_Priority then
-                  Ctx.Cursors (Successor (Ctx, Fld)) := (State => S_Invalid, Predecessor => Fld);
-               end if;
             else
                Ctx.Cursors (Fld) := (State => S_Invalid, Predecessor => F_Final);
             end if;