[gcc(refs/users/guojiufu/heads/guojiufu-branch)] [Ada] Add Depends contracts to Delete procedures of formal containers

[gcc(refs/users/guojiufu/heads/guojiufu-branch)] [Ada] Add Depends contracts to Delete procedures of formal containers

[Jiu Fu Guo]

https://gcc.gnu.org/g:54c1fdb62b647c1dedf6d58d260ed85e93e0af20

commit 54c1fdb62b647c1dedf6d58d260ed85e93e0af20
Author: Claire Dross <dross@adacore.com>
Date:   Mon Feb 10 12:30:40 2020 +0100

    [Ada] Add Depends contracts to Delete procedures of formal containers
    
    2020-06-08  Claire Dross  <dross@adacore.com>
    
    gcc/ada/
    
            * libgnat/a-cfdlli.ads, libgnat/a-cfhama.ads,
            libgnat/a-cfhase.ads, libgnat/a-cforma.ads, libgnat/a-cforse.ads
            (Delete): Add Depends contract.

Diff:
---
 gcc/ada/libgnat/a-cfdlli.ads | 7 ++++---
 gcc/ada/libgnat/a-cfhama.ads | 7 ++++---
 gcc/ada/libgnat/a-cfhase.ads | 7 ++++---
 gcc/ada/libgnat/a-cforma.ads | 7 ++++---
 gcc/ada/libgnat/a-cforse.ads | 7 ++++---
 5 files changed, 20 insertions(+), 15 deletions(-)

diff --git a/gcc/ada/libgnat/a-cfdlli.ads b/gcc/ada/libgnat/a-cfdlli.ads
index 426a5848df4..61312396c63 100644
--- a/gcc/ada/libgnat/a-cfdlli.ads
+++ b/gcc/ada/libgnat/a-cfdlli.ads
@@ -789,9 +789,10 @@ is
                 Count => Count);
 
    procedure Delete (Container : in out List; Position : in out Cursor) with
-     Global => null,
-     Pre    => Has_Element (Container, Position),
-     Post   =>
+     Global  => null,
+     Depends => (Container =>+ Position, Position => null),
+     Pre     => Has_Element (Container, Position),
+     Post    =>
        Length (Container) = Length (Container)'Old - 1
 
          --  Position is set to No_Element
diff --git a/gcc/ada/libgnat/a-cfhama.ads b/gcc/ada/libgnat/a-cfhama.ads
index 7b500961d9e..8a735089577 100644
--- a/gcc/ada/libgnat/a-cfhama.ads
+++ b/gcc/ada/libgnat/a-cfhama.ads
@@ -669,9 +669,10 @@ is
                 Find (Container, Key)'Old);
 
    procedure Delete (Container : in out Map; Position : in out Cursor) with
-     Global => null,
-     Pre    => Has_Element (Container, Position),
-     Post   =>
+     Global  => null,
+     Depends => (Container =>+ Position, Position => null),
+     Pre     => Has_Element (Container, Position),
+     Post    =>
        Position = No_Element
          and Length (Container) = Length (Container)'Old - 1
 
diff --git a/gcc/ada/libgnat/a-cfhase.ads b/gcc/ada/libgnat/a-cfhase.ads
index 366735734d9..37022cafffc 100644
--- a/gcc/ada/libgnat/a-cfhase.ads
+++ b/gcc/ada/libgnat/a-cfhase.ads
@@ -801,9 +801,10 @@ is
    --  already in the set.)
 
    procedure Delete (Container : in out Set; Position : in out Cursor) with
-     Global => null,
-     Pre    => Has_Element (Container, Position),
-     Post   =>
+     Global  => null,
+     Depends => (Container =>+ Position, Position => null),
+     Pre     => Has_Element (Container, Position),
+     Post    =>
        Position = No_Element
          and Length (Container) = Length (Container)'Old - 1
 
diff --git a/gcc/ada/libgnat/a-cforma.ads b/gcc/ada/libgnat/a-cforma.ads
index acedbe4e097..99b02a55119 100644
--- a/gcc/ada/libgnat/a-cforma.ads
+++ b/gcc/ada/libgnat/a-cforma.ads
@@ -733,9 +733,10 @@ is
                 Cut   => Find (Keys (Container), Key)'Old);
 
    procedure Delete (Container : in out Map; Position : in out Cursor) with
-     Global => null,
-     Pre    => Has_Element (Container, Position),
-     Post   =>
+     Global  => null,
+     Depends => (Container =>+ Position, Position => null),
+     Pre     => Has_Element (Container, Position),
+     Post    =>
        Position = No_Element
          and Length (Container) = Length (Container)'Old - 1
 
diff --git a/gcc/ada/libgnat/a-cforse.ads b/gcc/ada/libgnat/a-cforse.ads
index 77fc0b401d4..a818726cad7 100644
--- a/gcc/ada/libgnat/a-cforse.ads
+++ b/gcc/ada/libgnat/a-cforse.ads
@@ -858,9 +858,10 @@ is
      (Container : in out Set;
       Position  : in out Cursor)
    with
-     Global => null,
-     Pre    => Has_Element (Container, Position),
-     Post   =>
+     Global  => null,
+     Depends => (Container =>+ Position, Position => null),
+     Pre     => Has_Element (Container, Position),
+     Post    =>
        Position = No_Element
          and Length (Container) = Length (Container)'Old - 1