From cab5dd47c6da4a81d68bae620f7dca2a0c497307 Mon Sep 17 00:00:00 2001
From: Tobias Reiher <reiher@componolit.com>
Date: Thu, 22 Jul 2021 11:15:52 +0200
Subject: [PATCH] Improve check message in case of wrong instantation

Ref. #292
---
 rflx/generator/generator.py                   | 23 +++++++++++++++++++
 .../generated/rflx-derivation-message.adb     |  1 +
 .../generated/rflx-enumeration-message.adb    |  1 +
 tests/spark/generated/rflx-ethernet-frame.adb |  1 +
 .../generated/rflx-expression-message.adb     |  1 +
 .../rflx-fixed_size-simple_message.adb        |  1 +
 tests/spark/generated/rflx-icmp-message.adb   |  1 +
 tests/spark/generated/rflx-ipv4-option.adb    |  1 +
 tests/spark/generated/rflx-ipv4-packet.adb    |  1 +
 .../generated/rflx-sequence-inner_message.adb |  1 +
 .../spark/generated/rflx-sequence-message.adb |  1 +
 .../rflx-sequence-messages_message.adb        |  1 +
 ...-sequence_size_defined_by_message_size.adb |  1 +
 tests/spark/generated/rflx-tlv-message.adb    |  1 +
 tests/spark/generated/rflx-udp-datagram.adb   |  1 +
 15 files changed, 37 insertions(+)

diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py
index 63085743c..7cb452c36 100644
--- 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
index 72897513e..aaaecaa79 100644
--- 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
index 591f442f7..53219bf11 100644
--- 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
index 7a8bdbb26..6e6b9086e 100644
--- 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
index 3396ea725..7d956f5bb 100644
--- 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
index f34395eaf..bb46a1f68 100644
--- 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
index f1ec99e8c..6e0e6a22a 100644
--- 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
index 7c90c048c..aaa7a543d 100644
--- 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
index 047aa6198..9b83f3f9b 100644
--- 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
index 7b6d0564b..8fba9cdea 100644
--- 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
index bbaba2876..3ab53a5e5 100644
--- 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
index 711826c34..5ae0e517e 100644
--- 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
index 7a4427e11..7c85e359f 100644
--- 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
index 6f86da5e2..545c6e2ee 100644
--- 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
index b1421fa73..dae1e1632 100644
--- 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;