[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.

From-SVN: r274643

8 files changed, 16 insertions, 0 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 3163ad1..8ba0dc4 100644
--- 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 f6bf8c9..b8df023 100644
--- 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 643a949..c4e8221 100644
--- 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 e359f8d..87940d2 100644
--- 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 d76cc76..a13bce4 100644
--- 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 5b62664..b23c661 100644
--- 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 8a71cb7..bf6e5a8 100644
--- 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 4f80450..804d7b0 100644
--- 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