From a8aecf319aaa77429584ac8c18f556c2577616b9 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Fri, 31 Jan 2020 21:13:31 +0100 Subject: [PATCH] [Ada] Add missing Global contract to Ada.Containers.Functional_Vectors 2020-06-05 Piotr Trojanek gcc/ada/ * libgnat/a-cofuve.ads (First): Add Global contract. --- gcc/ada/libgnat/a-cofuve.ads | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 ------------------------ -- 2.30.2