From: Yannick Moy Date: Mon, 28 May 2018 08:55:35 +0000 (+0000) Subject: [Ada] Update FE check following change in SPARK RM 7.1.3(12) X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cb1a067201dec2585968531ee1a03363bf9210f5;p=gcc.git [Ada] Update FE check following change in SPARK RM 7.1.3(12) 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 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 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 43106677690..19cb29682eb 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2018-05-28 Yannick Moy + + * 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 * sem_disp.ads, sem_disp.adb (Inheritance_Utilities): Package for diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 4d66d3898e7..4cef1baea7d 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -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)