[Ada] Spurious error on Ghost null procedure

This patch modifies the analysis (which is really expansion) of null
procedures to set the Ghost mode of the spec when the null procedure
acts as a completion.  This ensures that all nodes and entities
generated by the expansion are marked as Ghost, and provide a proper
context for references to Ghost entities.

2018-11-14  Hristian Kirtchev  <kirtchev@adacore.com>

gcc/ada/

	* sem_ch6.adb (Analyze_Null_Procedure): Capture Ghost and
	SPARK-related global state at the start of the routine. Set the
	Ghost mode of the completed spec if any.  Restore the saved
	Ghost and SPARK-related global state on exit from the routine.

gcc/testsuite/

	* gnat.dg/ghost1.adb, gnat.dg/ghost1.ads: New testcase.

From-SVN: r266132

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 1de2a84915c8d26c69f1e3adbee1e8f83d99a7a5..ba6055d08270538fa4455db3f672edd47fb04bab 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,10 @@
+2018-11-14  Hristian Kirtchev  <kirtchev@adacore.com>
+
+       * sem_ch6.adb (Analyze_Null_Procedure): Capture Ghost and
+       SPARK-related global state at the start of the routine. Set the
+       Ghost mode of the completed spec if any.  Restore the saved
+       Ghost and SPARK-related global state on exit from the routine.
+
 2018-11-14  Eric Botcazou  <ebotcazou@adacore.com>
 
        * doc/gnat_ugn/building_executable_programs_with_gnat.rst

diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index f7b688045eae1416d6b137b3a90044ee48814142..e7b90b7782a8cb839f1521a48f241dfaade1f8a1 100644 (file)
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -1396,12 +1396,23 @@ package body Sem_Ch6 is
    -- Analyze_Null_Procedure --
    ----------------------------
 
+   --  WARNING: This routine manages Ghost regions. Return statements must be
+   --  replaced by gotos that jump to the end of the routine and restore the
+   --  Ghost mode.
+
    procedure Analyze_Null_Procedure
      (N             : Node_Id;
       Is_Completion : out Boolean)
    is
-      Loc        : constant Source_Ptr := Sloc (N);
-      Spec       : constant Node_Id    := Specification (N);
+      Loc  : constant Source_Ptr := Sloc (N);
+      Spec : constant Node_Id    := Specification (N);
+
+      Saved_GM   : constant Ghost_Mode_Type := Ghost_Mode;
+      Saved_IGR  : constant Node_Id         := Ignored_Ghost_Region;
+      Saved_ISMP : constant Boolean         :=
+                     Ignore_SPARK_Mode_Pragmas_In_Instance;
+      --  Save the Ghost and SPARK mode-related data to restore on exit
+
       Designator : Entity_Id;
       Form       : Node_Id;
       Null_Body  : Node_Id := Empty;
@@ -1409,6 +1420,17 @@ package body Sem_Ch6 is
       Prev       : Entity_Id;
 
    begin
+      Prev := Current_Entity_In_Scope (Defining_Entity (Spec));
+
+      --  A null procedure is Ghost when it is stand-alone and is subject to
+      --  pragma Ghost, or when the corresponding spec is Ghost. Set the mode
+      --  now, to ensure that any nodes generated during analysis and expansion
+      --  are properly marked as Ghost.
+
+      if Present (Prev) then
+         Mark_And_Set_Ghost_Body (N, Prev);
+      end if;
+
       --  Capture the profile of the null procedure before analysis, for
       --  expansion at the freeze point and at each point of call. The body is
       --  used if the procedure has preconditions, or if it is a completion. In
@@ -1453,8 +1475,6 @@ package body Sem_Ch6 is
       --  and set minimal semantic information on the original declaration,
       --  which is rewritten as a null statement.
 
-      Prev := Current_Entity_In_Scope (Defining_Entity (Spec));
-
       if Present (Prev) and then Is_Generic_Subprogram (Prev) then
          Insert_Before (N, Null_Body);
          Set_Ekind (Defining_Entity (N), Ekind (Prev));
@@ -1462,7 +1482,8 @@ package body Sem_Ch6 is
          Rewrite (N, Make_Null_Statement (Loc));
          Analyze_Generic_Subprogram_Body (Null_Body, Prev);
          Is_Completion := True;
-         return;
+
+         goto Leave;
 
       else
          --  Resolve the types of the formals now, because the freeze point may
@@ -1535,6 +1556,10 @@ package body Sem_Ch6 is
          Rewrite (N, Null_Body);
          Analyze (N);
       end if;
+
+   <<Leave>>
+      Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
+      Restore_Ghost_Region (Saved_GM, Saved_IGR);
    end Analyze_Null_Procedure;
 
    -----------------------------
