[Ada] Interaction between 'Loop_Entry, 'Old, 'Update and Extensions_Visible

[Arnaud Charlet]

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  <kirtchev@adacore.com>

	* sem_util.adb (Is_EVF_Expression): Include
	attributes 'Loop_Entry, 'Old and 'Update to the logic.

-------------- next part --------------
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;