From: Piotr Trojanek <trojanek@adacore.com>
Date: Fri, 31 Jan 2020 20:13:31 +0000 (+0100)
Subject: [Ada] Add missing Global contract to Ada.Containers.Functional_Vectors
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a8aecf319aaa77429584ac8c18f556c2577616b9;p=gcc.git

[Ada] Add missing Global contract to Ada.Containers.Functional_Vectors

2020-06-05  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* libgnat/a-cofuve.ads (First): Add Global contract.
---

diff --git a/gcc/ada/libgnat/a-cofuve.ads b/gcc/ada/libgnat/a-cofuve.ads
index 7a48a5a319d..cfccf1d157f 100644
--- a/gcc/ada/libgnat/a-cofuve.ads
+++ b/gcc/ada/libgnat/a-cofuve.ads
@@ -92,7 +92,8 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
            Length (Container));
    pragma Annotate (GNATprove, Inline_For_Proof, Last);
 
-   function First return Extended_Index is (Index_Type'First);
+   function First return Extended_Index is (Index_Type'First) with
+     Global => null;
    --  First index of a sequence
 
    ------------------------