@@ -1583,7 +1608,7 @@ package body Sem_Ch6 is
    ----------------------------
 
    --  WARNING: This routine manages Ghost regions. Return statements must be
-   --  replaced by gotos which jump to the end of the routine and restore the
+   --  replaced by gotos that jump to the end of the routine and restore the
    --  Ghost mode.
 
    procedure Analyze_Procedure_Call (N : Node_Id) is
@@ -2249,7 +2274,7 @@ package body Sem_Ch6 is
    --  the subprogram, or to perform conformance checks.
 
    --  WARNING: This routine manages Ghost regions. Return statements must be
-   --  replaced by gotos which jump to the end of the routine and restore the
+   --  replaced by gotos that jump to the end of the routine and restore the
    --  Ghost mode.
 
    procedure Analyze_Subprogram_Body_Helper (N : Node_Id) is
@@ -3394,7 +3419,7 @@ package body Sem_Ch6 is
          if Is_Generic_Subprogram (Prev_Id) then
             Spec_Id := Prev_Id;
 
-            --  A subprogram body is Ghost when it is stand alone and subject
+            --  A subprogram body is Ghost when it is stand-alone and subject
             --  to pragma Ghost or when the corresponding spec is Ghost. Set
             --  the mode now to ensure that any nodes generated during analysis
             --  and expansion are properly marked as Ghost.
@@ -3446,7 +3471,7 @@ package body Sem_Ch6 is
             if Is_Private_Concurrent_Primitive (Body_Id) then
                Spec_Id := Disambiguate_Spec;
 
-               --  A subprogram body is Ghost when it is stand alone and
+               --  A subprogram body is Ghost when it is stand-alone and
                --  subject to pragma Ghost or when the corresponding spec is
                --  Ghost. Set the mode now to ensure that any nodes generated
                --  during analysis and expansion are properly marked as Ghost.
@@ -3462,7 +3487,7 @@ package body Sem_Ch6 is
             else
                Spec_Id := Find_Corresponding_Spec (N);
 
-               --  A subprogram body is Ghost when it is stand alone and
+               --  A subprogram body is Ghost when it is stand-alone and
                --  subject to pragma Ghost or when the corresponding spec is
                --  Ghost. Set the mode now to ensure that any nodes generated
                --  during analysis and expansion are properly marked as Ghost.
@@ -3569,7 +3594,7 @@ package body Sem_Ch6 is
          else
             Spec_Id := Corresponding_Spec (N);
 
-            --  A subprogram body is Ghost when it is stand alone and subject
+            --  A subprogram body is Ghost when it is stand-alone and subject
             --  to pragma Ghost or when the corresponding spec is Ghost. Set
             --  the mode now to ensure that any nodes generated during analysis
             --  and expansion are properly marked as Ghost.

diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog
index 1a5888b7c449541a4c83a3ed418bad980523fc6e..b7373c9de8fd8848886c1401fa4f6f04fc350088 100644 (file)
--- a/gcc/testsuite/ChangeLog
+++ b/gcc/testsuite/ChangeLog
@@ -1,3 +1,7 @@
+2018-11-14  Hristian Kirtchev  <kirtchev@adacore.com>
+
+       * gnat.dg/ghost1.adb, gnat.dg/ghost1.ads: New testcase.
+
 2018-11-14  Javier Miranda  <miranda@adacore.com>
 
        * gnat.dg/equal5.adb, gnat.dg/equal5.ads: New testcase.

diff --git a/gcc/testsuite/gnat.dg/ghost1.adb b/gcc/testsuite/gnat.dg/ghost1.adb
new file mode 100644 (file)
index 0000000..7a2c551
--- /dev/null
+++ b/gcc/testsuite/gnat.dg/ghost1.adb
@@ -0,0 +1,8 @@
+--  { dg-do compile }
+
+package body Ghost1 is
+   procedure Body_Only (Obj : Ghost_Typ) is null
+     with Ghost;
+
+   procedure Spec_And_Body (Obj : Ghost_Typ) is null;
+end Ghost1;

diff --git a/gcc/testsuite/gnat.dg/ghost1.ads b/gcc/testsuite/gnat.dg/ghost1.ads
new file mode 100644 (file)
index 0000000..afbcc2f
--- /dev/null
+++ b/gcc/testsuite/gnat.dg/ghost1.ads
@@ -0,0 +1,9 @@
+package Ghost1 is
+   type Ghost_Typ is record
+      Data : Integer;
+   end record
+     with Ghost;
+
+   procedure Spec_And_Body (Obj : Ghost_Typ)
+     with Ghost;
+end Ghost1;