Restrict copying to valid sequences

Ref. #292
AdaCore · Mar 31, 2021 · 56f6d9a · 56f6d9a
1 parent 723e5f6
commit 56f6d9a
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 0 deletions.
diff --git a/rflx/templates/rflx_message_sequence.ads b/rflx/templates/rflx_message_sequence.ads
@@ -103,6 +103,7 @@ is
    procedure Copy (Ctx : Context; Buffer : out Types.Bytes) with
      Pre =>
        (Has_Buffer (Ctx)
+        and Valid (Ctx)
         and Byte_Size (Ctx) = Buffer'Length);
 
    function Has_Element (Ctx : Context) return Boolean with

diff --git a/rflx/templates/rflx_scalar_sequence.ads b/rflx/templates/rflx_scalar_sequence.ads
@@ -97,6 +97,7 @@ is
    procedure Copy (Ctx : Context; Buffer : out Types.Bytes) with
      Pre =>
        (Has_Buffer (Ctx)
+        and Valid (Ctx)
         and Byte_Size (Ctx) = Buffer'Length);
 
    procedure Next (Ctx : in out Context) with

diff --git a/tests/spark/generated/rflx-rflx_message_sequence.ads b/tests/spark/generated/rflx-rflx_message_sequence.ads
@@ -103,6 +103,7 @@ is
    procedure Copy (Ctx : Context; Buffer : out Types.Bytes) with
      Pre =>
        (Has_Buffer (Ctx)
+        and Valid (Ctx)
         and Byte_Size (Ctx) = Buffer'Length);
 
    function Has_Element (Ctx : Context) return Boolean with

diff --git a/tests/spark/generated/rflx-rflx_scalar_sequence.ads b/tests/spark/generated/rflx-rflx_scalar_sequence.ads
@@ -97,6 +97,7 @@ is
    procedure Copy (Ctx : Context; Buffer : out Types.Bytes) with
      Pre =>
        (Has_Buffer (Ctx)
+        and Valid (Ctx)
         and Byte_Size (Ctx) = Buffer'Length);
 
    procedure Next (Ctx : in out Context) with