ada: Deconstruct support for abstract states with Relaxed_Initialization

GNATprove newer implemented support for abstract states with aspect
Relaxed_Initialization, so the frontend support is now deconstructed.

gcc/ada/

	* einfo-utils.adb (Is_Relaxed_Initialization_State): Remove.
	* einfo-utils.ads (Is_Relaxed_Initialization_State): Remove.
	* einfo.ads: Remove description of removed aspect.
	* fe.h (Is_Relaxed_Initialization_State): Remove.
	* sem_prag.adb (Analyze_Abstract_State): Remove support for
	Relaxed_Initialization.
	* sem_util.adb (Has_Relaxed_Initialization): Likewise.
	* sem_util.ads (Has_Relaxed_Initialization): Likewise.

diff --git a/gcc/ada/einfo-utils.adb b/gcc/ada/einfo-utils.adb
index 00799eb9beea6085e258d832cd733a37045aa273..438868ac7573ed07f3808cd2088a2f39e1ae3106 100644 (file)
--- a/gcc/ada/einfo-utils.adb
+++ b/gcc/ada/einfo-utils.adb
@@ -1649,20 +1649,6 @@ package body Einfo.Utils is
           and then Is_Protected_Type (Corresponding_Concurrent_Type (Id));
    end Is_Protected_Record_Type;
 
-   -------------------------------------
-   -- Is_Relaxed_Initialization_State --
-   -------------------------------------
-
-   function Is_Relaxed_Initialization_State (Id : E) return B is
-   begin
-      --  To qualify, the abstract state must appear with simple option
-      --  "Relaxed_Initialization" (SPARK RM 6.10).
-
-      return
-        Ekind (Id) = E_Abstract_State
-          and then Has_Option (Id, Name_Relaxed_Initialization);
-   end Is_Relaxed_Initialization_State;
-
    --------------------------------
    -- Is_Standard_Character_Type --
    --------------------------------

diff --git a/gcc/ada/einfo-utils.ads b/gcc/ada/einfo-utils.ads
index 701d8ce59fbdaebf613679cbfb32e5e34135d42d..d87a3e34f493e070d1fd9d0abfb99e91cca03ced 100644 (file)
--- a/gcc/ada/einfo-utils.ads
+++ b/gcc/ada/einfo-utils.ads
@@ -201,7 +201,6 @@ package Einfo.Utils is
    function Is_Protected_Component (Id : E) return B with Inline;
    function Is_Protected_Interface (Id : E) return B;
    function Is_Protected_Record_Type (Id : E) return B with Inline;
-   function Is_Relaxed_Initialization_State (Id : E) return B;
    function Is_Standard_Character_Type (Id : E) return B;
    function Is_Standard_String_Type (Id : E) return B;
    function Is_String_Type (Id : E) return B with Inline;

diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 6f563d5e62cc83ad949825f31badc5d4dbeca3d8..e3bfdb3507d12fc4583fdb9e2f7a51316be935e0 100644 (file)
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -3219,10 +3219,6 @@ package Einfo is
 --       Applies to all entities, true for record types and subtypes,
 --       includes class-wide types and subtypes (which are also records).
 
---    Is_Relaxed_Initialization_State (synthesized)
---       Applies to all entities, true for abstract states that are subject to
---       option Relaxed_Initialization.
-
 --    Is_Remote_Call_Interface
 --       Defined in all entities. Set in E_Package and E_Generic_Package
 --       entities to which a pragma Remote_Call_Interface is applied, and
@@ -5129,7 +5125,6 @@ package Einfo is
    --    Has_Null_Visible_Refinement         (synth)
    --    Is_External_State                   (synth)
    --    Is_Null_State                       (synth)
-   --    Is_Relaxed_Initialization_State     (synth)
    --    Is_Synchronized_State               (synth)
    --    Partial_Refinement_Constituents     (synth)
 

