Improve size functions

Ref. #908
AdaCore · May 18, 2022 · 781f738 · 781f738
1 parent 016b925
commit 781f738
Show file tree

Hide file tree

Showing 115 changed files with 406 additions and 842 deletions.
diff --git a/rflx/generator/message.py b/rflx/generator/message.py
@@ -2024,24 +2024,13 @@ def create_size_function() -> UnitPart:
                 ],
             )
         ],
-        [
+        private=[
             ExpressionFunctionDeclaration(
                 specification,
-                If(
-                    [
-                        (
-                            Equal(
-                                Variable("Ctx.Verified_Last"),
-                                Sub(Variable("Ctx.First"), Number(1)),
-                            ),
-                            Number(0),
-                        )
-                    ],
-                    Add(
-                        Variable("Ctx.Verified_Last"),
-                        -Variable("Ctx.First"),
-                        Number(1),
-                    ),
+                Add(
+                    Variable("Ctx.Verified_Last"),
+                    -Variable("Ctx.First"),
+                    Number(1),
                 ),
             )
         ],
@@ -2057,38 +2046,12 @@ def create_byte_size_function() -> UnitPart:
         [
             SubprogramDeclaration(
                 specification,
-                [
-                    Postcondition(
-                        Equal(
-                            Result("Byte_Size"),
-                            Call(const.TYPES_TO_LENGTH, [Call("Size", [Variable("Ctx")])]),
-                        )
-                    ),
-                ],
             )
         ],
-        [
+        private=[
             ExpressionFunctionDeclaration(
                 specification,
-                If(
-                    [
-                        (
-                            Equal(
-                                Variable("Ctx.Verified_Last"),
-                                Sub(Variable("Ctx.First"), Number(1)),
-                            ),
-                            Number(0),
-                        )
-                    ],
-                    Indexed(
-                        Variable(const.TYPES_LENGTH),
-                        Add(
-                            Call(const.TYPES_TO_INDEX, [Variable("Ctx.Verified_Last")]),
-                            -Call(const.TYPES_TO_INDEX, [Variable("Ctx.First")]),
-                            Number(1),
-                        ),
-                    ),
-                ),
+                Call(const.TYPES_TO_LENGTH, [Call("Size", [Variable("Ctx")])]),
             )
         ],
     )

diff --git a/tests/integration/messages/generated/rflx-universal-message.adb b/tests/integration/messages/generated/rflx-universal-message.adb
@@ -62,17 +62,6 @@ is
       Ctx.Written_Last := RFLX_Types.Bit_Index'Max (Ctx.Written_Last, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (Ctx.Buffer_First) + Offset + Length - 1));
    end Generic_Write;
 
-   function Size (Ctx : Context) return RFLX_Types.Bit_Length is
-     ((if Ctx.Verified_Last = Ctx.First - 1 then 0 else Ctx.Verified_Last - Ctx.First + 1));
-
-   function Byte_Size (Ctx : Context) return RFLX_Types.Length is
-     ((if
-          Ctx.Verified_Last = Ctx.First - 1
-       then
-          0
-       else
-          RFLX_Types.Length (RFLX_Types.To_Index (Ctx.Verified_Last) - RFLX_Types.To_Index (Ctx.First) + 1)));
-
    procedure Data (Ctx : Context; Data : out RFLX_Types.Bytes) is
    begin
       Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last));

diff --git a/tests/integration/messages/generated/rflx-universal-message.ads b/tests/integration/messages/generated/rflx-universal-message.ads
@@ -225,9 +225,7 @@ is
      Post =>
        Size'Result rem RFLX_Types.Byte'Size = 0;
 
-   function Byte_Size (Ctx : Context) return RFLX_Types.Length with
-     Post =>
-       Byte_Size'Result = RFLX_Types.To_Length (Size (Ctx));
+   function Byte_Size (Ctx : Context) return RFLX_Types.Length;
 
    function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length with
      Pre =>
