[Ada] Invariant checks on view conversion

[Arnaud Charlet <charlet@adacore.com>]

[-- Attachment #1: Type: text/plain, Size: 2150 bytes --]

This patch inplements RM 7.3.2 (12/3): an invariant check must be applied to
the result of a view conversion if the type of the expression has invariants.

THe following must execute quietly:

   gnatmake -q -gnata t_package_test
   t_package_test

---
with Ada.Assertions; use Ada.Assertions;
with T_Ancestor_Package;
with T_Package;
procedure T_Package_Test is
   pragma Assertion_Policy (Check);
   My_T_Ancestor : constant T_Ancestor_Package.T_Ancestor := (A => 3);
   -- Initialise My_T with something valid otherwise may get an
   --  Assertion_Error here
   My_T : T_Package.T := T_Package.Init; -- Sets to (A => 1, B => 2)
begin
   -- Should make invariant false
   T_Ancestor_Package.T_Ancestor (My_T) := My_T_Ancestor;
   raise Program_Error;
exception
   when Assertion_Error => null;
end T_Package_Test;
---
package T_Ancestor_Package is
   pragma Assertion_Policy (Check);
   type T_Ancestor is tagged record
      A : Integer;
   end record;
   function Init return T_Ancestor;
end T_Ancestor_Package;
---
package body T_Ancestor_Package is
   pragma Assertion_Policy (Check);
   function Init return T_Ancestor is
   begin
      return (A => 1);
   end Init;
end T_Ancestor_Package;
---
with T_Ancestor_Package;
package T_Package is
   pragma Assertion_Policy (Check);
   type T is new T_Ancestor_Package.T_Ancestor with private
     with
       Type_Invariant => Increasing (T);
   function Increasing (My_T : in T) return
     Boolean;
   function Init return T;
private
   type T is new T_Ancestor_Package.T_Ancestor with record
      B : Integer;
   end record;
end T_Package;
---
package body T_Package is
   pragma Assertion_Policy (Check);
   function Increasing (My_T : in T) return Boolean is
   begin
      return My_T.B > My_T.A;
   end Increasing;
   function Init return T is
   begin
      return (T_Ancestor_Package.Init with B => 2);
   end Init;
end T_Package;

Tested on x86_64-pc-linux-gnu, committed on trunk

2015-01-07  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch5.adb (Analyze_Assignment): If left-hand side is a view
	conversion and type of expression has invariant, apply invariant
	check on expression.


[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 1025 bytes --]

Index: sem_ch5.adb
===================================================================
--- sem_ch5.adb	(revision 219280)
+++ sem_ch5.adb	(working copy)
@@ -764,6 +764,18 @@
          Set_Referenced_Modified (Lhs, Out_Param => False);
       end if;
 
+      --  RM 7.3.2 (12/3)  An assignment to a view conversion (from a type
+      --  to one of its ancestors) requires an invariant check. Apply check
+      --  only if expression comes from source, otherwise it will be applied
+      --  when value is assigned to source entity.
+
+      if Nkind (Lhs) = N_Type_Conversion
+        and then Has_Invariants (Etype (Expression (Lhs)))
+        and then Comes_From_Source (Expression (Lhs))
+      then
+         Insert_After (N, Make_Invariant_Call (Expression (Lhs)));
+      end if;
+
       --  Final step. If left side is an entity, then we may be able to reset
       --  the current tracked values to new safe values. We only have something
       --  to do if the left side is an entity name, and expansion has not