diff --git a/gcc/ada/fe.h b/gcc/ada/fe.h
index 6aaa3fdc4d33c35f398ea1db52c897870d4949b4..397045ea5839d197af7b6481d24c555c4021d500 100644 (file)
--- a/gcc/ada/fe.h
+++ b/gcc/ada/fe.h
@@ -501,9 +501,6 @@ B Is_Protected_Interface              (E Id);
 #define Is_Protected_Record_Type einfo__utils__is_protected_record_type
 B Is_Protected_Record_Type            (E Id);
 
-#define Is_Relaxed_Initialization_State einfo__utils__is_relaxed_initialization_state
-B Is_Relaxed_Initialization_State     (E Id);
-
 #define Is_Standard_Character_Type einfo__utils__is_standard_character_type
 B Is_Standard_Character_Type          (E Id);
 

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 39005aaea05ae6013a672e5ce95036f7f22dcc69..299e388167fb9601c2afbba2881b543253890f34 100644 (file)
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -12181,16 +12181,15 @@ package body Sem_Prag is
             is
                --  Flags used to verify the consistency of options
 
-               AR_Seen                     : Boolean := False;
-               AW_Seen                     : Boolean := False;
-               ER_Seen                     : Boolean := False;
-               EW_Seen                     : Boolean := False;
-               External_Seen               : Boolean := False;
-               Ghost_Seen                  : Boolean := False;
-               Others_Seen                 : Boolean := False;
-               Part_Of_Seen                : Boolean := False;
-               Relaxed_Initialization_Seen : Boolean := False;
-               Synchronous_Seen            : Boolean := False;
+               AR_Seen          : Boolean := False;
+               AW_Seen          : Boolean := False;
+               ER_Seen          : Boolean := False;
+               EW_Seen          : Boolean := False;
+               External_Seen    : Boolean := False;
+               Ghost_Seen       : Boolean := False;
+               Others_Seen      : Boolean := False;
+               Part_Of_Seen     : Boolean := False;
+               Synchronous_Seen : Boolean := False;
 
                --  Flags used to store the static value of all external states'
                --  expressions.
@@ -12672,12 +12671,6 @@ package body Sem_Prag is
                            Check_Duplicate_Option (Opt, Synchronous_Seen);
                            Check_Ghost_Synchronous;
 
-                        --  Relaxed_Initialization
-
-                        elsif Chars (Opt) = Name_Relaxed_Initialization then
-                           Check_Duplicate_Option
-                             (Opt, Relaxed_Initialization_Seen);
-
                         --  Option Part_Of without an encapsulating state is
                         --  illegal (SPARK RM 7.1.4(8)).
 

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index ef6f3823b1baa5f1e6eda04e0ed88c0bc93b9ed4..c47904f168c8e494ec8e140757320e6946b47ae3 100644 (file)
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -13106,11 +13106,6 @@ package body Sem_Util is
       --  but now without any syntactic checks.
 
       case Ekind (E) is
-         --  Abstract states have option Relaxed_Initialization
-
-         when E_Abstract_State =>
-            return Is_Relaxed_Initialization_State (E);
-
          --  Constants have this aspect attached directly; for deferred
          --  constants, the aspect is attached to the partial view.
 

diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 384b9a3dac87a473ddc9e5ebe923419348448947..db02d39fdeea80fba29fcedbe28b8044e23307f5 100644 (file)
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1516,9 +1516,9 @@ package Sem_Util is
 
    function Has_Relaxed_Initialization (E : Entity_Id) return Boolean;
    --  Returns True iff entity E is subject to the Relaxed_Initialization
-   --  aspect. Entity E can be either type, variable, constant, subprogram,
-   --  entry or an abstract state. For private types and deferred constants
-   --  E should be the private view, because aspect can only be attached there.
+   --  aspect. Entity E can be either type, variable, constant, subprogram or
+   --  entry. For private types and deferred constants E should be the private
+   --  view, because aspect can only be attached there.
 
    function Has_Signed_Zeros (E : Entity_Id) return Boolean;
    --  Determines if the floating-point type E supports signed zeros.