[Ada] Fix ownership checking for pointers in SPARK

Checking of the readable status of sub-expressions occurring in the
target path of an assignment should occur before the right-hand-side is
moved or borrowed or observed.

There is no impact on compilation.

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

gcc/ada/

	* sem_spark.adb (Check_Expression): Change signature to take an
	Extended_Checking_Mode, for handling read permission checking of
	sub-expressions in an assignment.
	(Check_Parameter_Or_Global): Adapt to new behavior of
	Check_Expression for mode Assign.
	(Check_Safe_Pointers): Do not analyze generic bodies.
	(Check_Assignment): Separate checking of the target of an
	assignment.

From-SVN: r273266

gcc/ada/ChangeLog

+2019-07-09  Yannick Moy  <moy@adacore.com>
+
+	* sem_spark.adb (Check_Expression): Change signature to take an
+	Extended_Checking_Mode, for handling read permission checking of
+	sub-expressions in an assignment.
+	(Check_Parameter_Or_Global): Adapt to new behavior of
+	Check_Expression for mode Assign.
+	(Check_Safe_Pointers): Do not analyze generic bodies.
+	(Check_Assignment): Separate checking of the target of an
+	assignment.
+
 2019-07-09  Eric Botcazou  <ebotcazou@adacore.com>
 
 	* repinfo.ads (JSON format): Adjust.

gcc/ada/sem_spark.adb

@@ -560,9 +560,13 @@ package body Sem_SPARK is
    --  has the right permission, and also updating permissions when a path is
    --  moved, borrowed, or observed.
 
-   type Checking_Mode is
+   type Extended_Checking_Mode is
 
-     (Read,
+     (Read_Subexpr,
+      --  Special value used for assignment, to check that subexpressions of
+      --  the assigned path are readable.
+
+      Read,
       --  Default mode
 
       Move,
@@ -591,6 +595,8 @@ package body Sem_SPARK is
       --  and extensions are set to Read_Only.
      );
 
+   subtype Checking_Mode is Extended_Checking_Mode range Read .. Observe;
+
    type Result_Kind is (Folded, Unfolded);
    --  The type declaration to discriminate in the Perm_Or_Tree type
 
@@ -631,7 +637,7 @@ package body Sem_SPARK is
 
    procedure Check_Declaration (Decl : Node_Id);
 
-   procedure Check_Expression (Expr : Node_Id; Mode : Checking_Mode);
+   procedure Check_Expression (Expr : Node_Id; Mode : Extended_Checking_Mode);
    pragma Precondition (Nkind_In (Expr, N_Index_Or_Discriminant_Constraint,
                                         N_Range_Constraint,
                                         N_Subtype_Indication)
@@ -1421,8 +1427,10 @@ package body Sem_SPARK is
    -- Check_Expression --
    ----------------------
 
-   procedure Check_Expression (Expr : Node_Id; Mode : Checking_Mode) is
-
+   procedure Check_Expression
+     (Expr : Node_Id;
+      Mode : Extended_Checking_Mode)
+   is
       --  Local subprograms
 
       function Is_Type_Name (Expr : Node_Id) return Boolean;
@@ -1543,8 +1551,14 @@ package body Sem_SPARK is
          return;
 
       elsif Is_Path_Expression (Expr) then
-         Read_Indexes (Expr);
-         Process_Path (Expr, Mode);
+         if Mode /= Assign then
+            Read_Indexes (Expr);
+         end if;
+
+         if Mode /= Read_Subexpr then
+            Process_Path (Expr, Mode);
+         end if;
+
          return;
       end if;
 
@@ -2511,6 +2525,10 @@ package body Sem_SPARK is
             Mode := Move;
       end case;
 
+      if Mode = Assign then
+         Check_Expression (Expr, Read_Subexpr);
+      end if;
+
       Check_Expression (Expr, Mode);
    end Check_Parameter_Or_Global;
 
@@ -2618,11 +2636,6 @@ package body Sem_SPARK is
          Reset (Current_Perm_Env);
       end Initialize;
 
-      --  Local variables
-
-      Prag : Node_Id;
-      --  SPARK_Mode pragma in application
-
    --  Start of processing for Check_Safe_Pointers
 
    begin
@@ -2636,20 +2649,28 @@ package body Sem_SPARK is
             | N_Package_Declaration
             | N_Subprogram_Body
          =>
-            Prag := SPARK_Pragma (Defining_Entity (N));
+            declare
+               E    : constant Entity_Id := Defining_Entity (N);
+               Prag : constant Node_Id := SPARK_Pragma (E);
+               --  SPARK_Mode pragma in application
 
-            if Present (Prag) then
-               if Get_SPARK_Mode_From_Annotation (Prag) = Opt.On then
-                  Check_Node (N);
-               end if;
+            begin
+               if Ekind (Unique_Entity (E)) in Generic_Unit_Kind then
+                  null;
 
-            elsif Nkind (N) = N_Package_Body then
-               Check_List (Declarations (N));
+               elsif Present (Prag) then
+                  if Get_SPARK_Mode_From_Annotation (Prag) = Opt.On then
+                     Check_Node (N);
+                  end if;
 
-            elsif Nkind (N) = N_Package_Declaration then
-               Check_List (Private_Declarations (Specification (N)));
-               Check_List (Visible_Declarations (Specification (N)));
-            end if;
+               elsif Nkind (N) = N_Package_Body then
+                  Check_List (Declarations (N));
+
+               elsif Nkind (N) = N_Package_Declaration then
+                  Check_List (Private_Declarations (Specification (N)));
+                  Check_List (Visible_Declarations (Specification (N)));
+               end if;
+            end;
 
          when others =>
             null;
@@ -2717,7 +2738,14 @@ package body Sem_SPARK is
          when N_Assignment_Statement =>
             declare
                Target : constant Node_Id := Name (Stmt);
+
             begin
+               --  Start with checking that the subexpressions of the target
+               --  path are readable, before possibly updating the permission
+               --  of these subexpressions in Check_Assignment.
+
+               Check_Expression (Target, Read_Subexpr);
+
                Check_Assignment (Target => Target,
                                  Expr   => Expression (Stmt));