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 <schonb...@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.
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