diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2020-01-31 21:13:31 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-06-05 08:17:42 -0400 |
| commit | a8aecf319aaa77429584ac8c18f556c2577616b9 (patch) | |
| tree | ef3c8a4abbebd947480478a2f5fb0e63c26f63e8 /gcc | |
| parent | a9969d7feb35306ba82bc5d605d9c8c48f1c8271 (diff) | |
| download | gcc-a8aecf319aaa77429584ac8c18f556c2577616b9.zip gcc-a8aecf319aaa77429584ac8c18f556c2577616b9.tar.gz gcc-a8aecf319aaa77429584ac8c18f556c2577616b9.tar.bz2 | |
[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.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/libgnat/a-cofuve.ads | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/gcc/ada/libgnat/a-cofuve.ads b/gcc/ada/libgnat/a-cofuve.ads index 7a48a5a..cfccf1d 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 ------------------------ |