Fix contracts of abstract primitives

Ref. #1030
AdaCore · May 18, 2022 · 016b925 · 016b925
1 parent aeaaf56
commit 016b925
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 51 deletions.
diff --git a/rflx/generator/session.py b/rflx/generator/session.py
@@ -34,7 +34,6 @@
     Case,
     CaseStatement,
     ChoiceList,
-    ClassPostcondition,
     ClassPrecondition,
     CommentStatement,
     Component,
@@ -616,20 +615,9 @@ def _create_abstract_function(
                     ID(function.identifier),
                     procedure_parameters,
                 ),
-                [
-                    ClassPrecondition(
-                        And(
-                            Call("Initialized", [Variable("Ctx")]),
-                            *(
-                                [Not(Constrained("RFLX_Result"))]
-                                if isinstance(function.type_, rty.Enumeration)
-                                and function.type_.always_valid
-                                else []
-                            ),
-                        )
-                    ),
-                    ClassPostcondition(Call("Initialized", [Variable("Ctx")])),
-                ],
+                [ClassPrecondition(Not(Constrained("RFLX_Result")))]
+                if isinstance(function.type_, rty.Enumeration) and function.type_.always_valid
+                else [],
                 abstract=True,
             )
         ]
@@ -2809,7 +2797,8 @@ def _assign_to_call(  # pylint: disable = too-many-locals
 
         for i, (a, t) in enumerate(zip(call_expr.args, call_expr.argument_types)):
             if not isinstance(
-                a, (expr.Number, expr.Variable, expr.Selected, expr.Size, expr.String)
+                a,
+                (expr.Number, expr.Variable, expr.Selected, expr.Size, expr.String, expr.Aggregate),
             ) and not (
                 isinstance(a, expr.Opaque)
                 and isinstance(a.prefix, expr.Variable)

diff --git a/tests/integration/session_functions/generated/rflx-test-session.ads b/tests/integration/session_functions/generated/rflx-test-session.ads
@@ -28,22 +28,11 @@ is
 
    procedure Get_Message_Type (Ctx : in out Context; RFLX_Result : out RFLX.Universal.Option_Type) is abstract with
      Pre'Class =>
-       Initialized (Ctx)
-       and not RFLX_Result'Constrained,
-     Post'Class =>
-       Initialized (Ctx);
+       not RFLX_Result'Constrained;
 
-   procedure Create_Message (Ctx : in out Context; Message_Type : RFLX.Universal.Option_Type; Length : RFLX.Test.Length; Data : RFLX_Types.Bytes; RFLX_Result : out RFLX.Test.Definite_Message.Structure) is abstract with
-     Pre'Class =>
-       Initialized (Ctx),
-     Post'Class =>
-       Initialized (Ctx);
+   procedure Create_Message (Ctx : in out Context; Message_Type : RFLX.Universal.Option_Type; Length : RFLX.Test.Length; Data : RFLX_Types.Bytes; RFLX_Result : out RFLX.Test.Definite_Message.Structure) is abstract;
 
-   procedure Valid_Message (Ctx : in out Context; Message_Type : RFLX.Universal.Option_Type; Strict : Boolean; RFLX_Result : out RFLX.Test.Result) is abstract with
-     Pre'Class =>
-       Initialized (Ctx),
-     Post'Class =>
-       Initialized (Ctx);
+   procedure Valid_Message (Ctx : in out Context; Message_Type : RFLX.Universal.Option_Type; Strict : Boolean; RFLX_Result : out RFLX.Test.Result) is abstract;
 
    function Uninitialized (Ctx : Context'Class) return Boolean;
 

diff --git a/tests/integration/session_functions_opaque/generated/rflx-test-session.ads b/tests/integration/session_functions_opaque/generated/rflx-test-session.ads
@@ -17,11 +17,7 @@ is
          P : Private_Context;
       end record;
 
-   procedure Check_Size (Ctx : in out Context; Size : RFLX.Test.Size; Data : RFLX_Types.Bytes; RFLX_Result : out Boolean) is abstract with
-     Pre'Class =>
-       Initialized (Ctx),
-     Post'Class =>
-       Initialized (Ctx);
+   procedure Check_Size (Ctx : in out Context; Size : RFLX.Test.Size; Data : RFLX_Types.Bytes; RFLX_Result : out Boolean) is abstract;
 
    function Uninitialized (Unused_Ctx : Context'Class) return Boolean;
 

diff --git a/tests/unit/generator_test.py b/tests/unit/generator_test.py
@@ -309,14 +309,6 @@ def test_prefixed_type_identifier() -> None:
                             ada.OutParameter(["RFLX_Result"], "Boolean"),
                         ],
                     ),
-                    aspects=[
-                        ada.ClassPrecondition(
-                            ada.And(
-                                ada.Call("Initialized", [ada.Variable("Ctx")]),
-                            )
-                        ),
-                        ada.ClassPostcondition(ada.Call("Initialized", [ada.Variable("Ctx")])),
-                    ],
                     abstract=True,
                 ),
             ],
@@ -348,14 +340,6 @@ def test_prefixed_type_identifier() -> None:
                             ada.OutParameter(["RFLX_Result"], "T.Structure"),
                         ],
                     ),
-                    aspects=[
-                        ada.ClassPrecondition(
-                            ada.And(
-                                ada.Call("Initialized", [ada.Variable("Ctx")]),
-                            )
-                        ),
-                        ada.ClassPostcondition(ada.Call("Initialized", [ada.Variable("Ctx")])),
-                    ],
                     abstract=True,
                 ),
             ],