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;

Reply via email to