diff options
| author | Yannick Moy <moy@adacore.com> | 2018-05-28 08:55:35 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2018-05-28 08:55:35 +0000 |
| commit | cb1a067201dec2585968531ee1a03363bf9210f5 (patch) | |
| tree | d921ff0a59b546253d25386934a70b527fdaa173 /gcc | |
| parent | cc821e65107ed263200b8ee6650f0704311757c9 (diff) | |
| download | gcc-cb1a067201dec2585968531ee1a03363bf9210f5.zip gcc-cb1a067201dec2585968531ee1a03363bf9210f5.tar.gz gcc-cb1a067201dec2585968531ee1a03363bf9210f5.tar.bz2 | |
[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 <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
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 7 |
2 files changed, 10 insertions, 2 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 4310667..19cb296 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -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 diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 4d66d38..4cef1ba 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) |