The frontend does not expand record equalities found in Ada 2012 pre/post conditions. After this patch the execution of the following test fails the postcondition (as expected).
procedure Old_Bug is type Val is new Integer; type Index is new Integer range 1 .. 10; type Point is record X, Y : Val; end record; type Points is array (Index) of Point; procedure Set_X_Of_Nth (P : in out Points; V : Val; N : Index) with Post => (for all M in Index => P(M) = P'Old(M)); -- Test procedure Set_X_Of_Nth (P : in out Points; V : Val; N : Index) is begin P (N).X := V; end; Here : Points := (others => (0,0)); begin Set_X_Of_Nth (Here, 5, 5); end; Command: gnatmake -q -gnata -gnat12 old_bug; ./old_bug Output: raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed postcondition from old_bug.adb:9 Tested on x86_64-pc-linux-gnu, committed on trunk 2011-08-02 Javier Miranda <mira...@adacore.com> * exp_ch4.adb (Expand_N_Quantified_Expression): Force reanalysis and expansion of the condition. Required since the previous analysis was done with expansion disabled (see Resolve_Quantified_Expression) and hence checks were not inserted and record comparisons have not been expanded.
Index: exp_ch4.adb =================================================================== --- exp_ch4.adb (revision 177087) +++ exp_ch4.adb (working copy) @@ -7502,6 +7502,13 @@ Cond := Relocate_Node (Condition (N)); + -- Reset flag analyzed in the condition to force its analysis. Required + -- since the previous analysis was done with expansion disabled (see + -- Resolve_Quantified_Expression) and hence checks were not inserted + -- and record comparisons have not been expanded. + + Reset_Analyzed_Flags (Cond); + if Is_Universal then Cond := Make_Op_Not (Loc, Cond); end if;