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.
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-05-28 Yannick Moy <m...@adacore.com>
gcc/ada/
* sem_util.adb (Is_OK_Volatile_Context): Add attributes First, Last and
Length as valid non-interfering contexts for SPARK.--- gcc/ada/sem_util.adb
+++ 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)
