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

Message ID 20200605122338.GA56663@adacore.com
State New
Headers show
Series
  • [Ada] Add missing Global contract to Ada.Containers.Functional_Vectors
Related show

Commit Message

Pierre-Marie de Rodat June 5, 2020, 12:23 p.m.
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  <trojanek@adacore.com>

gcc/ada/

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

Patch

--- 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
 
    ------------------------