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.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-08-19 Joffrey Huguet <hug...@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.
--- gcc/ada/libgnat/a-cfdlli.ads
+++ 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
--- gcc/ada/libgnat/a-cfhama.ads
+++ 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
--- gcc/ada/libgnat/a-cfinve.ads
+++ 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
--- gcc/ada/libgnat/a-cforma.ads
+++ 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
--- gcc/ada/libgnat/a-cofove.ads
+++ 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
--- gcc/ada/libgnat/a-cofuma.ads
+++ 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
--- gcc/ada/libgnat/a-cofuve.ads
+++ 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