[Ada] Fix crashes on ownership checking in SPARK

Code that violates the conditions for ownership checking should lead to
error messages pointing to the violations instead of crashes.

There is no impact on compilation, only GNATprove.

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

gcc/ada/

	* sem_spark.adb (Get_Root_Object): Replace precondition by error
	message.
	(Read_Indexes): Replace precondition by error message.
	(Check_Callable_Body): Check only traversal function returns an
	anonymous access type.
	(Check_Expression): Issue error on unexpected expression as
	path.
	* sem_util.adb (First_Global): Fix access to global on
	entry/task.

From-SVN: r273329

gcc/ada/ChangeLog

+2019-07-10  Yannick Moy  <moy@adacore.com>
+
+	* sem_spark.adb (Get_Root_Object): Replace precondition by error
+	message.
+	(Read_Indexes): Replace precondition by error message.
+	(Check_Callable_Body): Check only traversal function returns an
+	anonymous access type.
+	(Check_Expression): Issue error on unexpected expression as
+	path.
+	* sem_util.adb (First_Global): Fix access to global on
+	entry/task.
+
 2019-07-10  Javier Miranda  <miranda@adacore.com>
 
 	* exp_ch6.adb (Is_Class_Wide_Interface_Type): New subprogram.

gcc/ada/sem_spark.adb

@@ -714,7 +714,6 @@ package body Sem_SPARK is
    function Get_Root_Object
      (Expr              : Node_Id;
       Through_Traversal : Boolean := True) return Entity_Id;
-   pragma Precondition (Is_Path_Expression (Expr));
    --  Return the root of the path expression Expr, or Empty for an allocator,
    --  NULL, or a function call. Through_Traversal is True if it should follow
    --  through calls to traversal functions.
@@ -1311,6 +1310,15 @@ package body Sem_SPARK is
 
       Inside_Elaboration := False;
 
+      if Ekind (Spec_Id) = E_Function
+        and then Is_Anonymous_Access_Type (Etype (Spec_Id))
+        and then not Is_Traversal_Function (Spec_Id)
+      then
+         Error_Msg_N ("anonymous access type for result only allowed for "
+                      & "traveral functions", Spec_Id);
+         return;
+      end if;
+
       --  Save environment and put a new one in place
 
       Move_Env (Current_Perm_Env, Saved_Env);
@@ -1451,7 +1459,6 @@ package body Sem_SPARK is
       --  Call Read_Expression on every expression in the list L
 
       procedure Read_Indexes (Expr : Node_Id);
-      pragma Precondition (Is_Path_Expression (Expr));
       --  When processing a path, the index expressions and function call
       --  arguments occurring on the path should be analyzed in Read mode.
 
@@ -1562,6 +1569,11 @@ package body Sem_SPARK is
       --  Start of processing for Read_Indexes
 
       begin
+         if not Is_Path_Expression (Expr) then
+            Error_Msg_N ("name expected here for move/borrow/observe", Expr);
+            return;
+         end if;
+
          case N_Subexpr'(Nkind (Expr)) is
             when N_Identifier
                | N_Expanded_Name
@@ -1710,7 +1722,10 @@ package body Sem_SPARK is
       --  Expressions that are not path expressions should only be analyzed in
       --  Read mode.
 
-      pragma Assert (Mode = Read);
+      if Mode /= Read then
+         Error_Msg_N ("name expected here for move/borrow/observe", Expr);
+         return;
+      end if;
 
       --  Special handling for nodes that may contain evaluated expressions in
       --  the form of constraints.
@@ -3484,6 +3499,11 @@ package body Sem_SPARK is
       Through_Traversal : Boolean := True) return Entity_Id
    is
    begin
+      if not Is_Path_Expression (Expr) then
+         Error_Msg_N ("name expected here for path", Expr);
+         return Empty;
+      end if;
+
       case Nkind (Expr) is
          when N_Expanded_Name
             | N_Identifier

gcc/ada/sem_util.adb

@@ -8713,7 +8713,24 @@ package body Sem_Util is
       --  case, it can only be located on the body entity.
 
       if Refined then
-         Body_Id := Subprogram_Body_Entity (Subp);
+         if Is_Subprogram_Or_Generic_Subprogram (Subp) then
+            Body_Id := Subprogram_Body_Entity (Subp);
+
+         elsif Is_Entry (Subp)
+           or else Is_Task_Type (Subp)
+         then
+            Body_Id := Corresponding_Body (Parent (Subp));
+
+         --  ??? It should be possible to retrieve the Refined_Global on the
+         --  task body associated to the task object. This is not yet possible.
+
+         elsif Is_Single_Task_Object (Subp) then
+            Body_Id := Empty;
+
+         else
+            Body_Id := Empty;
+         end if;
+
          if Present (Body_Id) then
             Global := Get_Pragma (Body_Id, Pragma_Refined_Global);
          end if;