[Ada] SPARK support for pointers through ownership

SPARK RM 3.10 is the final version of the pointer ownership rules. Start
changing the implementation accordingly. Anonymous access types are not
fully supported yet.

There is no impact on compilation.

2019-07-01  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_spark.adb: Completely rework the algorithm for ownership
	checking, as the rules in SPARK RM have changed a lot.
	* sem_spark.ads: Update comments.

From-SVN: r272878

gcc/ada/ChangeLog

@@ -1,3 +1,9 @@
+2019-07-01  Yannick Moy  <moy@adacore.com>
+
+	* sem_spark.adb: Completely rework the algorithm for ownership
+	checking, as the rules in SPARK RM have changed a lot.
+	* sem_spark.ads: Update comments.
+
 2019-07-01  Dmitriy Anisimkov  <anisimko@adacore.com>
 
 	* gsocket.h (Has_Sockaddr_Len): Use the offset of sin_family offset in

gcc/ada/sem_spark.ads

@@ -23,9 +23,9 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
---  This package implements an anti-aliasing analysis for access types. The
---  rules that are enforced are defined in the anti-aliasing section of the
---  SPARK RM 6.4.2
+--  This package implements an ownership analysis for access types. The rules
+--  that are enforced are defined in section 3.10 of the SPARK Reference
+--  Manual.
 --
 --  Check_Safe_Pointers is called by Gnat1drv, when GNATprove mode is
 --  activated. It does an analysis of the source code, looking for code that is
@@ -138,6 +138,6 @@ package Sem_SPARK is
 
    procedure Check_Safe_Pointers (N : Node_Id);
    --  The entry point of this package. It analyzes a node and reports errors
-   --  when there are violations of aliasing rules.
+   --  when there are violations of ownership rules.
 
 end Sem_SPARK;