public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc/devel/autopar_devel] [Ada] Add Depends contracts to Delete procedures of formal containers
@ 2020-08-22 22:09 Giuliano Belinassi
0 siblings, 0 replies; only message in thread
From: Giuliano Belinassi @ 2020-08-22 22:09 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:c22b643f50a3592454b30352adf1fa9bdf67ecad
commit c22b643f50a3592454b30352adf1fa9bdf67ecad
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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2020-08-22 22:09 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-08-22 22:09 [gcc/devel/autopar_devel] [Ada] Add Depends contracts to Delete procedures of formal containers Giuliano Belinassi
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).