[Ada] Issue error on SPARK ownership rule violation

A modified rule in SPARK RM specifies that object declarations of
anonymous access type should only occur immediately in subprogram, entry
or block. Now checked.

There is no impact on compilation.

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

gcc/ada/

	* sem_spark.ads (Is_Local_Context): New function.
	* sem_spark.adb (Check_Declaration): Issue errors on violations
	of SPARK RM 3.10(4)
	(Process_Path): Do not issue error on borrow/observe during
	elaboration, as these are caught by the new rule.

From-SVN: r273721

3 files changed, 62 insertions, 13 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 0f7cd2d..748f1bf 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,13 @@
 2019-07-23  Yannick Moy  <moy@adacore.com>
 
+	* sem_spark.ads (Is_Local_Context): New function.
+	* sem_spark.adb (Check_Declaration): Issue errors on violations
+	of SPARK RM 3.10(4)
+	(Process_Path): Do not issue error on borrow/observe during
+	elaboration, as these are caught by the new rule.
+
+2019-07-23  Yannick Moy  <moy@adacore.com>
+
 	* exp_ch7.adb (Create_Finalizer): Force finalizer not to be
 	Ghost enabled.
 	* exp_dbug.adb (Get_External_Name): Explain special case of
diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb
index 0de51f8..a60a6cb 100644
--- a/gcc/ada/sem_spark.adb
+++ b/gcc/ada/sem_spark.adb
@@ -1419,9 +1419,37 @@ package body Sem_SPARK is
             Check_Expression (Subtype_Indication (Decl), Read);
 
          when N_Object_Declaration =>
+            Expr := Expression (Decl);
+
             Check_Type (Target_Typ);
 
-            Expr := Expression (Decl);
+            --  A declaration of a stand-alone object of an anonymous access
+            --  type shall have an explicit initial value and shall occur
+            --  immediately within a subprogram body, an entry body, or a
+            --  block statement (SPARK RM 3.10(4)).
+
+            if Is_Anonymous_Access_Type (Target_Typ) then
+               declare
+                  Scop : constant Entity_Id := Scope (Target);
+               begin
+                  if not Is_Local_Context (Scop) then
+                     if Emit_Messages then
+                        Error_Msg_N
+                          ("object of anonymous access type must be declared "
+                           & "immediately within a subprogram, entry or block "
+                           & "(SPARK RM 3.10(4))", Decl);
+                     end if;
+                  end if;
+               end;
+
+               if No (Expr) then
+                  if Emit_Messages then
+                     Error_Msg_N ("object of anonymous access type must be "
+                                  & "initialized (SPARK RM 3.10(4))", Decl);
+                  end if;
+               end if;
+            end if;
+
             if Present (Expr) then
                Check_Assignment (Target => Target,
                                  Expr   => Expr);
@@ -2848,9 +2876,14 @@ package body Sem_SPARK is
          --  independently for R permission. Outputs are checked
          --  independently to have RW permission on exit.
 
-         when Pragma_Contract_Cases
+         --  Postconditions are checked for correct use of 'Old, but starting
+         --  from the corresponding declaration, in order to avoid dealing with
+         --  with contracts on generic subprograms, which are not handled in
+         --  GNATprove.
+
+         when Pragma_Precondition
             | Pragma_Postcondition
-            | Pragma_Precondition
+            | Pragma_Contract_Cases
             | Pragma_Refined_Post
          =>
             null;
@@ -3993,6 +4026,16 @@ package body Sem_SPARK is
       end case;
    end Is_Deep;
 
+   ----------------------
+   -- Is_Local_Context --
+   ----------------------
+
+   function Is_Local_Context (Scop : Entity_Id) return Boolean is
+   begin
+      return Is_Subprogram_Or_Entry (Scop)
+        or else Ekind (Scop) = E_Block;
+   end Is_Local_Context;
+
    ------------------------
    -- Is_Path_Expression --
    ------------------------
@@ -4863,13 +4906,10 @@ package body Sem_SPARK is
 
          when Borrow =>
 
-            --  Forbidden during elaboration
+            --  Forbidden during elaboration, an error is already issued in
+            --  Check_Declaration, just return.
 
             if Inside_Elaboration then
-               if not Inside_Procedure_Call and then Emit_Messages then
-                  Error_Msg_N ("illegal borrow during elaboration", Expr);
-               end if;
-
                return;
             end if;
 
@@ -4882,13 +4922,10 @@ package body Sem_SPARK is
 
          when Observe =>
 
-            --  Forbidden during elaboration
+            --  Forbidden during elaboration, an error is already issued in
+            --  Check_Declaration, just return.
 
             if Inside_Elaboration then
-               if not Inside_Procedure_Call and then Emit_Messages then
-                  Error_Msg_N ("illegal observe during elaboration", Expr);
-               end if;
-
                return;
             end if;
 
diff --git a/gcc/ada/sem_spark.ads b/gcc/ada/sem_spark.ads
index 0e8b29b..195e833 100644
--- a/gcc/ada/sem_spark.ads
+++ b/gcc/ada/sem_spark.ads
@@ -162,4 +162,8 @@ package Sem_SPARK is
 
    function Is_Traversal_Function (E : Entity_Id) return Boolean;
 
+   function Is_Local_Context (Scop : Entity_Id) return Boolean;
+   --  Return if a given scope defines a local context where it is legal to
+   --  declare a variable of anonymous access type.
+
 end Sem_SPARK;