From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 2100) id 782B9393C813; Sat, 22 Aug 2020 22:09:29 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 782B9393C813 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1598134169; bh=MAsr6HFx3hZFipRlWFhEOCgbS89h3UUq+F7ilENuga8=; h=From:To:Subject:Date:From; b=JUrrlbblTGTBUnxZsOqnokD02DkSkQtYe1z21K1E3szBs1i/TFh9A1SxfpcuLdGtb Du6ZBSTrl4rk45UXSmCQj6A0+aRL6oprJxfLsSXt4xDs0AZPFCkxap4VvDx4KkoOnm 5mipi9sn1VTdtVxi0+vYTBfzNf0HMsWMhKnv7kyM= Content-Type: text/plain; charset="us-ascii" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit From: Giuliano Belinassi To: gcc-cvs@gcc.gnu.org Subject: [gcc/devel/autopar_devel] [Ada] Add Depends contracts to Delete procedures of formal containers X-Act-Checkin: gcc X-Git-Author: Claire Dross X-Git-Refname: refs/heads/devel/autopar_devel X-Git-Oldrev: 34229115f5a8b36a844a77f446dc75e186e3e627 X-Git-Newrev: c22b643f50a3592454b30352adf1fa9bdf67ecad Message-Id: <20200822220929.782B9393C813@sourceware.org> Date: Sat, 22 Aug 2020 22:09:29 +0000 (GMT) X-BeenThere: gcc-cvs@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-cvs mailing list List-Unsubscribe: , List-Archive: List-Help: List-Subscribe: , X-List-Received-Date: Sat, 22 Aug 2020 22:09:29 -0000 https://gcc.gnu.org/g:c22b643f50a3592454b30352adf1fa9bdf67ecad commit c22b643f50a3592454b30352adf1fa9bdf67ecad Author: Claire Dross Date: Mon Feb 10 12:30:40 2020 +0100 [Ada] Add Depends contracts to Delete procedures of formal containers 2020-06-08 Claire Dross 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