[Ada] Skip code not in SPARK for ownership analysis

[Ada] Skip code not in SPARK for ownership analysis

[Pierre-Marie de Rodat]

[-- Attachment #1: Type: text/plain, Size: 327 bytes --]

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

Tested on x86_64-pc-linux-gnu, committed on trunk

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.

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 4168 bytes --]

--- gcc/ada/sem_spark.adb
+++ 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;
 
    -------------------------------