From: Joffrey Huguet Date: Mon, 19 Aug 2019 08:35:49 +0000 (+0000) Subject: [Ada] Add formal function parameter equality to SPARK containers X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=123f02156122ea13f3bfabdef2b6385a25527158;p=gcc.git [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 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 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 3163ad1c142..8ba0dc4a1d2 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,11 @@ +2019-08-19 Joffrey Huguet + + * 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 * 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 f6bf8c9f054..b8df0231255 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 643a94998e2..c4e822107ed 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 e359f8d5781..87940d27bda 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 d76cc76c132..a13bce4b669 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 5b62664097c..b23c6613bf0 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 8a71cb7af10..bf6e5a81710 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 4f804509ea6..804d7b0b7ed 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