[Ada] Add Depends contracts to Delete procedures of formal containers

Message ID 20200608080041.GA90235@adacore.com
State New
Headers show
Series
  • [Ada] Add Depends contracts to Delete procedures of formal containers
Related show

Commit Message

Pierre-Marie de Rodat June 8, 2020, 8 a.m.
Add a Depends contract to Delete procedures of formal containers to
state that the output value of the Position cursor depends on no inputs
(it is No_Element). This now ensures that no warnings will be emitted
by GNATprove if this value is not used after a call to Delete.

Tested on x86_64-pc-linux-gnu, committed on trunk

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.

Patch

--- gcc/ada/libgnat/a-cfdlli.ads
+++ 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

--- gcc/ada/libgnat/a-cfhama.ads
+++ 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
 

--- gcc/ada/libgnat/a-cfhase.ads
+++ 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
 

--- gcc/ada/libgnat/a-cforma.ads
+++ 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
 

--- gcc/ada/libgnat/a-cforse.ads
+++ 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