[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 0f7cd2d4838938d66eab5c7db8eac357206c9ce9..748f1bfd681938e5db6a2de40ce859c379eda0b6 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,11 @@
+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

diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb
index 0de51f866fa52b9a62a12866d43b592ed1f08ed4..a60a6cb4bacc51c5db3b48626fc531dc05cd52c2 100644 (file)
--- 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 0e8b29b41f7bf2176a9d98549fa00fe0f7d2607b..195e833277ba53059aab9fe39a75c8bae6e2d385 100644 (file)
--- 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;