[Ada] Add formal function parameter equality to SPARK containers

This patch adds a formal function parameter "=" (L, R : Element_Type) to
SPARK containers. The equality that is used by default for Element_Type
after this patch is the primitive equality and not the predefined any
more. It also allows to use any function with the appropriate signature
for the equality function.

2019-08-19  Joffrey Huguet  <huguet@adacore.com>

gcc/ada/

	* libgnat/a-cfdlli.ads, libgnat/a-cfhama.ads,
	libgnat/a-cfinve.ads, libgnat/a-cforma.ads,
	libgnat/a-cofove.ads, libgnat/a-cofuma.ads,
	libgnat/a-cofuve.ads: Add formal function parameter "=" (L, R :
	Element_Type) to the generic packages.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@274643 138bc75d-0d04-0410-961f-82ee72b054a4

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 3163ad1c14218f140e020ba79d060286055908b8..8ba0dc4a1d21ac351fe2603fb7bc6060ff75ad3f 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,11 @@
+2019-08-19  Joffrey Huguet  <huguet@adacore.com>
+
+       * libgnat/a-cfdlli.ads, libgnat/a-cfhama.ads,
+       libgnat/a-cfinve.ads, libgnat/a-cforma.ads,
+       libgnat/a-cofove.ads, libgnat/a-cofuma.ads,
+       libgnat/a-cofuve.ads: Add formal function parameter "=" (L, R :
+       Element_Type) to the generic packages.
+
 2019-08-19  Eric Botcazou  <ebotcazou@adacore.com>
 
        * opt.ads: Clean up left-overs of earlier implementation in

diff --git a/gcc/ada/libgnat/a-cfdlli.ads b/gcc/ada/libgnat/a-cfdlli.ads
index f6bf8c9f054061e3b56c81743f68e7d68e223b30..b8df023125596732eb6e3c269210b7a91b1dbfcc 100644 (file)
--- a/gcc/ada/libgnat/a-cfdlli.ads
+++ b/gcc/ada/libgnat/a-cfdlli.ads
@@ -34,6 +34,7 @@ with Ada.Containers.Functional_Maps;
 
 generic
    type Element_Type is private;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
 package Ada.Containers.Formal_Doubly_Linked_Lists with
   SPARK_Mode

diff --git a/gcc/ada/libgnat/a-cfhama.ads b/gcc/ada/libgnat/a-cfhama.ads
index 643a94998e271470978956e7ba54a9de11c67f4d..c4e822107ed46e6a96fd1205f994c6e1b9f189be 100644 (file)
--- a/gcc/ada/libgnat/a-cfhama.ads
+++ b/gcc/ada/libgnat/a-cfhama.ads
@@ -59,6 +59,7 @@ generic
    with function Equivalent_Keys
      (Left  : Key_Type;
       Right : Key_Type) return Boolean is "=";
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
 package Ada.Containers.Formal_Hashed_Maps with
   SPARK_Mode

diff --git a/gcc/ada/libgnat/a-cfinve.ads b/gcc/ada/libgnat/a-cfinve.ads
index e359f8d578171d9dd339a73da34512a89fa2f5c3..87940d27bdaad387d0e31fee4b34117a7d7dbd6e 100644 (file)
--- a/gcc/ada/libgnat/a-cfinve.ads
+++ b/gcc/ada/libgnat/a-cfinve.ads
@@ -38,6 +38,7 @@ with Ada.Containers.Functional_Vectors;
 generic
    type Index_Type is range <>;
    type Element_Type (<>) is private;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
    Max_Size_In_Storage_Elements : Natural;
    --  Maximum size of Vector elements in bytes. This has the same meaning as
    --  in Ada.Containers.Bounded_Holders, with the same restrictions. Note that

diff --git a/gcc/ada/libgnat/a-cforma.ads b/gcc/ada/libgnat/a-cforma.ads
index d76cc76c132a61efb780d298072ac2f030bfdbd8..a13bce4b669821d3a8c9554bc099adcea811a6f6 100644 (file)
--- a/gcc/ada/libgnat/a-cforma.ads
+++ b/gcc/ada/libgnat/a-cforma.ads
@@ -58,6 +58,7 @@ generic
    type Element_Type is private;
 
    with function "<" (Left, Right : Key_Type) return Boolean is <>;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
 package Ada.Containers.Formal_Ordered_Maps with
   SPARK_Mode

diff --git a/gcc/ada/libgnat/a-cofove.ads b/gcc/ada/libgnat/a-cofove.ads
index 5b62664097c8556662ef7ee5566f649549c7bb2f..b23c6613bf0321dc72048e97c58391663f607191 100644 (file)
--- a/gcc/ada/libgnat/a-cofove.ads
+++ b/gcc/ada/libgnat/a-cofove.ads
@@ -40,6 +40,8 @@ with Ada.Containers.Functional_Vectors;
 generic
    type Index_Type is range <>;
    type Element_Type is private;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
+
 package Ada.Containers.Formal_Vectors with
   SPARK_Mode
 is

diff --git a/gcc/ada/libgnat/a-cofuma.ads b/gcc/ada/libgnat/a-cofuma.ads
index 8a71cb7af10f0782a6e2cd31103adec0b6f6529b..bf6e5a8171060bf217ccfad7641b106bb6fcc256 100644 (file)
--- a/gcc/ada/libgnat/a-cofuma.ads
+++ b/gcc/ada/libgnat/a-cofuma.ads
@@ -39,6 +39,7 @@ generic
    with function Equivalent_Keys
      (Left  : Key_Type;
       Right : Key_Type) return Boolean is "=";
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
    Enable_Handling_Of_Equivalence : Boolean := True;
    --  This constant should only be set to False when no particular handling

diff --git a/gcc/ada/libgnat/a-cofuve.ads b/gcc/ada/libgnat/a-cofuve.ads
index 4f804509ea6a7a5c6e6b233188eb4ee8447a36fc..804d7b0b7edebe91b17908ebcfee48ef5460d76b 100644 (file)
--- a/gcc/ada/libgnat/a-cofuve.ads
+++ b/gcc/ada/libgnat/a-cofuve.ads
@@ -38,6 +38,7 @@ generic
    --  should have at least one more element at the low end than Index_Type.
 
    type Element_Type (<>) is private;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
 package Ada.Containers.Functional_Vectors with SPARK_Mode is