While annotating Ada.Containers.Functional_Vectors unit with
Global/Pre/Post contracts we omitted its First function. This was most
likely because it is an expression function and we though that Global
will be generated, while Pre/Post will be effectively provided by
inlining.
However, GNATprove still emits a warning on calls to First about
assuming Global to be null, just like it does for any predefined
subprogram without an explicit Global/Depends/Pure contracts.
There is no impact on compilation, so no test provided.
Tested on x86_64-pc-linux-gnu, committed on trunk
2020-06-05 Piotr Trojanek <troja...@adacore.com>
gcc/ada/
* libgnat/a-cofuve.ads (First): Add Global contract.--- gcc/ada/libgnat/a-cofuve.ads
+++ 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
------------------------