@@ -1346,6 +1344,12 @@ private
    function Buffer_Length (Ctx : Context) return RFLX_Types.Length is
      (Ctx.Buffer'Length);
 
+   function Size (Ctx : Context) return RFLX_Types.Bit_Length is
+     (Ctx.Verified_Last - Ctx.First + 1);
+
+   function Byte_Size (Ctx : Context) return RFLX_Types.Length is
+     (RFLX_Types.To_Length (Size (Ctx)));
+
    function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length is
      (Ctx.Verified_Last);
 

diff --git a/tests/integration/messages/generated/rflx-universal-option.adb b/tests/integration/messages/generated/rflx-universal-option.adb
@@ -62,17 +62,6 @@ is
       Ctx.Written_Last := RFLX_Types.Bit_Index'Max (Ctx.Written_Last, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (Ctx.Buffer_First) + Offset + Length - 1));
    end Generic_Write;
 
-   function Size (Ctx : Context) return RFLX_Types.Bit_Length is
-     ((if Ctx.Verified_Last = Ctx.First - 1 then 0 else Ctx.Verified_Last - Ctx.First + 1));
-
-   function Byte_Size (Ctx : Context) return RFLX_Types.Length is
-     ((if
-          Ctx.Verified_Last = Ctx.First - 1
-       then
-          0
-       else
-          RFLX_Types.Length (RFLX_Types.To_Index (Ctx.Verified_Last) - RFLX_Types.To_Index (Ctx.First) + 1)));
-
    procedure Data (Ctx : Context; Data : out RFLX_Types.Bytes) is
    begin
       Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last));

diff --git a/tests/integration/messages/generated/rflx-universal-option.ads b/tests/integration/messages/generated/rflx-universal-option.ads
@@ -222,9 +222,7 @@ is
      Post =>
        Size'Result rem RFLX_Types.Byte'Size = 0;
 
-   function Byte_Size (Ctx : Context) return RFLX_Types.Length with
-     Post =>
-       Byte_Size'Result = RFLX_Types.To_Length (Size (Ctx));
+   function Byte_Size (Ctx : Context) return RFLX_Types.Length;
 
    function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length with
      Pre =>
@@ -715,6 +713,12 @@ private
    function Buffer_Length (Ctx : Context) return RFLX_Types.Length is
      (Ctx.Buffer'Length);
 
+   function Size (Ctx : Context) return RFLX_Types.Bit_Length is
+     (Ctx.Verified_Last - Ctx.First + 1);
+
+   function Byte_Size (Ctx : Context) return RFLX_Types.Length is
+     (RFLX_Types.To_Length (Size (Ctx)));
+
    function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length is
      (Ctx.Verified_Last);
 

diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-message.adb b/tests/integration/messages_with_implict_size/generated/rflx-universal-message.adb
@@ -62,17 +62,6 @@ is
       Ctx.Written_Last := RFLX_Types.Bit_Index'Max (Ctx.Written_Last, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (Ctx.Buffer_First) + Offset + Length - 1));
    end Generic_Write;
 
-   function Size (Ctx : Context) return RFLX_Types.Bit_Length is
-     ((if Ctx.Verified_Last = Ctx.First - 1 then 0 else Ctx.Verified_Last - Ctx.First + 1));
-
-   function Byte_Size (Ctx : Context) return RFLX_Types.Length is
-     ((if
-          Ctx.Verified_Last = Ctx.First - 1
-       then
-          0
-       else
-          RFLX_Types.Length (RFLX_Types.To_Index (Ctx.Verified_Last) - RFLX_Types.To_Index (Ctx.First) + 1)));
-
    procedure Data (Ctx : Context; Data : out RFLX_Types.Bytes) is
    begin
       Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last));

diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads b/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads
@@ -225,9 +225,7 @@ is
      Post =>
        Size'Result rem RFLX_Types.Byte'Size = 0;
 
-   function Byte_Size (Ctx : Context) return RFLX_Types.Length with
-     Post =>
-       Byte_Size'Result = RFLX_Types.To_Length (Size (Ctx));
+   function Byte_Size (Ctx : Context) return RFLX_Types.Length;
 
    function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length with
      Pre =>
@@ -1346,6 +1344,12 @@ private
    function Buffer_Length (Ctx : Context) return RFLX_Types.Length is
      (Ctx.Buffer'Length);
 
+   function Size (Ctx : Context) return RFLX_Types.Bit_Length is
+     (Ctx.Verified_Last - Ctx.First + 1);
+
+   function Byte_Size (Ctx : Context) return RFLX_Types.Length is
+     (RFLX_Types.To_Length (Size (Ctx)));
+
    function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length is
      (Ctx.Verified_Last);
 

diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-option.adb b/tests/integration/messages_with_implict_size/generated/rflx-universal-option.adb
@@ -62,17 +62,6 @@ is
       Ctx.Written_Last := RFLX_Types.Bit_Index'Max (Ctx.Written_Last, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (Ctx.Buffer_First) + Offset + Length - 1));
    end Generic_Write;
 
-   function Size (Ctx : Context) return RFLX_Types.Bit_Length is
-     ((if Ctx.Verified_Last = Ctx.First - 1 then 0 else Ctx.Verified_Last - Ctx.First + 1));
-
-   function Byte_Size (Ctx : Context) return RFLX_Types.Length is
-     ((if
-          Ctx.Verified_Last = Ctx.First - 1
-       then
-          0
-       else
-          RFLX_Types.Length (RFLX_Types.To_Index (Ctx.Verified_Last) - RFLX_Types.To_Index (Ctx.First) + 1)));
-
    procedure Data (Ctx : Context; Data : out RFLX_Types.Bytes) is
    begin
       Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last));

diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads b/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads
@@ -222,9 +222,7 @@ is
      Post =>
        Size'Result rem RFLX_Types.Byte'Size = 0;
 
-   function Byte_Size (Ctx : Context) return RFLX_Types.Length with
-     Post =>
-       Byte_Size'Result = RFLX_Types.To_Length (Size (Ctx));
+   function Byte_Size (Ctx : Context) return RFLX_Types.Length;
 
    function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length with
      Pre =>
@@ -715,6 +713,12 @@ private
    function Buffer_Length (Ctx : Context) return RFLX_Types.Length is
      (Ctx.Buffer'Length);
 
+   function Size (Ctx : Context) return RFLX_Types.Bit_Length is
+     (Ctx.Verified_Last - Ctx.First + 1);
+
+   function Byte_Size (Ctx : Context) return RFLX_Types.Length is
+     (RFLX_Types.To_Length (Size (Ctx)));
+
    function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length is
      (Ctx.Verified_Last);
 

diff --git a/tests/integration/messages_with_single_opaque_field/generated/rflx-test-message.adb b/tests/integration/messages_with_single_opaque_field/generated/rflx-test-message.adb
@@ -62,17 +62,6 @@ is
       Ctx.Written_Last := RFLX_Types.Bit_Index'Max (Ctx.Written_Last, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (Ctx.Buffer_First) + Offset + Length - 1));
    end Generic_Write;
 
-   function Size (Ctx : Context) return RFLX_Types.Bit_Length is
-     ((if Ctx.Verified_Last = Ctx.First - 1 then 0 else Ctx.Verified_Last - Ctx.First + 1));
-
-   function Byte_Size (Ctx : Context) return RFLX_Types.Length is
-     ((if
-          Ctx.Verified_Last = Ctx.First - 1
-       then
-          0
-       else
-          RFLX_Types.Length (RFLX_Types.To_Index (Ctx.Verified_Last) - RFLX_Types.To_Index (Ctx.First) + 1)));
-
    procedure Data (Ctx : Context; Data : out RFLX_Types.Bytes) is
    begin
       Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last));

diff --git a/tests/integration/messages_with_single_opaque_field/generated/rflx-test-message.ads b/tests/integration/messages_with_single_opaque_field/generated/rflx-test-message.ads
@@ -222,9 +222,7 @@ is
      Post =>
        Size'Result rem RFLX_Types.Byte'Size = 0;
 
-   function Byte_Size (Ctx : Context) return RFLX_Types.Length with
-     Post =>
-       Byte_Size'Result = RFLX_Types.To_Length (Size (Ctx));
+   function Byte_Size (Ctx : Context) return RFLX_Types.Length;
 
    function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length with
      Pre =>
@@ -614,6 +612,12 @@ private
    function Buffer_Length (Ctx : Context) return RFLX_Types.Length is
      (Ctx.Buffer'Length);
 
+   function Size (Ctx : Context) return RFLX_Types.Bit_Length is
+     (Ctx.Verified_Last - Ctx.First + 1);
+
+   function Byte_Size (Ctx : Context) return RFLX_Types.Length is
+     (RFLX_Types.To_Length (Size (Ctx)));
+
    function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length is
      (Ctx.Verified_Last);
 

diff --git a/tests/integration/parameterized_messages/generated/rflx-test-message.adb b/tests/integration/parameterized_messages/generated/rflx-test-message.adb
@@ -62,17 +62,6 @@ is
       Ctx.Written_Last := RFLX_Types.Bit_Index'Max (Ctx.Written_Last, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (Ctx.Buffer_First) + Offset + Length - 1));
    end Generic_Write;
 
-   function Size (Ctx : Context) return RFLX_Types.Bit_Length is
-     ((if Ctx.Verified_Last = Ctx.First - 1 then 0 else Ctx.Verified_Last - Ctx.First + 1));
-
-   function Byte_Size (Ctx : Context) return RFLX_Types.Length is
-     ((if
-          Ctx.Verified_Last = Ctx.First - 1
-       then
-          0
-       else
-          RFLX_Types.Length (RFLX_Types.To_Index (Ctx.Verified_Last) - RFLX_Types.To_Index (Ctx.First) + 1)));
-
    procedure Data (Ctx : Context; Data : out RFLX_Types.Bytes) is
    begin
       Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last));

