[Ada] Skip code not in SPARK for ownership analysis

Ownership rules for pointer support should only apply to code marked in
SPARK. There is no impact on compilation.

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

gcc/ada/

	* sem_spark.adb (Check_Package_Spec, Check_Package_Body): Only
	analyze parts of the code marked in SPARK.

From-SVN: r273052

2 files changed, 49 insertions, 28 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 6f300dc..07c3747 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2019-07-04  Yannick Moy  <moy@adacore.com>
+
+	* sem_spark.adb (Check_Package_Spec, Check_Package_Body): Only
+	analyze parts of the code marked in SPARK.
+
 2019-07-04  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* erroutc.adb, exp_aggr.adb, inline.adb, opt.adb, sem_ch3.adb:
diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb
index 82ddb16..1b1ba0f 100644
--- a/gcc/ada/sem_spark.adb
+++ b/gcc/ada/sem_spark.adb
@@ -2364,39 +2364,43 @@ package body Sem_SPARK is
       Save_In_Elab : constant Boolean := Inside_Elaboration;
       Spec         : constant Node_Id :=
         Package_Specification (Corresponding_Spec (Pack));
-      Prag         : constant Node_Id := SPARK_Pragma (Defining_Entity (Pack));
+      Id           : constant Entity_Id := Defining_Entity (Pack);
+      Prag         : constant Node_Id := SPARK_Pragma (Id);
+      Aux_Prag     : constant Node_Id := SPARK_Aux_Pragma (Id);
       Saved_Env    : Perm_Env;
 
    begin
-      --  Only SPARK bodies are analyzed
-
-      if No (Prag)
-        or else Get_SPARK_Mode_From_Annotation (Prag) /= Opt.On
+      if Present (Prag)
+        and then Get_SPARK_Mode_From_Annotation (Prag) = Opt.On
       then
-         return;
-      end if;
+         Inside_Elaboration := True;
 
-      Inside_Elaboration := True;
+         --  Save environment and put a new one in place
 
-      --  Save environment and put a new one in place
+         Move_Env (Current_Perm_Env, Saved_Env);
 
-      Move_Env (Current_Perm_Env, Saved_Env);
+         --  Reanalyze package spec to have its variables in the environment
 
-      --  Reanalyze package spec to have its variables in the environment
+         Check_List (Visible_Declarations (Spec));
+         Check_List (Private_Declarations (Spec));
 
-      Check_List (Visible_Declarations (Spec));
-      Check_List (Private_Declarations (Spec));
+         --  Check declarations and statements in the special mode for
+         --  elaboration.
 
-      --  Check declarations and statements in the special mode for elaboration
+         Check_List (Declarations (Pack));
 
-      Check_List (Declarations (Pack));
-      Check_Node (Handled_Statement_Sequence (Pack));
+         if Present (Aux_Prag)
+           and then Get_SPARK_Mode_From_Annotation (Aux_Prag) = Opt.On
+         then
+            Check_Node (Handled_Statement_Sequence (Pack));
+         end if;
 
-      --  Restore the saved environment and free the current one
+         --  Restore the saved environment and free the current one
 
-      Move_Env (Saved_Env, Current_Perm_Env);
+         Move_Env (Saved_Env, Current_Perm_Env);
 
-      Inside_Elaboration := Save_In_Elab;
+         Inside_Elaboration := Save_In_Elab;
+      end if;
    end Check_Package_Body;
 
    ------------------------
@@ -2406,25 +2410,37 @@ package body Sem_SPARK is
    procedure Check_Package_Spec (Pack : Node_Id) is
       Save_In_Elab : constant Boolean := Inside_Elaboration;
       Spec         : constant Node_Id := Specification (Pack);
+      Id           : constant Entity_Id := Defining_Entity (Pack);
+      Prag         : constant Node_Id := SPARK_Pragma (Id);
+      Aux_Prag     : constant Node_Id := SPARK_Aux_Pragma (Id);
       Saved_Env    : Perm_Env;
 
    begin
-      Inside_Elaboration := True;
+      if Present (Prag)
+        and then Get_SPARK_Mode_From_Annotation (Prag) = Opt.On
+      then
+         Inside_Elaboration := True;
 
-      --  Save environment and put a new one in place
+         --  Save environment and put a new one in place
 
-      Move_Env (Current_Perm_Env, Saved_Env);
+         Move_Env (Current_Perm_Env, Saved_Env);
 
-      --  Check declarations in the special mode for elaboration
+         --  Check declarations in the special mode for elaboration
 
-      Check_List (Visible_Declarations (Spec));
-      Check_List (Private_Declarations (Spec));
+         Check_List (Visible_Declarations (Spec));
 
-      --  Restore the saved environment and free the current one
+         if Present (Aux_Prag)
+           and then Get_SPARK_Mode_From_Annotation (Aux_Prag) = Opt.On
+         then
+            Check_List (Private_Declarations (Spec));
+         end if;
 
-      Move_Env (Saved_Env, Current_Perm_Env);
+         --  Restore the saved environment and free the current one
 
-      Inside_Elaboration := Save_In_Elab;
+         Move_Env (Saved_Env, Current_Perm_Env);
+
+         Inside_Elaboration := Save_In_Elab;
+      end if;
    end Check_Package_Spec;
 
    -------------------------------