OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[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
This commit is contained in:
Joffrey Huguet 2019-08-19 08:35:49 +00:00 committed by Pierre-Marie de Rodat
parent b1d7f6fe2b
commit 123f021561
8 changed files with 16 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
gcc/ada/ChangeLog
View File

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

1
gcc/ada/libgnat/a-cfdlli.ads
View File

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

1
gcc/ada/libgnat/a-cfhama.ads
View File

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

1
gcc/ada/libgnat/a-cfinve.ads
View File

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

1
gcc/ada/libgnat/a-cforma.ads
View File

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

2
gcc/ada/libgnat/a-cofove.ads
View File

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

1
gcc/ada/libgnat/a-cofuma.ads
View File

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

1
gcc/ada/libgnat/a-cofuve.ads
View File

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