[Ada] Add formal function parameter equality to SPARK containers
diff mbox series

Message ID 20190819083859.GA33377@adacore.com
State New
Headers show
Series
  • [Ada] Add formal function parameter equality to SPARK containers
Related show

Commit Message

Pierre-Marie de Rodat Aug. 19, 2019, 8:38 a.m. UTC
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  <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.

Patch
diff mbox series

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