[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.
This commit is contained in:
parent
9490fd58a8
commit
54c1fdb62b
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
Loading…
Reference in New Issue