Improve check message in case of wrong instantation

Ref. #292
AdaCore · Jul 27, 2021 · cab5dd4 · cab5dd4
1 parent 7e34e6f
commit cab5dd4
Show file tree

Hide file tree

Showing 15 changed files with 37 additions and 0 deletions.
diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py
@@ -1265,6 +1265,29 @@ def __create_write_procedure() -> UnitPart:
                                 Variable("Length"),
                             ],
                         ),
+                        # ISSUE: Componolit/Workarounds#39
+                        # Improve the check message in case of a wrong instantiation of "Write".
+                        PragmaStatement(
+                            "Assert",
+                            [
+                                LessEqual(
+                                    Variable("Length"),
+                                    Length(
+                                        Indexed(
+                                            Variable("Ctx.Buffer.all"),
+                                            ValueRange(
+                                                Call(const.TYPES_TO_INDEX, [Variable("Ctx.First")]),
+                                                Call(const.TYPES_TO_INDEX, [Variable("Ctx.Last")]),
+                                            ),
+                                        )
+                                    ),
+                                ),
+                                String(
+                                    "Length <= Buffer'Length is not ensured by postcondition of"
+                                    ' "Write"'
+                                ),
+                            ],
+                        ),
                         CallStatement(
                             "Reset",
                             [

diff --git a/tests/spark/generated/rflx-derivation-message.adb b/tests/spark/generated/rflx-derivation-message.adb
@@ -53,6 +53,7 @@ is
       Length : RFLX_Types.Length;
    begin
       Write (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last)), Length);
+      pragma Assert (Length <= Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last))'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
       Reset (Ctx, Ctx.First, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (RFLX_Types.To_Index (Ctx.First)) + Length - 1));
    end Write;
 

diff --git a/tests/spark/generated/rflx-enumeration-message.adb b/tests/spark/generated/rflx-enumeration-message.adb
@@ -53,6 +53,7 @@ is
       Length : RFLX_Types.Length;
    begin
       Write (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last)), Length);
+      pragma Assert (Length <= Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last))'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
       Reset (Ctx, Ctx.First, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (RFLX_Types.To_Index (Ctx.First)) + Length - 1));
    end Write;
 

diff --git a/tests/spark/generated/rflx-ethernet-frame.adb b/tests/spark/generated/rflx-ethernet-frame.adb
@@ -53,6 +53,7 @@ is
       Length : RFLX_Types.Length;
    begin
       Write (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last)), Length);
+      pragma Assert (Length <= Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last))'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
       Reset (Ctx, Ctx.First, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (RFLX_Types.To_Index (Ctx.First)) + Length - 1));
    end Write;
 

diff --git a/tests/spark/generated/rflx-expression-message.adb b/tests/spark/generated/rflx-expression-message.adb
@@ -53,6 +53,7 @@ is
       Length : RFLX_Types.Length;
    begin
       Write (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last)), Length);
+      pragma Assert (Length <= Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last))'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
       Reset (Ctx, Ctx.First, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (RFLX_Types.To_Index (Ctx.First)) + Length - 1));
    end Write;
 

diff --git a/tests/spark/generated/rflx-fixed_size-simple_message.adb b/tests/spark/generated/rflx-fixed_size-simple_message.adb
@@ -53,6 +53,7 @@ is
       Length : RFLX_Types.Length;
    begin
       Write (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last)), Length);
+      pragma Assert (Length <= Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last))'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
       Reset (Ctx, Ctx.First, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (RFLX_Types.To_Index (Ctx.First)) + Length - 1));
    end Write;
 

diff --git a/tests/spark/generated/rflx-icmp-message.adb b/tests/spark/generated/rflx-icmp-message.adb
@@ -53,6 +53,7 @@ is
       Length : RFLX_Types.Length;
    begin
       Write (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last)), Length);
+      pragma Assert (Length <= Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last))'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
       Reset (Ctx, Ctx.First, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (RFLX_Types.To_Index (Ctx.First)) + Length - 1));
    end Write;
 

diff --git a/tests/spark/generated/rflx-ipv4-option.adb b/tests/spark/generated/rflx-ipv4-option.adb
@@ -53,6 +53,7 @@ is
       Length : RFLX_Types.Length;
    begin
       Write (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last)), Length);
+      pragma Assert (Length <= Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last))'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
       Reset (Ctx, Ctx.First, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (RFLX_Types.To_Index (Ctx.First)) + Length - 1));
    end Write;
 

diff --git a/tests/spark/generated/rflx-ipv4-packet.adb b/tests/spark/generated/rflx-ipv4-packet.adb
@@ -53,6 +53,7 @@ is
       Length : RFLX_Types.Length;
    begin
       Write (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last)), Length);
+      pragma Assert (Length <= Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last))'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
       Reset (Ctx, Ctx.First, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (RFLX_Types.To_Index (Ctx.First)) + Length - 1));
    end Write;
 

diff --git a/tests/spark/generated/rflx-sequence-inner_message.adb b/tests/spark/generated/rflx-sequence-inner_message.adb
@@ -53,6 +53,7 @@ is
       Length : RFLX_Types.Length;
    begin
       Write (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last)), Length);
+      pragma Assert (Length <= Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last))'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
       Reset (Ctx, Ctx.First, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (RFLX_Types.To_Index (Ctx.First)) + Length - 1));
    end Write;
 

diff --git a/tests/spark/generated/rflx-sequence-message.adb b/tests/spark/generated/rflx-sequence-message.adb
@@ -53,6 +53,7 @@ is
       Length : RFLX_Types.Length;
    begin
       Write (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last)), Length);
+      pragma Assert (Length <= Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last))'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
       Reset (Ctx, Ctx.First, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (RFLX_Types.To_Index (Ctx.First)) + Length - 1));
    end Write;
 

diff --git a/tests/spark/generated/rflx-sequence-messages_message.adb b/tests/spark/generated/rflx-sequence-messages_message.adb
@@ -53,6 +53,7 @@ is
       Length : RFLX_Types.Length;
    begin
       Write (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last)), Length);
+      pragma Assert (Length <= Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last))'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
       Reset (Ctx, Ctx.First, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (RFLX_Types.To_Index (Ctx.First)) + Length - 1));
    end Write;
 

diff --git a/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.adb b/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.adb
@@ -53,6 +53,7 @@ is
       Length : RFLX_Types.Length;
    begin
       Write (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last)), Length);
+      pragma Assert (Length <= Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last))'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
       Reset (Ctx, Ctx.First, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (RFLX_Types.To_Index (Ctx.First)) + Length - 1));
    end Write;
 

diff --git a/tests/spark/generated/rflx-tlv-message.adb b/tests/spark/generated/rflx-tlv-message.adb
@@ -53,6 +53,7 @@ is
       Length : RFLX_Types.Length;
    begin
       Write (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last)), Length);
+      pragma Assert (Length <= Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last))'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
       Reset (Ctx, Ctx.First, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (RFLX_Types.To_Index (Ctx.First)) + Length - 1));
    end Write;
 

diff --git a/tests/spark/generated/rflx-udp-datagram.adb b/tests/spark/generated/rflx-udp-datagram.adb
@@ -53,6 +53,7 @@ is
       Length : RFLX_Types.Length;
    begin
       Write (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last)), Length);
+      pragma Assert (Length <= Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Last))'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
       Reset (Ctx, Ctx.First, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (RFLX_Types.To_Index (Ctx.First)) + Length - 1));
    end Write;