diff mbox series

[Ada] Support aspect Relaxed_Initialization on private types and constants

Message ID 20200617081611.GA55400@adacore.com
State New
Headers show
Series [Ada] Support aspect Relaxed_Initialization on private types and constants | expand

Commit Message

Pierre-Marie de Rodat June 17, 2020, 8:16 a.m. UTC
Aspect Relaxed_Initialization can now be attached to private types and
deferred constants, but only to their private views. This is similar to
the spirit of SPARK RM 6.9(9) for ghost aspect, which says:

  "[This rule is to ensure that the ghostliness of a visible entity can be
  determined without having to look into the private part of the enclosing
  package.]"

Note: implementation of this rule for Ghost aspect appears to be
slightly wrong. We require Ghost aspect to be repeated on a full view
that completes a private type, but only for record types.

Tested on x86_64-pc-linux-gnu, committed on trunk

2020-06-17  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* einfo.adb (Is_Relaxed_Initialization_State): Add reference to
	SPARK RM.
	* sem_attr.adb (Analyze_Attribute_Old_Result): Likewise.
	* sem_ch13.adb (Analyze_Aspect_Relaxed_Initialization): Reject
	aspect on completions of private types and deferred constants.
	* sem_util.ads, sem_util.adb (Has_Relaxed_Initialization):
	Adjust comments; support queries for constants.
diff mbox series

Patch

--- gcc/ada/einfo.adb
+++ gcc/ada/einfo.adb
@@ -8256,8 +8256,7 @@  package body Einfo is
    function Is_Relaxed_Initialization_State (Id : E) return B is
    begin
       --  To qualify, the abstract state must appear with simple option
-      --  "Relaxed_Initialization" (??? add reference to SPARK RM once the
-      --  Relaxed_Initialization aspect is described there).
+      --  "Relaxed_Initialization" (SPARK RM 6.10).
 
       return
         Ekind (Id) = E_Abstract_State

--- gcc/ada/sem_attr.adb
+++ gcc/ada/sem_attr.adb
@@ -1333,8 +1333,7 @@  package body Sem_Attr is
                null;
 
             --  Attribute 'Result is allowed to appear in aspect
-            --  Relaxed_Initialization (??? add reference to SPARK RM once this
-            --  attribute is described there).
+            --  Relaxed_Initialization (SPARK RM 6.10).
 
             elsif Prag_Nam = Name_Relaxed_Initialization
               and then Aname = Name_Result

--- gcc/ada/sem_ch13.adb
+++ gcc/ada/sem_ch13.adb
@@ -2216,19 +2216,37 @@  package body Sem_Ch13 is
                --  Will be set to True if we need to restore the scope table
                --  after analyzing the aspect expression.
 
+               Prev_Id : Entity_Id;
+
             --  Start of processing for Analyze_Aspect_Relaxed_Initialization
 
             begin
                --  Set name of the aspect for error messages
                Error_Msg_Name_1 := Nam;
 
-               --  Annotation of a type; no aspect expression is allowed
+               --  Annotation of a type; no aspect expression is allowed.
+               --  For a private type, the aspect must be attached to the
+               --  partial view.
+               --
                --  ??? Once the exact rule for this aspect is ready, we will
                --  likely reject concurrent types, etc., so let's keep the code
                --  for types and variable separate.
 
                if Is_First_Subtype (E) then
-                  if Present (Expr) then
+                  Prev_Id := Incomplete_Or_Partial_View (E);
+                  if Present (Prev_Id) then
+
+                     --  Aspect may appear on the full view of an incomplete
+                     --  type because the incomplete declaration cannot have
+                     --  any aspects.
+
+                     if Ekind (Prev_Id) = E_Incomplete_Type then
+                        null;
+                     else
+                        Error_Msg_N ("aspect % must apply to partial view", N);
+                     end if;
+
+                  elsif Present (Expr) then
                      Error_Msg_N ("illegal aspect % expression", Expr);
                   end if;
 
@@ -2239,6 +2257,19 @@  package body Sem_Ch13 is
                      Error_Msg_N ("illegal aspect % expression", Expr);
                   end if;
 
+               --  Annotation of a constant; no aspect expression is allowed.
+               --  For a deferred constant, the aspect must be attached to the
+               --  partial view.
+
+               elsif Ekind (E) = E_Constant then
+                  if Present (Incomplete_Or_Partial_View (E)) then
+                     Error_Msg_N
+                       ("aspect % must apply to deferred constant", N);
+
+                  elsif Present (Expr) then
+                     Error_Msg_N ("illegal aspect % expression", Expr);
+                  end if;
+
                --  Annotation of a subprogram; aspect expression is required
 
                elsif Is_Subprogram (E) then

--- gcc/ada/sem_util.adb
+++ gcc/ada/sem_util.adb
@@ -12495,13 +12495,20 @@  package body Sem_Util is
          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.
+
+         when E_Constant =>
+            return Has_Aspect (E, Aspect_Relaxed_Initialization);
+
          --  Variables have this aspect attached directly
 
          when E_Variable =>
             return Has_Aspect (E, Aspect_Relaxed_Initialization);
 
          --  Types have this aspect attached directly (though we only allow it
-         --  to be specified for the first subtype).
+         --  to be specified for the first subtype). For private types, the
+         --  aspect is attached to the partial view.
 
          when Type_Kind =>
             pragma Assert (Is_First_Subtype (E));

--- gcc/ada/sem_util.ads
+++ gcc/ada/sem_util.ads
@@ -1382,9 +1382,10 @@  package Sem_Util is
    --  yet received a full declaration.
 
    function Has_Relaxed_Initialization (E : Entity_Id) return Boolean;
-   --  Returns True iff entity E, which can be either a type, a variable, an
-   --  abstract state or a function, is subject to the Relaxed_Initialization
-   --  aspect.
+   --  Returns True iff entity E is subject to the Relaxed_Initialization
+   --  aspect. Entity E can be either type, variable, constant, function,
+   --  or abstract state. 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.