This patch the following SPARK rule (the part about 'Loop_Entry, 'Old, 'Update)
If the Extensions_Visible aspect is False for a subprogram, then certain restrictions are imposed on the use of any parameter of the subprogram which is of a specific tagged type. Such a parameter shall not be converted to a class-wide type. Such a parameter shall not be passed as an actual parameter in a call to a subprogram whose Extensions_Visible aspect is True. These restrictions also apply to any parenthesized expression, qualified expression, or type conversion whose operand is subject to these restrictions, to any Old, Update, or Loop_Entry attribute_reference whose prefix is subject to these restrictions, and to any conditional expression having at least one dependent_expression which is subjec to these restrictions. ------------ -- Source -- ------------ -- test_loop_entry_old_update.adb procedure Test_Loop_Entry_Old_Update is -- Test that Extensions_Visible restrictions are enforced for -- Old, Update, and Loop_Entry attribute references. pragma Assertion_Policy (Check); package Pkg is type T is abstract tagged record Int1, Int2, Int3 : Integer; end record; function Is_Bodacious (X : T) return Boolean is abstract; end Pkg; use Pkg; procedure P1 (X : in out T) with Post => Is_Bodacious (T'Class (X'Old)), -- ERROR Extensions_Visible => False; procedure P1 (X : in out T) is begin null; end P1; procedure P2 (X : in out T) with Extensions_Visible => False; procedure P2 (X : in out T) is begin if Is_Bodacious (T'Class (X'Update (Int1 => 123))) then -- ERROR X.Int1 := 123; end if; end P2; procedure P3 (X : in out T) with Extensions_Visible => False; procedure P3 (X : in out T) is begin for I in 1 .. 10 loop X.Int1 := X.Int1 + 1; pragma Assert ((X.Int1 /= X.Int2) or else Is_Bodacious (T'Class (X'Loop_Entry))); -- ERROR end loop; end P3; procedure P4 (X : in out T; Y : T'Class) with Extensions_Visible => False; procedure P4 (X : in out T; Y : T'Class) is begin if Is_Bodacious (T'Class (T'(if X.Int1 = X.Int2 -- ERROR then X'Update (Int1 => X.Int1 + 1) else T (Y)))) then X.Int1 := 456; end if; end P4; begin null; end Test_Loop_Entry_Old_Update; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c test_loop_entry_old_update.adb test_loop_entry_old_update.adb:15:38: formal parameter with Extensions_Visible False cannot be converted to class-wide type test_loop_entry_old_update.adb:22:34: formal parameter with Extensions_Visible False cannot be converted to class-wide type test_loop_entry_old_update.adb:33:44: formal parameter with Extensions_Visible False cannot be converted to class-wide type test_loop_entry_old_update.adb:42:13: formal parameter with Extensions_Visible False cannot be converted to class-wide type Tested on x86_64-pc-linux-gnu, committed on trunk 2014-11-20 Hristian Kirtchev <kirtc...@adacore.com> * sem_util.adb (Is_EVF_Expression): Include attributes 'Loop_Entry, 'Old and 'Update to the logic.
Index: sem_util.adb =================================================================== --- sem_util.adb (revision 217835) +++ sem_util.adb (working copy) @@ -10846,6 +10846,16 @@ N_Type_Conversion) then return Is_EVF_Expression (Expression (N)); + + -- Attributes 'Loop_Entry, 'Old and 'Update are an EVF expression when + -- their prefix denotes an EVF expression. + + elsif Nkind (N) = N_Attribute_Reference + and then Nam_In (Attribute_Name (N), Name_Loop_Entry, + Name_Old, + Name_Update) + then + return Is_EVF_Expression (Prefix (N)); end if; return False;