diff gcc/ada/ghost.ads @ 132:d34655255c78

update gcc-8.2
author mir3636
date Thu, 25 Oct 2018 10:21:07 +0900
parents 84e7813d76e9
children 1830386684a0
line wrap: on
line diff
--- a/gcc/ada/ghost.ads	Thu Oct 25 08:08:40 2018 +0900
+++ b/gcc/ada/ghost.ads	Thu Oct 25 10:21:07 2018 +0900
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2014-2017, Free Software Foundation, Inc.         --
+--          Copyright (C) 2014-2018, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -31,10 +31,6 @@
 
 package Ghost is
 
-   procedure Add_Ignored_Ghost_Unit (Unit : Node_Id);
-   --  Add a single ignored Ghost compilation unit to the internal table for
-   --  post processing.
-
    procedure Check_Ghost_Completion
      (Prev_Id  : Entity_Id;
       Compl_Id : Entity_Id);
@@ -68,15 +64,20 @@
    --  Verify that the Ghost policy of constituent Constit_Id is compatible
    --  with the Ghost policy of abstract state State_I.
 
+   procedure Check_Ghost_Type (Typ : Entity_Id);
+   --  Verify that Ghost type Typ is neither concurrent, nor effectively
+   --  volatile.
+
    function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
    --  Determine whether type Typ implements at least one Ghost interface
 
    procedure Initialize;
    --  Initialize internal tables
 
-   procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type);
-   --  Set the value of global variable Ghost_Mode depending on the Ghost
-   --  policy denoted by Mode.
+   procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
+   pragma Inline (Install_Ghost_Region);
+   --  Install a Ghost region described by mode Mode and ignored region start
+   --  node N.
 
    function Is_Ghost_Assignment (N : Node_Id) return Boolean;
    --  Determine whether arbitrary node N denotes an assignment statement whose
@@ -107,7 +108,7 @@
    --    * The left hand side denotes a Ghost entity
    --
    --  Install the Ghost mode of the assignment statement. This routine starts
-   --  a Ghost region and must be used in conjunction with Restore_Ghost_Mode.
+   --  a Ghost region and must be used with routine Restore_Ghost_Region.
 
    procedure Mark_And_Set_Ghost_Body
      (N       : Node_Id;
@@ -122,7 +123,7 @@
    --    * The body appears within a Ghost region
    --
    --  Install the Ghost mode of the body. This routine starts a Ghost region
-   --  and must be used in conjunction with Restore_Ghost_Mode.
+   --  and must be used with routine Restore_Ghost_Region.
 
    procedure Mark_And_Set_Ghost_Completion
      (N       : Node_Id;
@@ -135,7 +136,7 @@
    --    * The completion appears within a Ghost region
    --
    --  Install the Ghost mode of the completion. This routine starts a Ghost
-   --  region and must be used in conjunction with Restore_Ghost_Mode.
+   --  region and must be used with routine Restore_Ghost_Region.
 
    procedure Mark_And_Set_Ghost_Declaration (N : Node_Id);
    --  Mark declaration N as Ghost when:
@@ -148,7 +149,7 @@
    --    * The declaration appears within a Ghost region
    --
    --  Install the Ghost mode of the declaration. This routine starts a Ghost
-   --  region and must be used in conjunction with Restore_Ghost_Mode.
+   --  region and must be used with routine Restore_Ghost_Region.
 
    procedure Mark_And_Set_Ghost_Instantiation
      (N      : Node_Id;
@@ -162,7 +163,7 @@
    --    * The instantiation appears within a Ghost region
    --
    --  Install the Ghost mode of the instantiation. This routine starts a Ghost
-   --  region and must be used in conjunction with Restore_Ghost_Mode.
+   --  region and must be used with routine Restore_Ghost_Region.
 
    procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id);
    --  Mark procedure call N as Ghost when:
@@ -170,7 +171,7 @@
    --    * The procedure being invoked is a Ghost entity
    --
    --  Install the Ghost mode of the procedure call. This routine starts a
-   --  Ghost region and must be used in conjunction with Restore_Ghost_Mode.
+   --  Ghost region and must be used with routine Restore_Ghost_Region.
 
    procedure Mark_Ghost_Clause (N : Node_Id);
    --  Mark use package, use type, or with clause N as Ghost when:
@@ -200,14 +201,19 @@
    --  WARNING: this is a separate front end pass, care should be taken to keep
    --  it optimized.
 
-   procedure Restore_Ghost_Mode (Mode : Ghost_Mode_Type);
-   --  Terminate a Ghost region by restoring the Ghost mode prior to the
-   --  region denoted by Mode. This routine must be used in conjunction
-   --  with Mark_And_Set_xxx routines as well as Set_Ghost_Mode.
+   procedure Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
+   pragma Inline (Restore_Ghost_Region);
+   --  Restore a Ghost region to a previous state described by mode Mode and
+   --  ignored region start node N. This routine must be used in conjunction
+   --  with the following routines:
+   --
+   --    Install_Ghost_Region
+   --    Mark_And_Set_xxx
+   --    Set_Ghost_Mode
 
    procedure Set_Ghost_Mode (N : Node_Or_Entity_Id);
    --  Install the Ghost mode of arbitrary node N. This routine starts a Ghost
-   --  region and must be used in conjunction with Restore_Ghost_Mode.
+   --  region and must be used with routine Restore_Ghost_Region.
 
    procedure Set_Is_Ghost_Entity (Id : Entity_Id);
    --  Set the relevant Ghost attributes of entity Id depending on the current