+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
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)