diff mbox series

[Ada] Update FE check following change in SPARK RM 7.1.3(12)

Message ID 20180528085912.GA68405@adacore.com
State New
Headers show
Series [Ada] Update FE check following change in SPARK RM 7.1.3(12) | expand

Commit Message

Pierre-Marie de Rodat May 28, 2018, 8:59 a.m. UTC 
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  <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.
diff mbox series

Patch

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