diff options
| author | Claire Dross <dross@adacore.com> | 2020-02-10 12:30:40 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-06-08 03:50:52 -0400 |
| commit | 54c1fdb62b647c1dedf6d58d260ed85e93e0af20 (patch) | |
| tree | e360663b89cc6b6eb362222bbd91e55aac662d46 /gcc | |
| parent | 9490fd58a82b80a7048d5e1a82f749da438b4306 (diff) | |
| download | gcc-54c1fdb62b647c1dedf6d58d260ed85e93e0af20.zip gcc-54c1fdb62b647c1dedf6d58d260ed85e93e0af20.tar.gz gcc-54c1fdb62b647c1dedf6d58d260ed85e93e0af20.tar.bz2 | |
[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.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/libgnat/a-cfdlli.ads | 7 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-cfhama.ads | 7 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-cfhase.ads | 7 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-cforma.ads | 7 | ||||
| -rw-r--r-- | 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 426a584..6131239 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 7b50096..8a73508 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 3667357..37022ca 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 acedbe4..99b02a5 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 77fc0b4..a818726 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 |