diff --git a/tests/integration/parameterized_messages/generated/rflx-test-message.ads b/tests/integration/parameterized_messages/generated/rflx-test-message.ads
@@ -233,9 +233,7 @@ is
      Post =>
        Size'Result rem RFLX_Types.Byte'Size = 0;
 
-   function Byte_Size (Ctx : Context) return RFLX_Types.Length with
-     Post =>
-       Byte_Size'Result = RFLX_Types.To_Length (Size (Ctx));
+   function Byte_Size (Ctx : Context) return RFLX_Types.Length;
 
    function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length with
      Pre =>
@@ -742,6 +740,12 @@ private
    function Buffer_Length (Ctx : Context) return RFLX_Types.Length is
      (Ctx.Buffer'Length);
 
+   function Size (Ctx : Context) return RFLX_Types.Bit_Length is
+     (Ctx.Verified_Last - Ctx.First + 1);
+
+   function Byte_Size (Ctx : Context) return RFLX_Types.Length is
+     (RFLX_Types.To_Length (Size (Ctx)));
+
    function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length is
      (Ctx.Verified_Last);
 

diff --git a/tests/integration/session_append_unconstrained/generated/rflx-universal-message.adb b/tests/integration/session_append_unconstrained/generated/rflx-universal-message.adb
@@ -62,17 +62,6 @@ is
       Ctx.Written_Last := RFLX_Types.Bit_Index'Max (Ctx.Written_Last, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (Ctx.Buffer_First) + Offset + Length - 1));
    end Generic_Write;
 
-   function Size (Ctx : Context) return RFLX_Types.Bit_Length is
-     ((if Ctx.Verified_Last = Ctx.First - 1 then 0 else Ctx.Verified_Last - Ctx.First + 1));
-
-   function Byte_Size (Ctx : Context) return RFLX_Types.Length is
-     ((if
-          Ctx.Verified_Last = Ctx.First - 1
-       then
-          0
-       else
-          RFLX_Types.Length (RFLX_Types.To_Index (Ctx.Verified_Last) - RFLX_Types.To_Index (Ctx.First) + 1)));
-
    procedure Data (Ctx : Context; Data : out RFLX_Types.Bytes) is
    begin
       Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last));

diff --git a/tests/integration/session_append_unconstrained/generated/rflx-universal-message.ads b/tests/integration/session_append_unconstrained/generated/rflx-universal-message.ads
@@ -225,9 +225,7 @@ is
      Post =>
        Size'Result rem RFLX_Types.Byte'Size = 0;
 
-   function Byte_Size (Ctx : Context) return RFLX_Types.Length with
-     Post =>
-       Byte_Size'Result = RFLX_Types.To_Length (Size (Ctx));
+   function Byte_Size (Ctx : Context) return RFLX_Types.Length;
 
    function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length with
      Pre =>
@@ -1346,6 +1344,12 @@ private
    function Buffer_Length (Ctx : Context) return RFLX_Types.Length is
      (Ctx.Buffer'Length);
 
+   function Size (Ctx : Context) return RFLX_Types.Bit_Length is
+     (Ctx.Verified_Last - Ctx.First + 1);
+
+   function Byte_Size (Ctx : Context) return RFLX_Types.Length is
+     (RFLX_Types.To_Length (Size (Ctx)));
+
    function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length is
      (Ctx.Verified_Last);
 

diff --git a/tests/integration/session_append_unconstrained/generated/rflx-universal-option.adb b/tests/integration/session_append_unconstrained/generated/rflx-universal-option.adb
@@ -62,17 +62,6 @@ is
       Ctx.Written_Last := RFLX_Types.Bit_Index'Max (Ctx.Written_Last, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (Ctx.Buffer_First) + Offset + Length - 1));
    end Generic_Write;
 
-   function Size (Ctx : Context) return RFLX_Types.Bit_Length is
-     ((if Ctx.Verified_Last = Ctx.First - 1 then 0 else Ctx.Verified_Last - Ctx.First + 1));
-
-   function Byte_Size (Ctx : Context) return RFLX_Types.Length is
-     ((if
-          Ctx.Verified_Last = Ctx.First - 1
-       then
-          0
-       else
-          RFLX_Types.Length (RFLX_Types.To_Index (Ctx.Verified_Last) - RFLX_Types.To_Index (Ctx.First) + 1)));
-
    procedure Data (Ctx : Context; Data : out RFLX_Types.Bytes) is
    begin
       Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last));