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 <[email protected]>
* 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;