[Ada] Adapt body of formal sets and maps for SPARK

Remove violations of SPARK rules, to prepare for the proof of hashed
sets and maps:

- Make the type of hash tables not tagged, so that it will be possible
  to mark the type of nodes as having relaxed initialization.

- Remove comparison of addresses as check or optimization: as a check,
  it is not necessary in SPARK as the caller cannot pass in aliased
  parameters in such cases; as an optimization, it is not possible in
  SPARK code.

- Avoid aliasing when inserting a node in the hash table. The code for
  insertion in sets and maps was explicitly aliasing a global for the
  container and a parameter for its hash table component, both being
  written. Rewrite the code to pass only the hash table as parameter.

- Insert constants for subtype constraints, which cannot depend on
  variables in SPARK code.

- Use procedures instead of functions when side-effects are expected.

- Rename variables whose value is only written through calls and not
  read, using Unused prefix, so that flow analysis does not warn about
  it.

gcc/ada/

	* libgnat/a-cfhama.adb (Generic_Allocate): Retype to avoid
	aliasing.
	(Assign, Move): Remove address comparison.
	(Include): Insert constants for subtype constraints.
	(Insert): Rewrite to avoid aliasing and function with side-effects.
	* libgnat/a-cfhase.adb (Generic_Allocate): Retype to avoid
	aliasing.
	(Assign, Move): Remove address comparison.
	(Difference, Intersection, Is_Subset, Overlap,
	Symmetric_Difference, Union): Remove address comparison.  Insert
	constants for subtype constraints.
	(Insert): Rewrite to avoid aliasing and function with
	side-effects.
	* libgnat/a-chtgfk.adb (Checked_Equivalent_Keys, Checked_Index,
	Delete_Key_Sans_Free, Find, Generic_Replace_Element, Index):
	Type for hash tables not tagged anymore.
	(Generic_Conditional_Insert): New_Node generic formal is a
	procedure taking the hash table as first parameter now, to avoid
	aliasing in the caller.
	* libgnat/a-chtgfk.ads: Same.
	* libgnat/a-chtgfo.adb (Checked_Index, Clear,
	Delete_Node_At_Index, Delete_Node_Sans_Free, First, Free,
	Generic_Allocate, Generic_Iteration, Generic_Read,
	Generic_Write, Index, Next): Type for hash tables not tagged
	anymore.
	(Generic_Equal): Removed tagged. Remove address comparison.
	* libgnat/a-chtgfo.ads: Same.
	* libgnat/a-cohata.ads (Hash_Table_Type): Remove tagged.

0 files changed, 0 insertions, 0 deletions