[Ada] Update FE check following change in SPARK RM 7.1.3(12)
authorYannick Moy <moy@adacore.com>
Mon, 28 May 2018 08:55:35 +0000 (08:55 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Mon, 28 May 2018 08:55:35 +0000 (08:55 +0000)
SPARK Reference Manual changed to accept attributes First, Last and Length
as not leading to an evaluation of a part of the prefix object. This is
reflected here in the checking code for that rule.

2018-05-28  Yannick Moy  <moy@adacore.com>

gcc/ada/

* sem_util.adb (Is_OK_Volatile_Context): Add attributes First, Last and
Length as valid non-interfering contexts for SPARK.

From-SVN: r260836

gcc/ada/ChangeLog
gcc/ada/sem_util.adb

index 431066776902cc315fcc9d10420935a1f1b59f00..19cb29682eba4f72b8a2628a57bc0484cd141aea 100644 (file)
@@ -1,3 +1,8 @@
+2018-05-28  Yannick Moy  <moy@adacore.com>
+
+       * sem_util.adb (Is_OK_Volatile_Context): Add attributes First, Last and
+       Length as valid non-interfering contexts for SPARK.
+
 2018-05-28  Claire Dross  <dross@adacore.com>
 
        * sem_disp.ads, sem_disp.adb (Inheritance_Utilities): Package for
index 4d66d3898e7f6c043c134eba40a68aef187f50dd..4cef1baea7d63a425ebcb8a3dcf9a2bfb0802d99 100644 (file)
@@ -15999,16 +15999,19 @@ package body Sem_Util is
          return True;
 
       --  The volatile object appears as the prefix of attributes Address,
-      --  Alignment, Component_Size, First_Bit, Last_Bit, Position, Size,
-      --  Storage_Size.
+      --  Alignment, Component_Size, First, First_Bit, Last, Last_Bit, Length,
+      --  Position, Size, Storage_Size.
 
       elsif Nkind (Context) = N_Attribute_Reference
         and then Prefix (Context) = Obj_Ref
         and then Nam_In (Attribute_Name (Context), Name_Address,
                                                    Name_Alignment,
                                                    Name_Component_Size,
+                                                   Name_First,
                                                    Name_First_Bit,
+                                                   Name_Last,
                                                    Name_Last_Bit,
+                                                   Name_Length,
                                                    Name_Position,
                                                    Name_Size,
                                                    Name_Storage_Size)