[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 389a12d8687d0dac9796f10ea0dc58d1a3bb9b18..a5ba51343ef38d9012b564bd3ac73f6b4ab87855 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,15 @@
+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.

diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb
index 70953b5b6da9ba21519f912986917089c67b9d63..af7dcd5f256b495ee9952ed9e6bbebc1da7d234b 100644 (file)
--- a/gcc/ada/sem_spark.adb
+++ b/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

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 19e0026d6f71b1c71044376aae6efced6871c00e..1c266341dfd3457469f408a91f778546bf763f0a 100644 (file)
--- a/gcc/ada/sem_util.adb
+++ b/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;