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.
Tested on x86_64-pc-linux-gnu, committed on trunk
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.
patch.diff.gz
Description: application/gzip
